Interval Evaluation with Real Endpoints

This file implements interval evaluation using IntervalReal (real endpoints), which allows us to support exp in a fully verified way.

Main definitions

• ExprSupportedExt - Extended predicate including exp
• evalIntervalReal - Evaluate an expression over real-endpoint intervals
• evalIntervalReal_correct - Correctness theorem (fully proved)

Design notes

This extends the verified subset from {const, var, add, mul, neg, sin, cos} to also include {exp}. The key insight is that with real endpoints, we can use Real.exp directly and its monotonicity properties.

For numerical computation, users should still use IntervalRat and convert to IntervalReal when they need to reason about exp. This keeps computation efficient while allowing proofs about transcendental functions.

Extended supported expression subset

inductive LeanCert.Engine.ExprSupportedExt : Core.Expr → Prop

Predicate indicating an expression is in the extended verified subset. This includes exp in addition to the base subset. Does NOT support: inv (requires nonzero interval checks)

• const (q : ℚ) : ExprSupportedExt (Core.Expr.const q)
• var (idx : ℕ) : ExprSupportedExt (Core.Expr.var idx)
• add {e₁ e₂ : Core.Expr} : ExprSupportedExt e₁ → ExprSupportedExt e₂ → ExprSupportedExt (e₁.add e₂)
• mul {e₁ e₂ : Core.Expr} : ExprSupportedExt e₁ → ExprSupportedExt e₂ → ExprSupportedExt (e₁.mul e₂)
• neg {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.neg
• sin {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.sin
• cos {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.cos
• exp {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.exp
• atan {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.atan
• arsinh {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.arsinh
• sinh {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.sinh
• cosh {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.cosh
• sqrt {e : Core.Expr} : ExprSupportedExt e → ExprSupportedExt e.sqrt

theorem LeanCert.Engine.ExprSupported.toExt {e : Core.Expr} (h : ExprSupported e) : ExprSupportedExt e

The base supported subset is a subset of the extended one

Real-endpoint interval evaluation

@[reducible, inline]

abbrev LeanCert.Engine.IntervalRealEnv : Type

Variable assignment as real-endpoint intervals

Equations

• LeanCert.Engine.IntervalRealEnv = (ℕ → LeanCert.Core.IntervalReal)

noncomputable def LeanCert.Engine.evalIntervalReal (e : Core.Expr) (ρ : IntervalRealEnv) : Core.IntervalReal

Evaluate an expression over real-endpoint intervals.

For expressions in ExprSupportedExt (const, var, add, mul, neg, sin, cos, exp), this computes correct interval bounds with a fully-verified proof.

For unsupported expressions (inv, log), this returns a trivial interval. Do not call evalIntervalReal on expressions containing inv or log unless you are prepared for unsound results.

Equations

• LeanCert.Engine.evalIntervalReal (LeanCert.Core.Expr.const q) ρ = LeanCert.Core.IntervalReal.singleton ↑q
• LeanCert.Engine.evalIntervalReal (LeanCert.Core.Expr.var idx) ρ = ρ idx
• LeanCert.Engine.evalIntervalReal (e₁.add e₂) ρ = (LeanCert.Engine.evalIntervalReal e₁ ρ).add (LeanCert.Engine.evalIntervalReal e₂ ρ)
• LeanCert.Engine.evalIntervalReal (e₁.mul e₂) ρ = (LeanCert.Engine.evalIntervalReal e₁ ρ).mul (LeanCert.Engine.evalIntervalReal e₂ ρ)
• LeanCert.Engine.evalIntervalReal e_2.neg ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).neg
• LeanCert.Engine.evalIntervalReal e_2.inv ρ = { lo := 0, hi := 0, le := LeanCert.Engine.evalIntervalReal._proof_1 }
• LeanCert.Engine.evalIntervalReal e_2.exp ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).expInterval
• LeanCert.Engine.evalIntervalReal e_2.sin ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).sinInterval
• LeanCert.Engine.evalIntervalReal e_2.cos ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).cosInterval
• LeanCert.Engine.evalIntervalReal e_2.log ρ = { lo := 0, hi := 0, le := LeanCert.Engine.evalIntervalReal._proof_1 }
• LeanCert.Engine.evalIntervalReal e_2.atan ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).atanInterval
• LeanCert.Engine.evalIntervalReal e_2.arsinh ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).arsinhInterval
• LeanCert.Engine.evalIntervalReal e_2.atanh ρ = { lo := 0, hi := 0, le := LeanCert.Engine.evalIntervalReal._proof_1 }
• LeanCert.Engine.evalIntervalReal e_2.sinc ρ = { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalReal._proof_2 }
• LeanCert.Engine.evalIntervalReal e_2.erf ρ = { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalReal._proof_2 }
• LeanCert.Engine.evalIntervalReal e_2.sinh ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).sinhInterval
• LeanCert.Engine.evalIntervalReal e_2.cosh ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).coshInterval
• LeanCert.Engine.evalIntervalReal e_2.tanh ρ = { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalReal._proof_2 }
• LeanCert.Engine.evalIntervalReal e_2.sqrt ρ = (LeanCert.Engine.evalIntervalReal e_2 ρ).sqrtInterval
• LeanCert.Engine.evalIntervalReal LeanCert.Core.Expr.pi ρ = { lo := Real.pi, hi := Real.pi, le := ⋯ }

