Fast Float Evaluator

This file provides a fast, unverified floating-point evaluator for expressions. It is used only for heuristics to guide the verified search (e.g., finding good initial upper bounds for branch-and-bound optimization).

Main definitions

• evalFloat - Evaluate an expression using hardware floats
• FloatEnv - Environment mapping variable indices to Float values

Design notes

This evaluator uses Lean's native Float type, which maps to hardware IEEE 754 double precision. The results are NOT verified and should only be used as hints for the rigorous interval arithmetic algorithms.

Functions not directly available in Lean's Float stdlib are approximated:

• tanh(x) via (exp(2x) - 1) / (exp(2x) + 1)
• sinh(x) via (exp(x) - exp(-x)) / 2
• cosh(x) via (exp(x) + exp(-x)) / 2
• arsinh(x) via log(x + sqrt(x² + 1))
• atanh(x) via log((1+x)/(1-x)) / 2
• sinc(x) via sin(x)/x with special case at 0
• erf(x) via polynomial approximation

@[reducible, inline]

abbrev LeanCert.Engine.FloatEnv : Type

Evaluation environment for Floats

Equations

• LeanCert.Engine.FloatEnv = (ℕ → Float)

def LeanCert.Engine.evalFloat (e : Core.Expr) (ρ : FloatEnv) : Float

Fast, unverified floating point evaluator. Used only for heuristics to guide the verified search.

Equations

• LeanCert.Engine.evalFloat (LeanCert.Core.Expr.const q) ρ = LeanCert.Engine.ratToFloat✝ q
• LeanCert.Engine.evalFloat (LeanCert.Core.Expr.var i) ρ = ρ i
• LeanCert.Engine.evalFloat (a.add b) ρ = LeanCert.Engine.evalFloat a ρ + LeanCert.Engine.evalFloat b ρ
• LeanCert.Engine.evalFloat (a.mul b) ρ = LeanCert.Engine.evalFloat a ρ * LeanCert.Engine.evalFloat b ρ
• LeanCert.Engine.evalFloat a.neg ρ = -LeanCert.Engine.evalFloat a ρ
• LeanCert.Engine.evalFloat a.inv ρ = 1.0 / LeanCert.Engine.evalFloat a ρ
• LeanCert.Engine.evalFloat a.exp ρ = (LeanCert.Engine.evalFloat a ρ).exp
• LeanCert.Engine.evalFloat a.log ρ = (LeanCert.Engine.evalFloat a ρ).log
• LeanCert.Engine.evalFloat a.sin ρ = (LeanCert.Engine.evalFloat a ρ).sin
• LeanCert.Engine.evalFloat a.cos ρ = (LeanCert.Engine.evalFloat a ρ).cos
• LeanCert.Engine.evalFloat a.sqrt ρ = (LeanCert.Engine.evalFloat a ρ).sqrt
• LeanCert.Engine.evalFloat a.atan ρ = (LeanCert.Engine.evalFloat a ρ).atan
• LeanCert.Engine.evalFloat a.sinh ρ = ((LeanCert.Engine.evalFloat a ρ).exp - (-LeanCert.Engine.evalFloat a ρ).exp) / 2.0
• LeanCert.Engine.evalFloat a.cosh ρ = ((LeanCert.Engine.evalFloat a ρ).exp + (-LeanCert.Engine.evalFloat a ρ).exp) / 2.0
• LeanCert.Engine.evalFloat a.tanh ρ = ((2.0 * LeanCert.Engine.evalFloat a ρ).exp - 1.0) / ((2.0 * LeanCert.Engine.evalFloat a ρ).exp + 1.0)
• LeanCert.Engine.evalFloat a.arsinh ρ = (LeanCert.Engine.evalFloat a ρ + (LeanCert.Engine.evalFloat a ρ * LeanCert.Engine.evalFloat a ρ + 1.0).sqrt).log
• LeanCert.Engine.evalFloat a.atanh ρ = ((1.0 + LeanCert.Engine.evalFloat a ρ) / (1.0 - LeanCert.Engine.evalFloat a ρ)).log / 2.0
• LeanCert.Engine.evalFloat a.sinc ρ = if (LeanCert.Engine.evalFloat a ρ).abs < 1e-10 then 1.0 else (LeanCert.Engine.evalFloat a ρ).sin / LeanCert.Engine.evalFloat a ρ
• LeanCert.Engine.evalFloat a.erf ρ = LeanCert.Engine.floatErf✝ (LeanCert.Engine.evalFloat a ρ)
• LeanCert.Engine.evalFloat LeanCert.Core.Expr.pi ρ = 3.141592653589793

def LeanCert.Engine.evalFloatList (e : Core.Expr) (vars : List Float) : Float

Evaluate with a list-based environment (for compatibility with Box)

Equations

• LeanCert.Engine.evalFloatList e vars = LeanCert.Engine.evalFloat e fun (i : ℕ) => vars.getD i 0.0

def LeanCert.Engine.evalFloatArray (e : Core.Expr) (vars : Array Float) : Float

Evaluate with an array-based environment (faster for repeated access)

Equations

• LeanCert.Engine.evalFloatArray e vars = LeanCert.Engine.evalFloat e fun (i : ℕ) => vars.getD i 0.0