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

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

Definition H_MIN : R := 1.0.
Definition H_MAX : R := 20.0.

(* ── catenary ── *)

Definition catenary (scale : R) (curv : R) (x : R) : R :=
  let raw := (scale * cosh (curv * x)) in
  Rmin H_MAX (Rmax H_MIN raw).

(* source obligations for catenary: {O1, O2} *)
(*   O1 [0199c9d0417e] -> PRESERVED (equivalent)  theorem catenary_within_envelope -- 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 [1d3d6d6a5e9d] -> PRESERVED (equivalent)  theorem catenary_within_envelope -- 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 catenary_within_envelope (scale : R) (curv : R) (x : R)
    (h_scale : (- 5.0 <= scale /\ scale <= 5.0))
    (h_curv : (- 0.5 <= curv /\ curv <= 0.5))
    (h_x : (- 4.0 <= x /\ x <= 4.0)) :
    (((catenary scale curv x) >= H_MIN)) /\ (((catenary scale curv x) <= H_MAX)).
Proof.
  unfold catenary, H_MAX, H_MIN, Rmin, Rmax.
  repeat destruct (Rle_dec _ _); lra.
Qed.