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

import MachLib.EML
import MachLib.Trig
import MachLib.Forge
import MachLib.Linarith
import MachLib.FixedPoint
import MachLib.SignTactic

open MachLib
open MachLib.Real

noncomputable def OUT_MIN : Real := (-(1 : Real))
noncomputable def OUT_MAX : Real := (1 : Real)

-- ── soft_actuator ──

noncomputable def soft_actuator (error : Real) (gain : Real) : Real :=
  (min (max (Real.tanh (gain * error)) OUT_MIN) OUT_MAX)

theorem soft_actuator_within_band (error : Real) (gain : Real)
    (h_error : (-(100.0 : Real) ≤ error ∧ error ≤ (100.0 : Real)))
    (h_gain : (-(10.0 : Real) ≤ gain ∧ gain ≤ (10.0 : Real)))
    (h_clamp1 : OUT_MIN ≤ OUT_MAX) :
    (((soft_actuator error gain) >= OUT_MIN)) ∧ (((soft_actuator error gain) <= OUT_MAX)) := by
  unfold soft_actuator
  refine ⟨?_, ?_⟩ <;>
    first
    | (apply lo_le_clamp <;> (first | assumption | mach_positivity))
    | apply clamp_le_hi
    | mach_positivity
    | mach_sign
    | (apply convex_comb_le <;> assumption)
    | (apply convex_comb_ge <;> assumption)
    | (apply convex_comb3_le <;> assumption)
    | (apply convex_comb3_ge <;> assumption)
    | (apply convex_comb4_le <;> assumption)
    | (apply convex_comb4_ge <;> assumption)
    | (apply convex_comb5_le <;> assumption)
    | (apply convex_comb5_ge <;> assumption)
    | (apply convex_comb6_le <;> assumption)
    | (apply convex_comb6_ge <;> assumption)
    | rfl
    | sorry  -- out of reach; left for the prover