Computable Interval Evaluation

This file implements the computable interval evaluator for LeanCert.Core.Expr. Given an expression and intervals for its variables, we compute an interval guaranteed to contain all possible values.

Main definitions

• IntervalEnv - Variable assignment as intervals
• EvalConfig - Configuration for evaluation parameters (Taylor depth)
• evalIntervalCore - Computable interval evaluator for core expressions
• evalIntervalCore_correct - Correctness theorem for core evaluation

Design notes

This evaluator is COMPUTABLE, allowing use of native_decide for bound checking in tactics. The transcendental functions (exp, sin, cos) use Taylor series with configurable depth for precision control.

For inv: computes bounds using invInterval, but correctness is not covered by evalIntervalCore_correct. Use evalInterval? for inv.

Interval bounds for transcendental functions

def LeanCert.Engine.sinInterval (_I : Core.IntervalRat) : Core.IntervalRat

Simple interval bound for sin. Since |sin x| ≤ 1 for all x, we use the global bound [-1, 1]. This is sound but not tight.

Equations

• LeanCert.Engine.sinInterval _I = { lo := -1, hi := 1, le := LeanCert.Engine.sinInterval._proof_1 }

theorem LeanCert.Engine.mem_sinInterval {x : ℝ} {I : Core.IntervalRat} (_hx : x ∈ I) : Real.sin x ∈ sinInterval I

Correctness of sin interval: sin x ∈ [-1, 1] for all x

def LeanCert.Engine.cosInterval (_I : Core.IntervalRat) : Core.IntervalRat

Simple interval bound for cos. Since |cos x| ≤ 1 for all x, we use the global bound [-1, 1]. This is sound but not tight.

Equations

• LeanCert.Engine.cosInterval _I = { lo := -1, hi := 1, le := LeanCert.Engine.sinInterval._proof_1 }

theorem LeanCert.Engine.mem_cosInterval {x : ℝ} {I : Core.IntervalRat} (_hx : x ∈ I) : Real.cos x ∈ cosInterval I

Correctness of cos interval: cos x ∈ [-1, 1] for all x

def LeanCert.Engine.atanInterval (_I : Core.IntervalRat) : Core.IntervalRat

Simple interval bound for atan. Since atan x ∈ (-π/2, π/2) for all x, we use the global bound [-2, 2]. This is sound but not tight (π/2 ≈ 1.57).

Equations

• LeanCert.Engine.atanInterval _I = { lo := -2, hi := 2, le := LeanCert.Engine.atanInterval._proof_1 }

theorem LeanCert.Engine.mem_atanInterval {x : ℝ} {I : Core.IntervalRat} (_hx : x ∈ I) : Real.arctan x ∈ atanInterval I

Correctness of atan interval: arctan x ∈ [-2, 2] for all x

def LeanCert.Engine.erfInterval (I : Core.IntervalRat) (taylorDepth : ℕ := 15) : Core.IntervalRat

Interval bound for erf using computable Taylor series. erf(x) = (2/√π) * ∫₀ˣ exp(-t²) dt, strictly monotone increasing. This computes tight bounds using verified Taylor series.

Equations

• LeanCert.Engine.erfInterval I taylorDepth = I.erfComputable taylorDepth

theorem LeanCert.Engine.Real.strictMono_erf : StrictMono Core.Real.erf

erf is strictly monotone increasing. Proof: erf'(x) = (2/√π) * exp(-x²) > 0 for all x.

We use that for a < b, the integral ∫_{a}^{b} exp(-t²) dt > 0 since the integrand is strictly positive.

theorem LeanCert.Engine.mem_erfPointComputable (q : ℚ) (n : ℕ) : Core.Real.erf ↑q ∈ Core.IntervalRat.erfPointComputable q n

Correctness of erfPointComputable. The enclosure is sign-aware and uses monotonicity of erf with erf(0)=0.

