Rational Endpoint Intervals - Core Definitions

This file defines IntervalRat, a concrete interval type with rational endpoints suitable for computation. We prove the Fundamental Theorem of Interval Arithmetic (FTIA) for each operation.

Main definitions

• LeanCert.Core.IntervalRat - Intervals with rational endpoints
• LeanCert.Core.IntervalRat.toSet - Semantic interpretation as a subset of ℝ
• Operations: add, neg, sub, mul, inv, div

Main theorems

• mem_add - FTIA for addition
• mem_neg - FTIA for negation
• mem_sub - FTIA for subtraction
• mem_mul - FTIA for multiplication

Design notes

All operations maintain the invariant lo ≤ hi. Domain restrictions for partial operations (like inv) are encoded via separate types or explicit hypotheses.

structure LeanCert.Core.IntervalRat : Type

An interval with rational endpoints

• lo : ℚ
• hi : ℚ
• le : self.lo ≤ self.hi

instance LeanCert.Core.instReprIntervalRat : Repr IntervalRat

Equations

• LeanCert.Core.instReprIntervalRat = { reprPrec := LeanCert.Core.instReprIntervalRat.repr }

def LeanCert.Core.instReprIntervalRat.repr : IntervalRat → ℕ → Std.Format

Equations

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

instance LeanCert.Core.instInhabitedIntervalRat : Inhabited IntervalRat

Default interval [0, 0] for unsupported expression branches

Equations

• LeanCert.Core.instInhabitedIntervalRat = { default := { lo := 0, hi := 0, le := LeanCert.Core.instInhabitedIntervalRat._proof_1 } }

def LeanCert.Core.IntervalRat.toSet (I : IntervalRat) : Set ℝ

The set of reals contained in this interval

Equations

• I.toSet = Set.Icc ↑I.lo ↑I.hi

instance LeanCert.Core.IntervalRat.instMembershipReal : Membership ℝ IntervalRat

Membership in an interval

Equations

• LeanCert.Core.IntervalRat.instMembershipReal = { mem := fun (I : LeanCert.Core.IntervalRat) (x : ℝ) => ↑I.lo ≤ x ∧ x ≤ ↑I.hi }

@[simp]

theorem LeanCert.Core.IntervalRat.mem_def (x : ℝ) (I : IntervalRat) : x ∈ I ↔ ↑I.lo ≤ x ∧ x ≤ ↑I.hi

theorem LeanCert.Core.IntervalRat.mem_iff_mem_Icc (x : ℝ) (I : IntervalRat) : x ∈ I ↔ x ∈ Set.Icc ↑I.lo ↑I.hi

Membership in IntervalRat is the same as membership in Set.Icc

theorem LeanCert.Core.IntervalRat.forall_mem_iff_forall_Icc {P : ℝ → Prop} (I : IntervalRat) : (∀ x ∈ I, P x) ↔ ∀ x ∈ Set.Icc ↑I.lo ↑I.hi, P x

Universal quantifier over IntervalRat equals universal over Set.Icc

theorem LeanCert.Core.IntervalRat.exists_mem_iff_exists_Icc {P : ℝ → Prop} (I : IntervalRat) : (∃ x ∈ I, P x) ↔ ∃ x ∈ Set.Icc ↑I.lo ↑I.hi, P x

Existence in IntervalRat equals existence in Set.Icc

def LeanCert.Core.IntervalRat.singleton (q : ℚ) : IntervalRat

Create an interval from a single rational

Equations

• LeanCert.Core.IntervalRat.singleton q = { lo := q, hi := q, le := ⋯ }

theorem LeanCert.Core.IntervalRat.mem_singleton (q : ℚ) : ↑q ∈ singleton q

def LeanCert.Core.IntervalRat.width (I : IntervalRat) : ℚ

The width of an interval

Equations

• I.width = I.hi - I.lo

theorem LeanCert.Core.IntervalRat.width_nonneg (I : IntervalRat) : 0 ≤ I.width