def LeanCert.Engine.envMemReal (ρ_real : ℕ → ℝ) (ρ_int : IntervalRealEnv) : Prop

A real environment is contained in a real-interval environment

Equations

• LeanCert.Engine.envMemReal ρ_real ρ_int = ∀ (i : ℕ), ρ_real i ∈ ρ_int i

Membership lemmas for IntervalReal operations

theorem LeanCert.Engine.IntervalReal.mem_singleton' (r : ℝ) : r ∈ Core.IntervalReal.singleton r

Membership in singleton

theorem LeanCert.Engine.IntervalReal.mem_singleton_rat (q : ℚ) : ↑q ∈ Core.IntervalReal.singleton ↑q

Membership for rational casts in singleton

theorem LeanCert.Engine.IntervalReal.mem_mul' {x y : ℝ} {I J : Core.IntervalReal} (hx : x ∈ I) (hy : y ∈ J) : x * y ∈ I.mul J

FTIA for multiplication on IntervalReal

Main correctness theorem

theorem LeanCert.Engine.evalIntervalReal_correct (e : Core.Expr) (hsupp : ExprSupportedExt e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalRealEnv) (hρ : envMemReal ρ_real ρ_int) : Core.Expr.eval ρ_real e ∈ evalIntervalReal e ρ_int

Fundamental correctness theorem for real-endpoint interval evaluation. If variables are in their intervals, the expression evaluates to a value in the computed interval.

This theorem is FULLY PROVED (no sorry, no axioms) for ExprSupportedExt expressions. This includes exp!

Convenience functions

noncomputable def LeanCert.Engine.evalIntervalReal1 (e : Core.Expr) (I : Core.IntervalReal) : Core.IntervalReal

Evaluate an expression with a single variable over a real-endpoint interval

Equations

• LeanCert.Engine.evalIntervalReal1 e I = LeanCert.Engine.evalIntervalReal e fun (x : ℕ) => I

theorem LeanCert.Engine.evalIntervalReal1_correct (e : Core.Expr) (hsupp : ExprSupportedExt e) (x : ℝ) (I : Core.IntervalReal) (hx : x ∈ I) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ evalIntervalReal1 e I

Correctness for single-variable evaluation

Conversion from rational to real interval environment

def LeanCert.Engine.toIntervalRealEnv (ρ : IntervalEnv) : IntervalRealEnv

Convert a rational interval environment to a real one

Equations

• LeanCert.Engine.toIntervalRealEnv ρ i = LeanCert.Core.IntervalReal.ofRat (ρ i)

theorem LeanCert.Engine.mem_toIntervalRealEnv {x : ℝ} {ρ : IntervalEnv} {i : ℕ} (hx : x ∈ ρ i) : x ∈ toIntervalRealEnv ρ i

Membership is preserved under conversion

Tactic-facing lemmas for interval bounds (extended subset with exp)

theorem LeanCert.Engine.exprExt_le_of_interval_hi (e : Core.Expr) (hsupp : ExprSupportedExt e) (I : Core.IntervalReal) (c : ℝ) (hhi : (evalIntervalReal1 e I).hi ≤ c) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ c

Upper bound lemma for extended subset (includes exp). FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.exprExt_ge_of_interval_lo (e : Core.Expr) (hsupp : ExprSupportedExt e) (I : Core.IntervalReal) (c : ℝ) (hlo : c ≤ (evalIntervalReal1 e I).lo) (x : ℝ) : x ∈ I → c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Lower bound lemma for extended subset (includes exp). FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.exprExt_lt_of_interval_hi_lt (e : Core.Expr) (hsupp : ExprSupportedExt e) (I : Core.IntervalReal) (c : ℝ) (hhi : (evalIntervalReal1 e I).hi < c) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < c

Strict upper bound for extended subset. FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.exprExt_gt_of_interval_lo_gt (e : Core.Expr) (hsupp : ExprSupportedExt e) (I : Core.IntervalReal) (c : ℝ) (hlo : c < (evalIntervalReal1 e I).lo) (x : ℝ) : x ∈ I → c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Strict lower bound for extended subset. FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.exprExt_le_of_mem_interval (e : Core.Expr) (hsupp : ExprSupportedExt e) (I : Core.IntervalReal) (c x : ℝ) (hx : x ∈ I) (hhi : (evalIntervalReal1 e I).hi ≤ c) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ c

Point variant for extended subset.

theorem LeanCert.Engine.exprExt_ge_of_mem_interval (e : Core.Expr) (hsupp : ExprSupportedExt e) (I : Core.IntervalReal) (c x : ℝ) (hx : x ∈ I) (hlo : c ≤ (evalIntervalReal1 e I).lo) : c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Point variant for extended subset.