theorem LeanCert.Engine.mem_erfInterval {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (n : ℕ := 15) : Core.Real.erf x ∈ erfInterval I n

Correctness of erf interval using monotonicity and endpoint evaluation.

Since erf is strictly monotone increasing:

• For x ∈ [I.lo, I.hi], we have erf(I.lo) ≤ erf(x) ≤ erf(I.hi)
• erfPointComputable(I.lo) contains erf(I.lo)
• erfPointComputable(I.hi) contains erf(I.hi)
• hull of these intervals contains [erf(I.lo), erf(I.hi)]
• Therefore erf(x) ∈ hull(...) ∩ [-1, 1]

def LeanCert.Engine.arsinhInterval (I : Core.IntervalRat) : Core.IntervalRat

Simple interval bound for arsinh. arsinh is unbounded, so we use a very rough linear bound. We use max(|lo|, |hi|) + 1 as a safe bound that always works.

Equations

• LeanCert.Engine.arsinhInterval I = { lo := -(max |I.lo| |I.hi| + 1), hi := max |I.lo| |I.hi| + 1, le := ⋯ }

theorem LeanCert.Engine.mem_arsinhInterval {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : Real.arsinh x ∈ arsinhInterval I

Correctness of arsinh interval. Uses the bound |arsinh x| ≤ |x| for all x (from IntervalRealEndpoints).

noncomputable def LeanCert.Engine.atanhInterval (I : Core.IntervalRat) : Core.IntervalRat

Interval bound for atanh. atanh is defined for (-1, 1). If interval is within this range, we compute tight bounds using monotonicity. Otherwise returns default.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanCert.Engine.mem_atanhInterval {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hlo : -1 < I.lo) (hhi : I.hi < 1) : Core.Real.atanh x ∈ atanhInterval I

Correctness of atanh interval: when x ∈ I and I ⊂ (-1, 1), atanh(x) ∈ atanhInterval I.

def LeanCert.Engine.tanhInterval (_I : Core.IntervalRat) : Core.IntervalRat

Tight interval bound for tanh. Since tanh(x) ∈ (-1, 1) for all x ∈ ℝ, we use the global bound [-1, 1]. This avoids the interval explosion that occurs when desugaring to exp.

Equations

• LeanCert.Engine.tanhInterval _I = { lo := -1, hi := 1, le := LeanCert.Engine.sinInterval._proof_1 }

theorem LeanCert.Engine.mem_tanhInterval {x : ℝ} {I : Core.IntervalRat} (_hx : x ∈ I) : Real.tanh x ∈ tanhInterval I

Correctness of tanh interval: tanh x ∈ [-1, 1] for all x

def LeanCert.Engine.piInterval : Core.IntervalRat

Interval enclosure for π. Uses tight bounds from Mathlib's pi_gt_d20 and pi_lt_d20 which give 20 decimal digits. 3.14159265358979323846 < π < 3.14159265358979323847

Equations

• LeanCert.Engine.piInterval = { lo := 31415926535897932 / 10000000000000000, hi := 31415926535897933 / 10000000000000000, le := LeanCert.Engine.piInterval._proof_1 }

theorem LeanCert.Engine.mem_piInterval : Real.pi ∈ piInterval

Correctness of pi interval: Real.pi ∈ piInterval

def LeanCert.Engine.sinhInterval (I : Core.IntervalRat) (taylorDepth : ℕ := 10) : Core.IntervalRat

Interval bound for sinh using computable Taylor series for exp. sinh(x) = (exp(x) - exp(-x)) / 2, and sinh is strictly monotonic. This computes tight bounds using the verified exp implementation.

Equations

• LeanCert.Engine.sinhInterval I taylorDepth = I.sinhComputable taylorDepth

def LeanCert.Engine.coshInterval (I : Core.IntervalRat) (taylorDepth : ℕ := 10) : Core.IntervalRat

Interval bound for cosh using computable Taylor series for exp. cosh(x) = (exp(x) + exp(-x)) / 2, with minimum 1 at x = 0. This computes tight bounds using the verified exp implementation.

Equations

• LeanCert.Engine.coshInterval I taylorDepth = I.coshComputable taylorDepth

Interval inverse

def LeanCert.Engine.invWideBound : ℚ

Wide bound constant for when inverse is undefined (denominator contains 0)

Equations

• LeanCert.Engine.invWideBound = 10 ^ 30

def LeanCert.Engine.invInterval (I : Core.IntervalRat) : Core.IntervalRat

Computable interval inverse. For [a,b] with a > 0: returns [1/b, 1/a] (1/x is decreasing on positive reals) For [a,b] with b < 0: returns [1/b, 1/a] (1/x is decreasing on negative reals) For intervals containing 0: returns very wide bounds [-M, M] as a sound default

Equations

• One or more equations did not get rendered due to their size.

theorem LeanCert.Engine.mem_invInterval_pos {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hpos : I.lo > 0) : x⁻¹ ∈ invInterval I

Correctness of invInterval when denominator interval is positive. For x ∈ [a,b] with a > 0, we have 1/x ∈ [1/b, 1/a]

theorem LeanCert.Engine.mem_invInterval_neg {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hneg : I.hi < 0) : x⁻¹ ∈ invInterval I

Correctness of invInterval when denominator interval is negative. For x ∈ [a,b] with b < 0, we have 1/x ∈ [1/b, 1/a]

theorem LeanCert.Engine.mem_invInterval_wide {x : ℝ} {I : Core.IntervalRat} (_hx : x ∈ I) (hlo : ¬I.lo > 0) (hhi : ¬I.hi < 0) (hbnd : |x⁻¹| ≤ ↑invWideBound) : x⁻¹ ∈ invInterval I

Correctness of invInterval when denominator interval contains zero. Requires a bound on |x⁻¹| to be provable, since x can be arbitrarily close to 0.

theorem LeanCert.Engine.mem_invInterval {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hbnd : |x⁻¹| ≤ ↑invWideBound) : x⁻¹ ∈ invInterval I

Main correctness theorem for invInterval. Fully proved for intervals bounded away from zero. For intervals containing zero, requires a bound on |x⁻¹|.

theorem LeanCert.Engine.mem_invInterval_nonzero {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hnonzero : I.lo > 0 ∨ I.hi < 0) : x⁻¹ ∈ invInterval I

Correctness of invInterval for intervals bounded away from zero (no extra hypothesis needed)

Core interval evaluation (computable)

@[reducible, inline]

abbrev LeanCert.Engine.IntervalEnv : Type

Variable assignment as intervals

Equations

• LeanCert.Engine.IntervalEnv = (ℕ → LeanCert.Core.IntervalRat)

structure LeanCert.Engine.EvalConfig : Type

Configuration for interval evaluation parameters. This allows certificates to specify the required precision.

• taylorDepth : ℕ

  Number of Taylor series terms for transcendental functions

instance LeanCert.Engine.instReprEvalConfig : Repr EvalConfig

Equations

• LeanCert.Engine.instReprEvalConfig = { reprPrec := LeanCert.Engine.instReprEvalConfig.repr }

def LeanCert.Engine.instReprEvalConfig.repr : EvalConfig → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Engine.instDecidableEqEvalConfig : DecidableEq EvalConfig

Equations

• LeanCert.Engine.instDecidableEqEvalConfig = LeanCert.Engine.instDecidableEqEvalConfig.decEq

def LeanCert.Engine.instDecidableEqEvalConfig.decEq (x✝ x✝¹ : EvalConfig) : Decidable (x✝ = x✝¹)

Equations

• LeanCert.Engine.instDecidableEqEvalConfig.decEq { taylorDepth := a } { taylorDepth := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance LeanCert.Engine.instInhabitedEvalConfig : Inhabited EvalConfig

Default evaluation configuration with 10 Taylor terms

Equations

• LeanCert.Engine.instInhabitedEvalConfig = { default := { } }

def LeanCert.Engine.evalIntervalCore (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig := { }) : Core.IntervalRat

Computable interval evaluator for core expressions with configurable depth.

For expressions in ExprSupportedCore, this computes correct interval bounds with a fully-verified proof (given domain validity conditions).

For inv: computes bounds using invInterval, but correctness is not covered by evalIntervalCore_correct. Use evalInterval? for inv.

For log: uses logComputable with Taylor series. Correctness requires that the argument interval is positive (see evalDomainValid).

This evaluator is COMPUTABLE, allowing use of native_decide for bound checking in tactics. The transcendental functions (exp, sin, cos, log) use Taylor series with configurable depth for precision control.

Equations

• LeanCert.Engine.evalIntervalCore (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Core.IntervalRat.singleton q
• LeanCert.Engine.evalIntervalCore (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
• LeanCert.Engine.evalIntervalCore (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalIntervalCore e₁ ρ cfg).add (LeanCert.Engine.evalIntervalCore e₂ ρ cfg)
• LeanCert.Engine.evalIntervalCore (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalIntervalCore e₁ ρ cfg).mul (LeanCert.Engine.evalIntervalCore e₂ ρ cfg)
• LeanCert.Engine.evalIntervalCore e_2.neg ρ cfg = (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).neg
• LeanCert.Engine.evalIntervalCore e_2.inv ρ cfg = LeanCert.Engine.invInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCore e_2.exp ρ cfg = (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).expComputable cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.sin ρ cfg = (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).sinComputableReduced cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.cos ρ cfg = (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).cosComputableReduced cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.log ρ cfg = (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).logComputable cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.atan ρ cfg = LeanCert.Engine.atanInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCore e_2.arsinh ρ cfg = LeanCert.Engine.arsinhInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCore e_2.atanh ρ cfg = default
• LeanCert.Engine.evalIntervalCore e_2.sinc ρ cfg = { lo := -1, hi := 1, le := LeanCert.Engine.sinInterval._proof_1 }
• LeanCert.Engine.evalIntervalCore e_2.erf ρ cfg = LeanCert.Engine.erfInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg) cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.sinh ρ cfg = LeanCert.Engine.sinhInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg) cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.cosh ρ cfg = LeanCert.Engine.coshInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg) cfg.taylorDepth
• LeanCert.Engine.evalIntervalCore e_2.tanh ρ cfg = LeanCert.Engine.tanhInterval (LeanCert.Engine.evalIntervalCore e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCore e_2.sqrt ρ cfg = (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).sqrtIntervalTightPrec
• LeanCert.Engine.evalIntervalCore LeanCert.Core.Expr.pi ρ cfg = LeanCert.Engine.piInterval

def LeanCert.Engine.evalIntervalCoreWithDiv (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig := { }) : Core.IntervalRat

Computable interval evaluator with division support.

This extends evalIntervalCore to handle inv/div by computing interval inverse when the denominator is bounded away from zero. Returns wide bounds when the denominator interval contains zero.

NOTE: This is less rigorous than evalInterval? because it doesn't fail when 0 is in the denominator range - it just returns wide bounds. This is useful for applications where we want to continue safely even when the analysis is imprecise.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.evalIntervalCoreWithDiv (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Core.IntervalRat.singleton q
• LeanCert.Engine.evalIntervalCoreWithDiv (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
• LeanCert.Engine.evalIntervalCoreWithDiv (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e₁ ρ cfg).add (LeanCert.Engine.evalIntervalCoreWithDiv e₂ ρ cfg)
• LeanCert.Engine.evalIntervalCoreWithDiv (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e₁ ρ cfg).mul (LeanCert.Engine.evalIntervalCoreWithDiv e₂ ρ cfg)
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.neg ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg).neg
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.exp ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg).expComputable cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.sin ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg).sinComputableReduced cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.cos ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg).cosComputableReduced cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.log ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg).logComputable cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.atan ρ cfg = LeanCert.Engine.atanInterval (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.arsinh ρ cfg = LeanCert.Engine.arsinhInterval (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.atanh ρ cfg = { lo := -100, hi := 100, le := LeanCert.Engine.evalIntervalCoreWithDiv._proof_3 }
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.sinc ρ cfg = { lo := -1, hi := 1, le := LeanCert.Engine.sinInterval._proof_1 }
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.erf ρ cfg = LeanCert.Engine.erfInterval (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg) cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.sinh ρ cfg = LeanCert.Engine.sinhInterval (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg) cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.cosh ρ cfg = LeanCert.Engine.coshInterval (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg) cfg.taylorDepth
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.tanh ρ cfg = LeanCert.Engine.tanhInterval (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg)
• LeanCert.Engine.evalIntervalCoreWithDiv e_2.sqrt ρ cfg = (LeanCert.Engine.evalIntervalCoreWithDiv e_2 ρ cfg).sqrtIntervalTightPrec
• LeanCert.Engine.evalIntervalCoreWithDiv LeanCert.Core.Expr.pi ρ cfg = LeanCert.Engine.piInterval

def LeanCert.Engine.envMem (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) : Prop

A real environment is contained in an interval environment

Equations

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

def LeanCert.Engine.evalDomainValid (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig := { }) : Prop

Domain validity predicate for expressions with domain restrictions.

For log: requires the argument interval to be strictly positive. This ensures that logComputable returns correct bounds.

For other expressions: always true (no domain restrictions).

Equations

• LeanCert.Engine.evalDomainValid (LeanCert.Core.Expr.const q) ρ cfg = True
• LeanCert.Engine.evalDomainValid (LeanCert.Core.Expr.var idx) ρ cfg = True
• LeanCert.Engine.evalDomainValid (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalDomainValid e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValid e₂ ρ cfg)
• LeanCert.Engine.evalDomainValid (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalDomainValid e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValid e₂ ρ cfg)
• LeanCert.Engine.evalDomainValid e_2.neg ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.inv ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.exp ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.sin ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.cos ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.log ρ cfg = (LeanCert.Engine.evalDomainValid e_2 ρ cfg ∧ (LeanCert.Engine.evalIntervalCore e_2 ρ cfg).lo > 0)
• LeanCert.Engine.evalDomainValid e_2.atan ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.arsinh ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.atanh ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.sinc ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.erf ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.sinh ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.cosh ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.tanh ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid e_2.sqrt ρ cfg = LeanCert.Engine.evalDomainValid e_2 ρ cfg
• LeanCert.Engine.evalDomainValid LeanCert.Core.Expr.pi ρ cfg = True

def LeanCert.Engine.evalDomainValid1 (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : Prop

Single-variable domain validity

Equations

• LeanCert.Engine.evalDomainValid1 e I cfg = LeanCert.Engine.evalDomainValid e (fun (x : ℕ) => I) cfg

def LeanCert.Engine.checkDomainValid (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig := { }) : Bool

Computable (decidable) check for domain validity

Equations

• LeanCert.Engine.checkDomainValid (LeanCert.Core.Expr.const q) ρ cfg = true
• LeanCert.Engine.checkDomainValid (LeanCert.Core.Expr.var idx) ρ cfg = true
• LeanCert.Engine.checkDomainValid (e₁.add e₂) ρ cfg = (LeanCert.Engine.checkDomainValid e₁ ρ cfg && LeanCert.Engine.checkDomainValid e₂ ρ cfg)
• LeanCert.Engine.checkDomainValid (e₁.mul e₂) ρ cfg = (LeanCert.Engine.checkDomainValid e₁ ρ cfg && LeanCert.Engine.checkDomainValid e₂ ρ cfg)
• LeanCert.Engine.checkDomainValid e_2.neg ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.inv ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.exp ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.sin ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.cos ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.log ρ cfg = (LeanCert.Engine.checkDomainValid e_2 ρ cfg && decide ((LeanCert.Engine.evalIntervalCore e_2 ρ cfg).lo > 0))
• LeanCert.Engine.checkDomainValid e_2.atan ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.arsinh ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.atanh ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.sinc ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.erf ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.sinh ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.cosh ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.tanh ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid e_2.sqrt ρ cfg = LeanCert.Engine.checkDomainValid e_2 ρ cfg
• LeanCert.Engine.checkDomainValid LeanCert.Core.Expr.pi ρ cfg = true

def LeanCert.Engine.checkDomainValid1 (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : Bool

Single-variable domain check

Equations

• LeanCert.Engine.checkDomainValid1 e I cfg = LeanCert.Engine.checkDomainValid e (fun (x : ℕ) => I) cfg

theorem LeanCert.Engine.checkDomainValid_correct (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig) (h : checkDomainValid e ρ cfg = true) : evalDomainValid e ρ cfg

checkDomainValid = true implies evalDomainValid

theorem LeanCert.Engine.checkDomainValid1_correct (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig) (h : checkDomainValid1 e I cfg = true) : evalDomainValid1 e I cfg

checkDomainValid1 = true implies evalDomainValid1

theorem LeanCert.Engine.evalDomainValid_iff_checkDomainValid (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig) : evalDomainValid e ρ cfg ↔ checkDomainValid e ρ cfg = true

evalDomainValid is equivalent to checkDomainValid = true

instance LeanCert.Engine.decidableEvalDomainValid (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig) : Decidable (evalDomainValid e ρ cfg)

Decidability instance for domain validity

Equations

• LeanCert.Engine.decidableEvalDomainValid e ρ cfg = decidable_of_iff' (LeanCert.Engine.checkDomainValid e ρ cfg = true) ⋯

instance LeanCert.Engine.decidableEvalDomainValid1 (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig) : Decidable (evalDomainValid1 e I cfg)

Decidability instance for single-variable domain validity

Equations

• LeanCert.Engine.decidableEvalDomainValid1 e I cfg = LeanCert.Engine.decidableEvalDomainValid e (fun (x : ℕ) => I) cfg

theorem LeanCert.Engine.ExprSupported.domainValid {e : Core.Expr} (hsupp : ExprSupported e) (ρ : IntervalEnv) (cfg : EvalConfig) : evalDomainValid e ρ cfg

ExprSupported expressions (which don't include log) always have valid domains. This is because only log has domain restrictions (positive argument).

theorem LeanCert.Engine.exprSupported_domainValid1 {e : Core.Expr} (hsupp : ExprSupported e) (I : Core.IntervalRat) (cfg : EvalConfig) : evalDomainValid1 e I cfg

Single-variable version of domainValid for ExprSupported

theorem LeanCert.Engine.evalIntervalCore_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) (cfg : EvalConfig := { }) (hdom : evalDomainValid e ρ_int cfg) : Core.Expr.eval ρ_real e ∈ evalIntervalCore e ρ_int cfg

Fundamental correctness theorem for core evaluation.

This theorem is FULLY PROVED for core expressions (no sorry, no axioms). The hsupp hypothesis ensures we only consider expressions in the computable verified subset. The hdom hypothesis ensures domain validity (e.g., log arguments are positive). Works for any Taylor depth.

Convenience functions

def LeanCert.Engine.evalIntervalCore1 (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : Core.IntervalRat

Computable single-variable evaluation for core expressions

Equations

• LeanCert.Engine.evalIntervalCore1 e I cfg = LeanCert.Engine.evalIntervalCore e (fun (x : ℕ) => I) cfg

theorem LeanCert.Engine.evalIntervalCore1_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ evalIntervalCore1 e I cfg

Correctness for single-variable core evaluation

Smart constructors for supported expressions

def LeanCert.Engine.mkConst (q : ℚ) : { e : Core.Expr // ExprSupported e }

Build a constant expression (always supported)

Equations

• LeanCert.Engine.mkConst q = ⟨LeanCert.Core.Expr.const q, ⋯⟩

def LeanCert.Engine.mkVar (idx : ℕ) : { e : Core.Expr // ExprSupported e }

Build a variable expression (always supported)

Equations

• LeanCert.Engine.mkVar idx = ⟨LeanCert.Core.Expr.var idx, ⋯⟩

def LeanCert.Engine.mkAdd (e₁ e₂ : { e : Core.Expr // ExprSupported e }) : { e : Core.Expr // ExprSupported e }

Build an addition (supported if both operands are supported)

Equations

• LeanCert.Engine.mkAdd e₁ e₂ = ⟨(↑e₁).add ↑e₂, ⋯⟩

def LeanCert.Engine.mkMul (e₁ e₂ : { e : Core.Expr // ExprSupported e }) : { e : Core.Expr // ExprSupported e }

Build a multiplication (supported if both operands are supported)

Equations

• LeanCert.Engine.mkMul e₁ e₂ = ⟨(↑e₁).mul ↑e₂, ⋯⟩

def LeanCert.Engine.mkNeg (e : { e : Core.Expr // ExprSupported e }) : { e : Core.Expr // ExprSupported e }

Build a negation (supported if operand is supported)

Equations

• LeanCert.Engine.mkNeg e = ⟨(↑e).neg, ⋯⟩

def LeanCert.Engine.mkSin (e : { e : Core.Expr // ExprSupported e }) : { e : Core.Expr // ExprSupported e }

Build a sin (supported if operand is supported)

Equations

• LeanCert.Engine.mkSin e = ⟨(↑e).sin, ⋯⟩

def LeanCert.Engine.mkCos (e : { e : Core.Expr // ExprSupported e }) : { e : Core.Expr // ExprSupported e }

Build a cos (supported if operand is supported)

Equations

• LeanCert.Engine.mkCos e = ⟨(↑e).cos, ⋯⟩

def LeanCert.Engine.mkExp (e : { e : Core.Expr // ExprSupported e }) : { e : Core.Expr // ExprSupported e }

Build an exp (supported if operand is supported)

Equations

• LeanCert.Engine.mkExp e = ⟨(↑e).exp, ⋯⟩