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

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

(* ── oscillate ── *)

Definition oscillate (amplitude : R) (omega : R) (t : R) : R :=
  (amplitude * sin (omega * t)).

(* source obligations for oscillate: {O1} *)
(*   O1 [d2dda41d7165] -> PRESERVED (unreadable)  theorem sine_oscillator_amplitude_bound -- 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 sine_oscillator_amplitude_bound (amplitude : R) (omega : R) (t : R)
    (h1 : (amplitude >= 0.0))
    (h2 : (amplitude <= 1.0))
    (h3 : (omega >= 0.0))
    (h4 : (omega <= 10000.0))
    (h5 : (t >= 0.0)) :
    (Rabs (oscillate amplitude omega t) <= amplitude).
Proof.
  unfold oscillate.
  (* TODO: prove against MachLib foundations *)
Admitted.