(* Generated by the EML-lang Coq backend *)
(* Source module: rc_filter *)
(* Source file:   /home/monogate/monogate/forge/examples/rc_filter.eml *)
(* Verified fns:  tau, vout_steady, vout_initial, vout_charging, vout_charging_at_zero *)

Require Import Reals.
Require Import Lra.
Open Scope R_scope.

(* ── tau ── *)

Definition tau (r : R) (c : R) : R :=
  (r * c).

(* source obligations for tau: {O1} *)
(*   O1 [5ba209b56275] -> PRESERVED (equivalent)  theorem rc_time_constant_def -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem rc_time_constant_def (r : R) (c : R)
    (h1 : (r > 0.0))
    (h2 : (c > 0.0)) :
    ((tau r c) = (r * c)).
Proof.
  unfold tau.
  (* TODO: prove against MachLib foundations *)
Admitted.

(* ── vout_steady ── *)

Definition vout_steady (vin : R) : R :=
  vin.

(* source obligations for vout_steady: {O1} *)
(*   O1 [31596b009a78] -> PRESERVED (equivalent)  theorem rc_steady_state_equals_input -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem rc_steady_state_equals_input (vin : R) :
    ((vout_steady vin) = vin).
Proof.
  unfold vout_steady.
  (* TODO: prove against MachLib foundations *)
Admitted.

(* ── vout_initial ── *)

Definition vout_initial  : R :=
  0.0.

(* source obligations for vout_initial: {O1} *)
(*   O1 [72bd339ed0a8] -> PRESERVED (equivalent)  theorem rc_initial_output_zero -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem rc_initial_output_zero :
    ((vout_initial ) = 0.0).
Proof.
  unfold vout_initial.
  (* TODO: prove against MachLib foundations *)
Admitted.

(* ── vout_charging ── *)

Definition vout_charging (vin : R) (t : R) (tau_val : R) : R :=
  (vin * (1.0 - exp ((- t) / tau_val))).

(* source obligations for vout_charging: {O1} *)
(*   O1 [2982fe130529] -> PRESERVED (equivalent)  theorem rc_step_response_form -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem rc_step_response_form (vin : R) (t : R) (tau_val : R)
    (h1 : (tau_val > 0.0)) :
    ((vout_charging vin t tau_val) = (vin * (1.0 - exp ((- t) / tau_val)))).
Proof.
  unfold vout_charging.
  (* TODO: prove against MachLib foundations *)
Admitted.

(* ── vout_charging_at_zero ── *)

Definition vout_charging_at_zero (vin : R) (tau_val : R) : R :=
  (vin * (1.0 - exp (0.0 / tau_val))).

(* source obligations for vout_charging_at_zero: {O1} *)
(*   O1 [ca4ff999454f] -> PRESERVED (equivalent)  theorem rc_step_response_at_zero -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem rc_step_response_at_zero (vin : R) (tau_val : R)
    (h1 : (tau_val > 0.0)) :
    ((vout_charging_at_zero vin tau_val) = 0.0).
Proof.
  unfold vout_charging_at_zero.
  (* TODO: prove against MachLib foundations *)
Admitted.