def LeanCert.Core.IntervalRat.midpoint (I : IntervalRat) : ℚ

Midpoint of an interval

Equations

• I.midpoint = (I.lo + I.hi) / 2

theorem LeanCert.Core.IntervalRat.midpoint_mem (I : IntervalRat) : ↑I.midpoint ∈ I

The midpoint of an interval is contained in the interval

Interval addition

def LeanCert.Core.IntervalRat.add (I J : IntervalRat) : IntervalRat

Add two intervals

Equations

• I.add J = { lo := I.lo + J.lo, hi := I.hi + J.hi, le := ⋯ }

theorem LeanCert.Core.IntervalRat.mem_add {x y : ℝ} {I J : IntervalRat} (hx : x ∈ I) (hy : y ∈ J) : x + y ∈ I.add J

FTIA for addition

Interval negation

def LeanCert.Core.IntervalRat.neg (I : IntervalRat) : IntervalRat

Negate an interval

Equations

• I.neg = { lo := -I.hi, hi := -I.lo, le := ⋯ }

theorem LeanCert.Core.IntervalRat.mem_neg {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : -x ∈ I.neg

FTIA for negation

Interval subtraction

def LeanCert.Core.IntervalRat.sub (I J : IntervalRat) : IntervalRat

Subtract two intervals

Equations

• I.sub J = I.add J.neg

theorem LeanCert.Core.IntervalRat.mem_sub {x y : ℝ} {I J : IntervalRat} (hx : x ∈ I) (hy : y ∈ J) : x - y ∈ I.sub J

FTIA for subtraction

Interval multiplication

def LeanCert.Core.IntervalRat.mul (I J : IntervalRat) : IntervalRat

Multiply two intervals

Equations

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

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

FTIA for multiplication

Interval containing zero check

def LeanCert.Core.IntervalRat.containsZero (I : IntervalRat) : Prop

Check if an interval contains zero

Equations

• I.containsZero = (I.lo ≤ 0 ∧ 0 ≤ I.hi)

instance LeanCert.Core.IntervalRat.instDecidableContainsZero (I : IntervalRat) : Decidable I.containsZero

Decidable containsZero

Equations

• I.instDecidableContainsZero = inferInstanceAs (Decidable (I.lo ≤ 0 ∧ 0 ≤ I.hi))

structure LeanCert.Core.IntervalRat.IntervalRatNonzeroextends LeanCert.Core.IntervalRat : Type

An interval that is guaranteed not to contain zero

• lo : ℚ
• hi : ℚ
• le : self.lo ≤ self.hi
• nonzero : ¬self.containsZero

Interval inversion (for nonzero intervals)

def LeanCert.Core.IntervalRat.invNonzero (I : IntervalRatNonzero) : IntervalRat

Invert an interval that doesn't contain zero

Equations

• LeanCert.Core.IntervalRat.invNonzero I = if h : 0 < I.lo then { lo := I.hi⁻¹, hi := I.lo⁻¹, le := ⋯ } else { lo := I.hi⁻¹, hi := I.lo⁻¹, le := ⋯ }

FTIA for inversion

theorem LeanCert.Core.IntervalRat.mem_invNonzero {x : ℝ} {I : IntervalRatNonzero} (hx : x ∈ I.toIntervalRat) (_hxne : x ≠ 0) : x⁻¹ ∈ invNonzero I

Scalar operations

def LeanCert.Core.IntervalRat.scale (q : ℚ) (I : IntervalRat) : IntervalRat

Scale an interval by a rational

Equations

• LeanCert.Core.IntervalRat.scale q I = if hq : 0 ≤ q then { lo := q * I.lo, hi := q * I.hi, le := ⋯ } else { lo := q * I.hi, hi := q * I.lo, le := ⋯ }

theorem LeanCert.Core.IntervalRat.mem_scale {x : ℝ} {I : IntervalRat} (q : ℚ) (hx : x ∈ I) : ↑q * x ∈ scale q I

FTIA for scaling

Interval splitting

def LeanCert.Core.IntervalRat.bisect (I : IntervalRat) : IntervalRat × IntervalRat

Split an interval at its midpoint

Equations

• I.bisect = ({ lo := I.lo, hi := I.midpoint, le := ⋯ }, { lo := I.midpoint, hi := I.hi, le := ⋯ })

theorem LeanCert.Core.IntervalRat.mem_bisect_left {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hm : x ≤ ↑I.midpoint) : x ∈ I.bisect.1

theorem LeanCert.Core.IntervalRat.mem_bisect_right {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hm : ↑I.midpoint ≤ x) : x ∈ I.bisect.2

theorem LeanCert.Core.IntervalRat.midpoint_sub_lo (I : IntervalRat) : ↑I.midpoint - ↑I.lo = (↑I.hi - ↑I.lo) / 2

Distance from midpoint to lo is half the width

theorem LeanCert.Core.IntervalRat.hi_sub_midpoint (I : IntervalRat) : ↑I.hi - ↑I.midpoint = (↑I.hi - ↑I.lo) / 2

Distance from hi to midpoint is half the width

theorem LeanCert.Core.IntervalRat.midpoint_ge_lo (I : IntervalRat) : I.lo ≤ I.midpoint

Midpoint is at least lo

theorem LeanCert.Core.IntervalRat.midpoint_le_hi (I : IntervalRat) : I.midpoint ≤ I.hi

Midpoint is at most hi

theorem LeanCert.Core.IntervalRat.midpoint_ge_lo_real (I : IntervalRat) : ↑I.lo ≤ ↑I.midpoint

Midpoint is at least lo (real version)

theorem LeanCert.Core.IntervalRat.midpoint_le_hi_real (I : IntervalRat) : ↑I.midpoint ≤ ↑I.hi

Midpoint is at most hi (real version)

theorem LeanCert.Core.IntervalRat.mem_of_mem_bisect_left {x : ℝ} {I : IntervalRat} (hx : x ∈ I.bisect.1) : x ∈ I

Left bisection is a subset of the original interval

theorem LeanCert.Core.IntervalRat.mem_of_mem_bisect_right {x : ℝ} {I : IntervalRat} (hx : x ∈ I.bisect.2) : x ∈ I

Right bisection is a subset of the original interval

theorem LeanCert.Core.IntervalRat.mem_bisect_or {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : x ∈ I.bisect.1 ∨ x ∈ I.bisect.2

Any point in an interval is in one of its bisected halves

theorem LeanCert.Core.IntervalRat.mem_default (x : ℝ) : x ∈ default ↔ x = 0

The default interval [0,0] contains only 0

Interval intersection

def LeanCert.Core.IntervalRat.intersect (I J : IntervalRat) : Option IntervalRat

Intersect two intervals. Returns none if they don't intersect.

Equations

• I.intersect J = if h : max I.lo J.lo ≤ min I.hi J.hi then some { lo := max I.lo J.lo, hi := min I.hi J.hi, le := h } else none

theorem LeanCert.Core.IntervalRat.mem_intersect {x : ℝ} {I J : IntervalRat} (hI : x ∈ I) (hJ : x ∈ J) : ∃ (K : IntervalRat), I.intersect J = some K ∧ x ∈ K

If intersection succeeds, the result contains any point in both intervals

theorem LeanCert.Core.IntervalRat.intersect_subset_left {I J K : IntervalRat} (h : I.intersect J = some K) : K.lo ≥ I.lo ∧ K.hi ≤ I.hi

If intersection returns some K, then K ⊆ I

theorem LeanCert.Core.IntervalRat.intersect_subset_right {I J K : IntervalRat} (h : I.intersect J = some K) : K.lo ≥ J.lo ∧ K.hi ≤ J.hi

If intersection returns some K, then K ⊆ J