(* Generated by the EML-lang Coq backend *)
(* Source module: soft_actuator *)
(* Source file:   /home/monogate/monogate/forge/examples/soft_actuator.eml *)
(* Verified fns:  soft_actuator *)

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

Definition OUT_MIN : R := (- 1.0).
Definition OUT_MAX : R := 1.0.

(* ── soft_actuator ── *)

Definition soft_actuator (error : R) (gain : R) : R :=
  let raw := tanh (gain * error) in
  Rmin OUT_MAX (Rmax OUT_MIN raw).

(* source obligations for soft_actuator: {O1, O2} *)
(*   O1 [407e1cf6bb77] -> PRESERVED (equivalent)  theorem soft_actuator_within_band -- 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 *)
(*   O2 [ce05ed80f322] -> PRESERVED (equivalent)  theorem soft_actuator_within_band -- 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 soft_actuator_within_band (error : R) (gain : R)
    (h_error : (- 100.0 <= error /\ error <= 100.0))
    (h_gain : (- 10.0 <= gain /\ gain <= 10.0)) :
    (((soft_actuator error gain) >= OUT_MIN)) /\ (((soft_actuator error gain) <= OUT_MAX)).
Proof.
  unfold soft_actuator, OUT_MAX, OUT_MIN, Rmin, Rmax.
  repeat destruct (Rle_dec _ _); lra.
Qed.