Tests for Automated Interval Bound Tactic

This file tests the interval_bound tactic.

def LeanCert.Tactic.TestAuto.I01 : Core.IntervalRat

The unit interval [0, 1]

Equations

• LeanCert.Tactic.TestAuto.I01 = { lo := 0, hi := 1, le := LeanCert.Tactic.TestAuto.I01._proof_1 }

theorem LeanCert.Tactic.TestAuto.test_xsq_le_one (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).mul (Core.Expr.var 0)) ≤ ↑1

theorem LeanCert.Tactic.TestAuto.test_zero_le_xsq (x : ℝ) : x ∈ I01 → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).mul (Core.Expr.var 0))

theorem LeanCert.Tactic.TestAuto.test_sin_le_one (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).sin ≤ ↑1

theorem LeanCert.Tactic.TestAuto.test_neg_one_le_sin (x : ℝ) : x ∈ I01 → ↑(-1) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).sin

theorem LeanCert.Tactic.TestAuto.test_xsq_plus_sin (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (((Core.Expr.var 0).mul (Core.Expr.var 0)).add (Core.Expr.var 0).sin) ≤ ↑2

theorem LeanCert.Tactic.TestAuto.test_xsq_minus_two_lt_zero (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

theorem LeanCert.Tactic.TestAuto.test_exp_le_three (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp ≤ ↑3

theorem LeanCert.Tactic.TestAuto.test_point_nine_le_exp (x : ℝ) : x ∈ I01 → ↑(9 / 10) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp

theorem LeanCert.Tactic.TestAuto.test_one_le_exp (x : ℝ) : x ∈ I01 → ↑1 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp

theorem LeanCert.Tactic.TestAuto.test_exp_le_e_approx (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp ≤ ↑(11 / 4)

Raw Lean Expression Tests

These tests use raw Lean math syntax (x * x, Real.sin x, etc.) instead of the pre-reified Expr.eval form. The tactic should automatically reify these expressions.

theorem LeanCert.Tactic.TestAuto.test_raw_xsq_le_one (x : ℝ) : x ∈ I01 → x * x ≤ ↑1

theorem LeanCert.Tactic.TestAuto.test_raw_zero_le_xsq (x : ℝ) : x ∈ I01 → ↑0 ≤ x * x

theorem LeanCert.Tactic.TestAuto.test_raw_sin_le_one (x : ℝ) : x ∈ I01 → Real.sin x ≤ ↑1

theorem LeanCert.Tactic.TestAuto.test_raw_exp_le_three (x : ℝ) : x ∈ I01 → Real.exp x ≤ ↑3

theorem LeanCert.Tactic.TestAuto.test_raw_one_le_exp (x : ℝ) : x ∈ I01 → ↑1 ≤ Real.exp x

theorem LeanCert.Tactic.TestAuto.test_raw_xsq_plus_sin (x : ℝ) : x ∈ I01 → x * x + Real.sin x ≤ ↑2

Global Optimization - Manual Usage

The global optimization theorems are proven and can be used manually. The automatic opt_bound tactic is a work in progress for full automation. Below are examples of how to use the verification theorems directly.

def LeanCert.Tactic.TestAuto.B01 : Engine.Optimization.Box

A 1D box [0, 1] for single variable optimization

Equations

• LeanCert.Tactic.TestAuto.B01 = [LeanCert.Tactic.TestAuto.I01]

def LeanCert.Tactic.TestAuto.B01_2D : Engine.Optimization.Box

A 2D box [0, 1] × [0, 1]

Equations

• LeanCert.Tactic.TestAuto.B01_2D = [LeanCert.Tactic.TestAuto.I01, LeanCert.Tactic.TestAuto.I01]

theorem LeanCert.Tactic.TestAuto.test_opt_xsq_le_one (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ B01 → (∀ i ≥ List.length B01, ρ i = 0) → Core.Expr.eval ρ ((Core.Expr.var 0).mul (Core.Expr.var 0)) ≤ ↑1

theorem LeanCert.Tactic.TestAuto.test_opt_zero_le_xsq (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ B01 → (∀ i ≥ List.length B01, ρ i = 0) → ↑0 ≤ Core.Expr.eval ρ ((Core.Expr.var 0).mul (Core.Expr.var 0))

theorem LeanCert.Tactic.TestAuto.test_opt_2d_sum_sq (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ B01_2D → (∀ i ≥ List.length B01_2D, ρ i = 0) → Core.Expr.eval ρ (((Core.Expr.var 0).mul (Core.Expr.var 0)).add ((Core.Expr.var 1).mul (Core.Expr.var 1))) ≤ ↑2

Root Finding Tests

These tests verify the root_bound tactic for proving absence of roots. Note: The 0 must be of type ℝ (not ℚ coerced to ℝ) since Expr.eval returns ℝ.

theorem LeanCert.Tactic.TestAuto.test_xsq_plus_one_ne_zero (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

theorem LeanCert.Tactic.TestAuto.test_exp_ne_zero (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp ≠ 0

theorem LeanCert.Tactic.TestAuto.test_x_plus_two_ne_zero (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).add (Core.Expr.const 2)) ≠ 0

theorem LeanCert.Tactic.TestAuto.test_xsq_minus_two_ne_zero (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

Multivariate Bounds Tests

These tests verify the multivariate_bound tactic for proving bounds over multi-variable domains. The multivariate_bound tactic is currently under development.

NOTE: The full automatic bridging from ∀ x ∈ Set.Icc ... to the internal Box form requires additional work. For now, use the opt_bound tactic for global optimization goals that are already in the Box.envMem form.