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

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

Definition Kp : R := 1.5.
Definition Ki : R := 0.4.
Definition Kd : R := 0.05.
Definition OUT_MIN : R := (- 1.0).
Definition OUT_MAX : R := 1.0.

(* ── pid ── *)

Definition pid (error : R) (integral : R) (derivative : R) : R :=
  let raw := (((Kp * error) + (Ki * integral)) + (Kd * derivative)) in
  Rmin OUT_MAX (Rmax OUT_MIN raw).

(* source obligations for pid: {O1, O2} *)
(*   O1 [ab7c27058d39] -> PRESERVED (equivalent)  theorem pid_output_clamped -- 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 [244a8c1dd7b9] -> PRESERVED (equivalent)  theorem pid_output_clamped -- 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 pid_output_clamped (error : R) (integral : R) (derivative : R)
    (h_error : (- 100.0 <= error /\ error <= 100.0))
    (h_integral : (- 100.0 <= integral /\ integral <= 100.0))
    (h_derivative : (- 100.0 <= derivative /\ derivative <= 100.0)) :
    (((pid error integral derivative) >= OUT_MIN)) /\ (((pid error integral derivative) <= OUT_MAX)).
Proof.
  unfold pid, Kd, Ki, Kp, OUT_MAX, OUT_MIN, Rmin, Rmax.
  repeat destruct (Rle_dec _ _); lra.
Qed.