Tactic Examples

This file demonstrates using LeanCert's interval arithmetic to prove bounds on expressions.

Verified Examples

All examples in this file are FULLY PROVED using interval arithmetic. No sorry, no axioms beyond the standard Lean/Mathlib foundations.

Computability Design

We have two evaluation strategies:

1. Core (computable): For expressions in ExprSupportedCore (const, var, add, mul, neg, sin, cos), we use evalIntervalCore1 which is fully computable. The interval_le, interval_ge, etc. tactics work with native_decide.

2. Extended (noncomputable): For expressions with exp, we use evalInterval1 which requires noncomputable evaluation due to Real.exp floor/ceil bounds. These proofs use FTIA directly.

Basic interval bound examples

def LeanCert.Examples.Tactics.exprXSq : Core.Expr

The expression x²

Equations

• LeanCert.Examples.Tactics.exprXSq = (LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)

def LeanCert.Examples.Tactics.exprXSq_core : Core.ExprSupportedCore exprXSq

Proof that x² is in the core (computable) subset

Equations

• LeanCert.Examples.Tactics.exprXSq_core = ⋯

def LeanCert.Examples.Tactics.exprXSq_supp : Core.ExprSupported exprXSq

Proof that x² is supported

Equations

• LeanCert.Examples.Tactics.exprXSq_supp = ⋯

def LeanCert.Examples.Tactics.I01 : Core.IntervalRat

The unit interval [0, 1]

Equations

• LeanCert.Examples.Tactics.I01 = { lo := 0, hi := 1, le := LeanCert.Examples.Tactics.I01._proof_1 }

