Documentation

LeanCert.Examples.Showcase

LeanCert Showcase #

Demonstrations of verified numerical computation in Lean 4.

What This Library Does #

LeanCert proves facts about real-valued functions using interval arithmetic. The key idea: compute with rational intervals, get proofs about reals.

Highlights #

  1. Transcendental bounds: exp, sin, cos with Taylor model error bounds
  2. Root existence: Prove √2 exists via sign change
  3. Root absence: Prove functions stay away from zero
  4. Composition: Combine operations freely

The Golden Theorem Pattern #

Each verified result follows this pattern:

  1. Build an Expr (expression AST) or use raw Lean syntax
  2. Run interval evaluation → get rational bounds
  3. Use native_decide to check the bound
  4. Golden theorem lifts to a proof about reals

Intervals #

source
def LeanCert.Examples.Showcase.I01 :
Core.IntervalRat
Equations
Instances For
    source
    def LeanCert.Examples.Showcase.I_sym :
    Core.IntervalRat
    Equations
    Instances For

      Section 1: Basic Polynomial Bounds #

      Simple examples showing interval_bound on polynomials.

      source
      theorem LeanCert.Examples.Showcase.xsq_le_one (x : ℝ) :
      x ∈ I01 → x * x ≤ ↑1

      x² ≤ 1 on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.zero_le_xsq (x : ℝ) :
      x ∈ I01 → ↑0 ≤ x * x

      0 ≤ x² on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.xsq_le_one_sym (x : ℝ) :
      x ∈ I_sym → x * x ≤ ↑1

      x² ≤ 1 on [-1, 1]

      Section 2: Transcendental Functions #

      exp, sin, cos with verified Taylor series bounds.

      source
      theorem LeanCert.Examples.Showcase.sin_le_one (x : ℝ) :
      x ∈ I01 → Real.sin x ≤ ↑1

      sin(x) ≤ 1 on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.neg_one_le_sin (x : ℝ) :
      x ∈ I01 → ↑(-1) ≤ Real.sin x

      -1 ≤ sin(x) on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.cos_le_one (x : ℝ) :
      x ∈ I01 → Real.cos x ≤ ↑1

      cos(x) ≤ 1 on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.exp_le_three (x : ℝ) :
      x ∈ I01 → Real.exp x ≤ ↑3

      exp(x) ≤ 3 on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.one_le_exp (x : ℝ) :
      x ∈ I01 → ↑1 ≤ Real.exp x

      1 ≤ exp(x) on [0, 1] - boundary case with monotonicity

      Section 3: Combined Expressions #

      Mixing polynomials with transcendentals.

      source
      theorem LeanCert.Examples.Showcase.xsq_plus_sin_le_two (x : ℝ) :
      x ∈ I01 → x * x + Real.sin x ≤ ↑2

      x² + sin(x) ≤ 2 on [0, 1]

      source
      theorem LeanCert.Examples.Showcase.xsq_minus_two_neg (x : ℝ) :
      x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (((Core.Expr.var 0).mul (Core.Expr.var 0)).add (Core.Expr.const 2).neg) < ↑0

      x² - 2 < 0 on [0, 1] (since √2 > 1)

      Section 4: Root Absence #

      Prove functions have no roots by showing they stay strictly positive/negative.

      source
      theorem LeanCert.Examples.Showcase.xsq_plus_one_no_root (x : ℝ) :
      x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (((Core.Expr.var 0).mul (Core.Expr.var 0)).add (Core.Expr.const 1)) ≠ 0

      x² + 1 ≠ 0 on [0, 1] (always positive)

      source
      theorem LeanCert.Examples.Showcase.exp_no_root (x : ℝ) :
      x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp ≠ 0

      exp(x) ≠ 0 on [0, 1] (always positive)

      source
      theorem LeanCert.Examples.Showcase.x_plus_two_no_root (x : ℝ) :
      x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).add (Core.Expr.const 2)) ≠ 0

      x + 2 ≠ 0 on [0, 1] (always positive)

      source
      theorem LeanCert.Examples.Showcase.xsq_minus_two_no_root (x : ℝ) :
      x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (((Core.Expr.var 0).mul (Core.Expr.var 0)).add (Core.Expr.const 2).neg) ≠ 0

      x² - 2 ≠ 0 on [0, 1] (√2 ≈ 1.41 is outside [0,1])

      Section 5: Root Existence #

      Prove roots exist via sign change (Intermediate Value Theorem).

      source
      def LeanCert.Examples.Showcase.I12 :
      Core.IntervalRat
      Equations
      Instances For
        source
        theorem LeanCert.Examples.Showcase.sqrt2_exists :
        ∃ x ∈ I12, Core.Expr.eval (fun (x_1 : ℕ) => x) (((Core.Expr.var 0).mul (Core.Expr.var 0)).add (Core.Expr.const 2).neg) = 0

        √2 exists: there is an x ∈ [1, 2] with x² = 2

        source
        theorem LeanCert.Examples.Showcase.pi_half_exists :
        ∃ x ∈ I12, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).cos = 0

        π/2 exists: there is an x ∈ [1, 2] with cos(x) = 0

        source
        theorem LeanCert.Examples.Showcase.ln2_exists :
        ∃ x ∈ I01, Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).exp.add (Core.Expr.const 2).neg) = 0

        ln(2) exists: there is an x ∈ [0, 1] with exp(x) = 2

        Why This Matters #

        1. Verified: Every bound is machine-checked by Lean's kernel
        2. Computational: Bounds computed at compile time via native_decide
        3. Composable: Build complex proofs from simple pieces
        4. Automated: Tactics handle boilerplate

        The library automates numerical verification where symbolic methods are tedious.