Extended Interval Arithmetic

This file implements Extended Interval Arithmetic, which handles singularities by returning a disjoint union of intervals instead of a single interval.

Motivation

Standard interval arithmetic returns overly conservative bounds when evaluating expressions with singularities. For example, 1/[-1, 1] returns (-∞, ∞) as a single interval, losing all useful information.

Extended interval arithmetic instead returns (-∞, -1] ∪ [1, ∞), preserving the fact that the result is bounded away from zero.

Main definitions

• ExtendedInterval - A union of disjoint rational intervals
• invExtended - Extended inversion that splits at zero crossings
• evalExtended - Recursive evaluator returning extended intervals
• ExtendedInterval.hull - Collapse to a single interval (convex hull)

Main theorems

• mem_invExtended - Soundness of extended inversion
• evalExtended_correct_core - Soundness of the extended evaluator

Design notes

The largeBound parameter represents "infinity" for practical computation. Using 10^30 is sufficient for most numerical applications while keeping arithmetic tractable.

The Extended Interval Data Structure

structure LeanCert.Engine.ExtendedInterval : Type

Extended Interval: A union of rational intervals. Used to handle singularities (e.g., 1/[-1, 1] becomes (-∞, -1] ∪ [1, ∞)).

Design choices:

• Empty list represents the empty set (e.g., sqrt(-1) for strict domains)
• Intervals in the list may overlap (we don't enforce disjointness for simplicity)
• Operations conservatively handle all parts

• parts : List Core.IntervalRat

  The intervals making up this extended interval. Empty list means the empty set.

instance LeanCert.Engine.instReprExtendedInterval : Repr ExtendedInterval

Equations

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

def LeanCert.Engine.instReprExtendedInterval.repr : ExtendedInterval → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.instInhabitedExtendedInterval : Inhabited ExtendedInterval

Equations

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

def LeanCert.Engine.instInhabitedExtendedInterval.default : ExtendedInterval

Equations

• LeanCert.Engine.instInhabitedExtendedInterval.default = { parts := default }

def LeanCert.Engine.ExtendedInterval.singleton (I : Core.IntervalRat) : ExtendedInterval

Construct from a single interval

Equations

• LeanCert.Engine.ExtendedInterval.singleton I = { parts := [I] }

def LeanCert.Engine.ExtendedInterval.empty : ExtendedInterval

The empty set (for undefined operations)

Equations

• LeanCert.Engine.ExtendedInterval.empty = { parts := [] }

def LeanCert.Engine.ExtendedInterval.whole (large_bound : ℚ) (h : 0 ≤ large_bound) : ExtendedInterval

The entire real line (represented by a very wide interval)

Equations

• LeanCert.Engine.ExtendedInterval.whole large_bound h = LeanCert.Engine.ExtendedInterval.singleton { lo := -large_bound, hi := large_bound, le := ⋯ }

def LeanCert.Engine.ExtendedInterval.isEmpty (E : ExtendedInterval) : Bool

Check if an extended interval is empty

Equations

• E.isEmpty = E.parts.isEmpty

def LeanCert.Engine.ExtendedInterval.numParts (E : ExtendedInterval) : ℕ

Number of parts in the extended interval

Equations

• E.numParts = E.parts.length

def LeanCert.Engine.ExtendedInterval.hull? (E : ExtendedInterval) : Option Core.IntervalRat

Compute the convex hull: merge all parts into a single interval. Returns none if the extended interval is empty.

Equations

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

def LeanCert.Engine.ExtendedInterval.hull (E : ExtendedInterval) : Core.IntervalRat

Compute the convex hull with a default for empty intervals

Equations

• E.hull = E.hull?.getD default

def LeanCert.Engine.ExtendedInterval.mem (x : ℝ) (E : ExtendedInterval) : Prop

Membership: x is in the extended interval if it's in any part

Equations

• LeanCert.Engine.ExtendedInterval.mem x E = ∃ I ∈ E.parts, x ∈ I

instance LeanCert.Engine.ExtendedInterval.instMembershipReal : Membership ℝ ExtendedInterval

Equations

• LeanCert.Engine.ExtendedInterval.instMembershipReal = { mem := fun (E : LeanCert.Engine.ExtendedInterval) (x : ℝ) => LeanCert.Engine.ExtendedInterval.mem x E }

theorem LeanCert.Engine.ExtendedInterval.mem_def {x : ℝ} {E : ExtendedInterval} : x ∈ E ↔ ∃ I ∈ E.parts, x ∈ I

theorem LeanCert.Engine.ExtendedInterval.mem_singleton {x : ℝ} {I : Core.IntervalRat} : x ∈ singleton I ↔ x ∈ I

theorem LeanCert.Engine.ExtendedInterval.foldl_contains_head (t : List Core.IntervalRat) (h : Core.IntervalRat) : have result := List.foldl (fun (acc I : Core.IntervalRat) => { lo := min acc.lo I.lo, hi := max acc.hi I.hi, le := ⋯ }) h t; result.lo ≤ h.lo ∧ h.hi ≤ result.hi

Helper: the foldl operation maintains the property that the accumulated interval has lo ≤ head.lo and hi ≥ head.hi

theorem LeanCert.Engine.ExtendedInterval.foldl_contains_tail (t : List Core.IntervalRat) (h I : Core.IntervalRat) (hI : I ∈ t) : have result := List.foldl (fun (acc J : Core.IntervalRat) => { lo := min acc.lo J.lo, hi := max acc.hi J.hi, le := ⋯ }) h t; result.lo ≤ I.lo ∧ I.hi ≤ result.hi

Helper: the foldl operation maintains the property that the accumulated interval contains any element from the tail

theorem LeanCert.Engine.ExtendedInterval.mem_hull {x : ℝ} {E : ExtendedInterval} (hx : x ∈ E) (hne : E.parts ≠ []) : x ∈ E.hull

If x is in some part, then x is in the hull. The proof follows from the fact that hull.lo = min of all lo's ≤ I.lo ≤ x and x ≤ I.hi ≤ max of all hi's = hull.hi.

Extended Inversion

def LeanCert.Engine.defaultLargeBound : ℚ

The default "large bound" representing infinity for extended arithmetic. Using 10^30 is sufficient for most numerical applications.

Equations

• LeanCert.Engine.defaultLargeBound = 10 ^ 30

theorem LeanCert.Engine.defaultLargeBound_pos : 0 < defaultLargeBound

Helper: defaultLargeBound is positive

def LeanCert.Engine.invExtended (I : Core.IntervalRat) (large_bound : ℚ := defaultLargeBound) : ExtendedInterval

Extended inversion: handles 1/I when I may contain zero.

Cases:

1. I strictly positive → standard inversion [1/hi, 1/lo]
2. I strictly negative → standard inversion [1/hi, 1/lo]
3. I straddles zero → split into two parts: (-∞, 1/lo] ∪ [1/hi, ∞)
4. I = [0, b] with b > 0 → [1/b, ∞)
5. I = [a, 0] with a < 0 → (-∞, 1/a]
6. I = [0, 0] → empty (1/0 is undefined)

NOTE: Uses large_bound (default 10^30) to represent ±∞. For inputs with |lo|, |hi| ≥ 10^-30, the bounds are guaranteed valid.

Equations

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

theorem LeanCert.Engine.mem_invExtended {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hxne : x ≠ 0) (large_bound : ℚ := defaultLargeBound) (hlb : |x⁻¹| ≤ ↑large_bound) : x⁻¹ ∈ invExtended I large_bound

Soundness of extended inversion: if x ∈ I and x ≠ 0, then 1/x ∈ invExtended I.

The hypothesis hlb : |x⁻¹| ≤ large_bound ensures that 1/x fits within the finite bounds. This is the key assumption that makes extended inversion sound - without it, 1/x could be arbitrarily large for x close to 0.

NOTE: This theorem has remaining sorries because the invExtended function itself has design assumption sorries for interval validity when constructing intervals near zero. The membership logic is correct modulo these construction assumptions.

Lifting Operations to Extended Intervals

def LeanCert.Engine.liftUnary (op : Core.IntervalRat → Core.IntervalRat) (E : ExtendedInterval) : ExtendedInterval

Lift a unary operation to extended intervals

Equations

• LeanCert.Engine.liftUnary op E = { parts := List.map op E.parts }

theorem LeanCert.Engine.mem_liftUnary {f : ℝ → ℝ} {op : Core.IntervalRat → Core.IntervalRat} (hop : ∀ (x : ℝ) (I : Core.IntervalRat), x ∈ I → f x ∈ op I) {x : ℝ} {E : ExtendedInterval} (hx : x ∈ E) : f x ∈ liftUnary op E

Soundness of unary lifting

def LeanCert.Engine.liftBinary (op : Core.IntervalRat → Core.IntervalRat → Core.IntervalRat) (E₁ E₂ : ExtendedInterval) : ExtendedInterval

Lift a binary operation to extended intervals (Cartesian product)

Equations

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

theorem LeanCert.Engine.mem_liftBinary {f : ℝ → ℝ → ℝ} {op : Core.IntervalRat → Core.IntervalRat → Core.IntervalRat} (hop : ∀ (x y : ℝ) (I J : Core.IntervalRat), x ∈ I → y ∈ J → f x y ∈ op I J) {x y : ℝ} {E₁ E₂ : ExtendedInterval} (hx : x ∈ E₁) (hy : y ∈ E₂) : f x y ∈ liftBinary op E₁ E₂

Soundness of binary lifting

Extended Interval Evaluator

structure LeanCert.Engine.ExtendedConfig : Type

Configuration for extended interval evaluation

• taylorDepth : ℕ

  Taylor series depth for transcendental functions

• largeBound : ℚ

  Large bound representing "infinity"

instance LeanCert.Engine.instReprExtendedConfig : Repr ExtendedConfig

Equations

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

def LeanCert.Engine.instReprExtendedConfig.repr : ExtendedConfig → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.instInhabitedExtendedConfig : Inhabited ExtendedConfig

Equations

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

def LeanCert.Engine.instInhabitedExtendedConfig.default : ExtendedConfig

Equations

• LeanCert.Engine.instInhabitedExtendedConfig.default = { taylorDepth := default, largeBound := default }

@[reducible, inline]

abbrev LeanCert.Engine.ExtendedEnv : Type

Environment mapping variable indices to extended intervals

Equations

• LeanCert.Engine.ExtendedEnv = (ℕ → LeanCert.Engine.ExtendedInterval)

def LeanCert.Engine.extendEnv (ρ : IntervalEnv) : ExtendedEnv

Convert a standard interval environment to an extended environment

Equations

• LeanCert.Engine.extendEnv ρ i = LeanCert.Engine.ExtendedInterval.singleton (ρ i)

def LeanCert.Engine.evalExtended (e : Core.Expr) (ρ : ExtendedEnv) (cfg : ExtendedConfig := { }) : ExtendedInterval

Extended interval evaluator.

This evaluator handles singularities by splitting intervals at discontinuities. The key improvement over standard evaluation is in inv: when the denominator interval contains zero, we return two separate intervals rather than one huge interval spanning everything.

For other operations, we lift the standard interval operations to work on all pairs of interval parts.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.evalExtended (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Engine.ExtendedInterval.singleton (LeanCert.Core.IntervalRat.singleton q)
• LeanCert.Engine.evalExtended (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
• LeanCert.Engine.evalExtended (e₁.add e₂) ρ cfg = LeanCert.Engine.liftBinary LeanCert.Core.IntervalRat.add (LeanCert.Engine.evalExtended e₁ ρ cfg) (LeanCert.Engine.evalExtended e₂ ρ cfg)
• LeanCert.Engine.evalExtended (e₁.mul e₂) ρ cfg = LeanCert.Engine.liftBinary LeanCert.Core.IntervalRat.mul (LeanCert.Engine.evalExtended e₁ ρ cfg) (LeanCert.Engine.evalExtended e₂ ρ cfg)
• LeanCert.Engine.evalExtended e_2.neg ρ cfg = LeanCert.Engine.liftUnary LeanCert.Core.IntervalRat.neg (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.exp ρ cfg = LeanCert.Engine.liftUnary (fun (I : LeanCert.Core.IntervalRat) => I.expComputable cfg.taylorDepth) (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.sin ρ cfg = LeanCert.Engine.liftUnary (fun (I : LeanCert.Core.IntervalRat) => I.sinComputable cfg.taylorDepth) (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.cos ρ cfg = LeanCert.Engine.liftUnary (fun (I : LeanCert.Core.IntervalRat) => I.cosComputable cfg.taylorDepth) (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.atan ρ cfg = LeanCert.Engine.liftUnary LeanCert.Engine.atanInterval (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.arsinh ρ cfg = LeanCert.Engine.liftUnary LeanCert.Engine.arsinhInterval (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.atanh ρ cfg = LeanCert.Engine.ExtendedInterval.singleton { lo := -100, hi := 100, le := LeanCert.Engine.evalExtended._proof_2 }
• LeanCert.Engine.evalExtended e_2.sinc ρ cfg = LeanCert.Engine.ExtendedInterval.singleton { lo := -1, hi := 1, le := LeanCert.Engine.evalExtended._proof_3 }
• LeanCert.Engine.evalExtended e_2.erf ρ cfg = LeanCert.Engine.ExtendedInterval.singleton { lo := -1, hi := 1, le := LeanCert.Engine.evalExtended._proof_3 }
• LeanCert.Engine.evalExtended e_2.tanh ρ cfg = LeanCert.Engine.liftUnary LeanCert.Engine.tanhInterval (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended e_2.sqrt ρ cfg = LeanCert.Engine.liftUnary LeanCert.Core.IntervalRat.sqrtInterval (LeanCert.Engine.evalExtended e_2 ρ cfg)
• LeanCert.Engine.evalExtended LeanCert.Core.Expr.pi ρ cfg = LeanCert.Engine.ExtendedInterval.singleton LeanCert.Engine.piInterval

def LeanCert.Engine.evalExtended1 (e : Core.Expr) (I : Core.IntervalRat) (cfg : ExtendedConfig := { }) : ExtendedInterval

Convenience function for single-variable extended evaluation

Equations

• LeanCert.Engine.evalExtended1 e I cfg = LeanCert.Engine.evalExtended e (fun (x : ℕ) => LeanCert.Engine.ExtendedInterval.singleton I) cfg

def LeanCert.Engine.evalExtendedHull (e : Core.Expr) (ρ : ExtendedEnv) (cfg : ExtendedConfig := { }) : Core.IntervalRat

Collapse extended evaluation to standard evaluation via hull

Equations

• LeanCert.Engine.evalExtendedHull e ρ cfg = (LeanCert.Engine.evalExtended e ρ cfg).hull

Soundness Theorem

def LeanCert.Engine.extendedEnvMem (ρ_real : ℕ → ℝ) (ρ_ext : ExtendedEnv) : Prop

Real environment membership in extended environment

Equations

• LeanCert.Engine.extendedEnvMem ρ_real ρ_ext = ∀ (i : ℕ), ρ_real i ∈ ρ_ext i

def LeanCert.Engine.evalDomainValidExtended (e : Core.Expr) (ρ : ExtendedEnv) (cfg : ExtendedConfig := { }) : Prop

Domain validity for Extended evaluation. For log, we require the argument's hull to have positive lower bound, ensuring all parts have positive lo and the filter keeps them.

Equations

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

theorem LeanCert.Engine.evalDomainValidExtended_of_ExprSupported {e : Core.Expr} (hsupp : ExprSupported e) (ρ : ExtendedEnv) (cfg : ExtendedConfig := { }) : evalDomainValidExtended e ρ cfg

Domain validity is trivially true for ExprSupported expressions (which exclude log).

theorem LeanCert.Engine.evalExtended_correct_core (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_ext : ExtendedEnv) (hρ : extendedEnvMem ρ_real ρ_ext) (cfg : ExtendedConfig := { }) (hdom : evalDomainValidExtended e ρ_ext cfg) : Core.Expr.eval ρ_real e ∈ evalExtended e ρ_ext cfg

Soundness of extended evaluation for the core expression subset.

If all variables are in their respective extended intervals, and the expression is in the supported core subset (no partial functions), then the result is in the extended interval.

Utility: Hull Soundness

theorem LeanCert.Engine.mem_evalExtendedHull_of_mem_evalExtended (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_ext : ExtendedEnv) (heval : Core.Expr.eval ρ_real e ∈ evalExtended e ρ_ext) (hne : (evalExtended e ρ_ext).parts ≠ []) : Core.Expr.eval ρ_real e ∈ evalExtendedHull e ρ_ext

If x is in the extended interval, it's in the hull