theorem LeanCert.Examples.Tactics.xsq_le_one_native (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq ≤ ↑1

Example: x² ≤ 1 for all x ∈ [0, 1] using the interval_le tactic. This uses the computable core evaluator with native_decide.

theorem LeanCert.Examples.Tactics.zero_le_xsq_native (x : ℝ) : x ∈ I01 → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq

Example: 0 ≤ x² for all x ∈ [0, 1] using native_decide.

theorem LeanCert.Examples.Tactics.xsq_le_one (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq ≤ ↑1

Example: x² ≤ 1 for all x ∈ [0, 1]. Manual proof for reference.

theorem LeanCert.Examples.Tactics.zero_le_xsq (x : ℝ) : x ∈ I01 → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq

Example: 0 ≤ x² for all x ∈ [0, 1]. Manual proof for reference.

Trigonometric bounds

def LeanCert.Examples.Tactics.exprSin : Core.Expr

The expression sin(x)

Equations

• LeanCert.Examples.Tactics.exprSin = (LeanCert.Core.Expr.var 0).sin

def LeanCert.Examples.Tactics.exprSin_core : Core.ExprSupportedCore exprSin

Proof that sin(x) is in the core subset

Equations

• LeanCert.Examples.Tactics.exprSin_core = ⋯

def LeanCert.Examples.Tactics.exprSin_supp : Core.ExprSupported exprSin

Proof that sin(x) is supported

Equations

• LeanCert.Examples.Tactics.exprSin_supp = ⋯

theorem LeanCert.Examples.Tactics.sin_le_one_native (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin ≤ ↑1

Example: sin(x) ≤ 1 for all x ∈ [0, 1] using native_decide.

theorem LeanCert.Examples.Tactics.neg_one_le_sin_native (x : ℝ) : x ∈ I01 → ↑(-1) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin

Example: -1 ≤ sin(x) for all x ∈ [0, 1] using native_decide.

theorem LeanCert.Examples.Tactics.sin_le_one (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin ≤ ↑1

Example: sin(x) ≤ 1 for all x ∈ [0, 1]. Manual proof for reference.

theorem LeanCert.Examples.Tactics.neg_one_le_sin (x : ℝ) : x ∈ I01 → ↑(-1) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin

Example: -1 ≤ sin(x) for all x ∈ [0, 1]. Manual proof for reference.

Combined expressions

def LeanCert.Examples.Tactics.exprXSqPlusSin : Core.Expr

The expression x² + sin(x)

Equations

• LeanCert.Examples.Tactics.exprXSqPlusSin = ((LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)).add (LeanCert.Core.Expr.var 0).sin

def LeanCert.Examples.Tactics.exprXSqPlusSin_core : Core.ExprSupportedCore exprXSqPlusSin

Proof that x² + sin(x) is in the core subset

Equations

• LeanCert.Examples.Tactics.exprXSqPlusSin_core = ⋯

def LeanCert.Examples.Tactics.exprXSqPlusSin_supp : Core.ExprSupported exprXSqPlusSin

Proof that x² + sin(x) is supported

Equations

• LeanCert.Examples.Tactics.exprXSqPlusSin_supp = ⋯

theorem LeanCert.Examples.Tactics.xsq_plus_sin_le_two_native (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSqPlusSin ≤ ↑2

Example: x² + sin(x) ≤ 2 for all x ∈ [0, 1] using native_decide.

theorem LeanCert.Examples.Tactics.neg_one_le_xsq_plus_sin_native (x : ℝ) : x ∈ I01 → ↑(-1) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSqPlusSin

Example: -1 ≤ x² + sin(x) for all x ∈ [0, 1] using native_decide.

theorem LeanCert.Examples.Tactics.xsq_plus_sin_le_two (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSqPlusSin ≤ ↑2

Example: x² + sin(x) ≤ 2 for all x ∈ [0, 1]. Manual proof for reference.

theorem LeanCert.Examples.Tactics.neg_one_le_xsq_plus_sin (x : ℝ) : x ∈ I01 → ↑(-1) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSqPlusSin

Example: -1 ≤ x² + sin(x) for all x ∈ [0, 1]. Manual proof for reference.

Strict bounds

def LeanCert.Examples.Tactics.exprXSqMinus2 : Core.Expr

The expression x² - 2

Equations

• LeanCert.Examples.Tactics.exprXSqMinus2 = ((LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)).add (LeanCert.Core.Expr.const 2).neg

def LeanCert.Examples.Tactics.exprXSqMinus2_core : Core.ExprSupportedCore exprXSqMinus2

Proof that x² - 2 is in the core subset

Equations

• LeanCert.Examples.Tactics.exprXSqMinus2_core = ⋯

def LeanCert.Examples.Tactics.exprXSqMinus2_supp : Core.ExprSupported exprXSqMinus2

Proof that x² - 2 is supported

Equations

• LeanCert.Examples.Tactics.exprXSqMinus2_supp = ⋯

theorem LeanCert.Examples.Tactics.xsq_minus_two_lt_zero_native (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSqMinus2 < ↑0

Example: x² - 2 < 0 for all x ∈ [0, 1] using native_decide. Since x² ≤ 1 on [0,1], we have x² - 2 ≤ -1 < 0.

theorem LeanCert.Examples.Tactics.xsq_minus_two_lt_zero (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSqMinus2 < ↑0

Example: x² - 2 < 0 for all x ∈ [0, 1]. Manual proof for reference.

Working with polynomials

def LeanCert.Examples.Tactics.exprPoly : Core.Expr

The expression 2x² + 3x + 1

Equations

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

def LeanCert.Examples.Tactics.exprPoly_core : Core.ExprSupportedCore exprPoly

Proof that 2x² + 3x + 1 is in the core subset

Equations

• LeanCert.Examples.Tactics.exprPoly_core = ⋯

def LeanCert.Examples.Tactics.exprPoly_supp : Core.ExprSupported exprPoly

Proof that 2x² + 3x + 1 is supported

Equations

• LeanCert.Examples.Tactics.exprPoly_supp = ⋯

theorem LeanCert.Examples.Tactics.poly_le_six_native (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprPoly ≤ 6

Example: 2x² + 3x + 1 ≤ 6 for all x ∈ [0, 1] using native_decide. At x=1: 2 + 3 + 1 = 6.

theorem LeanCert.Examples.Tactics.one_le_poly_native (x : ℝ) : x ∈ I01 → ↑1 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprPoly

Example: 1 ≤ 2x² + 3x + 1 for all x ∈ [0, 1] using native_decide. At x=0: 0 + 0 + 1 = 1.

theorem LeanCert.Examples.Tactics.poly_le_six (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprPoly ≤ 6

Example: 2x² + 3x + 1 ≤ 6 for all x ∈ [0, 1]. Manual proof for reference.

theorem LeanCert.Examples.Tactics.one_le_poly (x : ℝ) : x ∈ I01 → ↑1 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprPoly

Example: 1 ≤ 2x² + 3x + 1 for all x ∈ [0, 1]. Manual proof for reference.

Examples with exp (noncomputable)

Expressions containing exp use the extended evaluator evalInterval1, which is noncomputable due to Real.exp floor/ceil bounds. These examples demonstrate bounds using direct FTIA application rather than native_decide.

def LeanCert.Examples.Tactics.exprExp : Core.Expr

The expression exp(x)

Equations

• LeanCert.Examples.Tactics.exprExp = (LeanCert.Core.Expr.var 0).exp

def LeanCert.Examples.Tactics.exprExp_supp : Core.ExprSupported exprExp

Proof that exp(x) is supported (but NOT in ExprSupportedCore)

Equations

• LeanCert.Examples.Tactics.exprExp_supp = ⋯

theorem LeanCert.Examples.Tactics.exp_le_three (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ≤ ↑3

Example: exp(x) ≤ 3 for all x ∈ [0, 1]. Since exp(1) ≈ 2.718, this bound holds. This uses the extended evaluator and requires direct proof.

theorem LeanCert.Examples.Tactics.one_le_exp (x : ℝ) : x ∈ I01 → ↑1 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp

Example: 1 ≤ exp(x) for all x ∈ [0, 1]. Since exp(0) = 1 and exp is increasing, this holds.

def LeanCert.Examples.Tactics.exprXPlusExp : Core.Expr

The expression x + exp(x)

Equations

• LeanCert.Examples.Tactics.exprXPlusExp = (LeanCert.Core.Expr.var 0).add (LeanCert.Core.Expr.var 0).exp

def LeanCert.Examples.Tactics.exprXPlusExp_supp : Core.ExprSupported exprXPlusExp

Proof that x + exp(x) is supported

Equations

• LeanCert.Examples.Tactics.exprXPlusExp_supp = ⋯

theorem LeanCert.Examples.Tactics.x_plus_exp_le_four (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXPlusExp ≤ ↑4

Example: x + exp(x) ≤ 4 for all x ∈ [0, 1]. x ≤ 1 and exp(x) ≤ 3, so x + exp(x) ≤ 4.

theorem LeanCert.Examples.Tactics.one_le_x_plus_exp (x : ℝ) : x ∈ I01 → ↑1 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXPlusExp

Example: 1 ≤ x + exp(x) for all x ∈ [0, 1]. x ≥ 0 and exp(x) ≥ 1, so x + exp(x) ≥ 1.