Tests for Discovery Mode Tactics

This file tests the interval_roots tactic.

interval_roots Tests

These tests verify the interval_roots tactic for proving root existence. The tactic works by:

1. Detecting a sign change at the interval endpoints
2. Applying the Intermediate Value Theorem

def LeanCert.Tactic.TestDiscovery.I_neg1_1 : Core.IntervalRat

Equations

• LeanCert.Tactic.TestDiscovery.I_neg1_1 = { lo := -1, hi := 1, le := LeanCert.Tactic.TestDiscovery.I_neg1_1._proof_1 }

def LeanCert.Tactic.TestDiscovery.I_0_2 : Core.IntervalRat

Equations

• LeanCert.Tactic.TestDiscovery.I_0_2 = { lo := 0, hi := 2, le := LeanCert.Tactic.TestDiscovery.I_0_2._proof_1 }

def LeanCert.Tactic.TestDiscovery.I_1_2 : Core.IntervalRat

Equations

• LeanCert.Tactic.TestDiscovery.I_1_2 = { lo := 1, hi := 2, le := LeanCert.Tactic.TestDiscovery.I_1_2._proof_1 }

def LeanCert.Tactic.TestDiscovery.I_3_4 : Core.IntervalRat

Equations

• LeanCert.Tactic.TestDiscovery.I_3_4 = { lo := 3, hi := 4, le := LeanCert.Tactic.TestDiscovery.I_3_4._proof_1 }

def LeanCert.Tactic.TestDiscovery.I_0_1 : Core.IntervalRat

Equations

• LeanCert.Tactic.TestDiscovery.I_0_1 = { lo := 0, hi := 1, le := LeanCert.Tactic.TestDiscovery.I_0_1._proof_1 }

def LeanCert.Tactic.TestDiscovery.defaultCfg : Engine.EvalConfig

Equations

• LeanCert.Tactic.TestDiscovery.defaultCfg = { }

theorem LeanCert.Tactic.TestDiscovery.test_x_root : ∃ x ∈ I_neg1_1, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0) = 0

theorem LeanCert.Tactic.TestDiscovery.test_sqrt2_exists : ∃ x ∈ I_1_2, 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.TestDiscovery.test_sin_root : ∃ x ∈ I_3_4, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).sin = 0

theorem LeanCert.Tactic.TestDiscovery.test_exp_root : ∃ x ∈ I_0_1, Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).exp.add (Core.Expr.const 2).neg) = 0

theorem LeanCert.Tactic.TestDiscovery.test_cos_root : ∃ x ∈ I_1_2, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).cos = 0

Test interval_roots tactic

Now let's test the automated tactic. The tactic should:

1. Parse the goal
2. Reify the function
3. Generate proofs
4. Apply verify_sign_change
5. Solve with native_decide

theorem LeanCert.Tactic.TestDiscovery.test_tactic_x_root : ∃ x ∈ I_neg1_1, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0) = 0

theorem LeanCert.Tactic.TestDiscovery.test_tactic_sqrt2 : ∃ x ∈ I_1_2, 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.TestDiscovery.test_tactic_sin : ∃ x ∈ I_3_4, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).sin = 0

theorem LeanCert.Tactic.TestDiscovery.test_tactic_exp : ∃ x ∈ I_0_1, Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).exp.add (Core.Expr.const 2).neg) = 0

theorem LeanCert.Tactic.TestDiscovery.test_tactic_cos : ∃ x ∈ I_1_2, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).cos = 0

Test interval_minimize / interval_maximize tactics

These tactics prove existential goals about bounds by:

1. Running global optimization to find the bound
2. Instantiating the existential with the found value
3. Proving the universal bound using opt_bound

NOTE: The goal format must match exactly:

• interval_minimize: ∃ m, ∀ x ∈ I, c ≤ f(x) (where c is bvar 0)
• interval_maximize: ∃ M, ∀ x ∈ I, f(x) ≤ c (where c is bvar 0)

theorem LeanCert.Tactic.TestDiscovery.test_minimize_x2 : ∃ (m : ℚ), ∀ x ∈ I_neg1_1, Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).mul (Core.Expr.var 0)) ≥ ↑m

theorem LeanCert.Tactic.TestDiscovery.test_maximize_x2 : ∃ (M : ℚ), ∀ x ∈ I_neg1_1, Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).mul (Core.Expr.var 0)) ≤ ↑M

def LeanCert.Tactic.TestDiscovery.I_0_7 : Core.IntervalRat

Equations

• LeanCert.Tactic.TestDiscovery.I_0_7 = { lo := 0, hi := 7, le := LeanCert.Tactic.TestDiscovery.I_0_7._proof_1 }

theorem LeanCert.Tactic.TestDiscovery.test_minimize_sin : ∃ (m : ℚ), ∀ x ∈ I_0_7, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).sin ≥ ↑m

theorem LeanCert.Tactic.TestDiscovery.test_maximize_exp : ∃ (M : ℚ), ∀ x ∈ I_0_1, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp ≤ ↑M

#explore Command Tests

The #explore command analyzes a function on an interval and reports:

• Range bounds (min/max)
• Sign change detection (root existence)

interval_unique_root Tests

The interval_unique_root tactic proves ∃! x ∈ I, f(x) = 0 by:

1. Checking Newton iteration contracts (derivative bounded away from 0)
2. Using Rolle's theorem for uniqueness
3. Using IVT for existence (via contraction)

NOTE: These tests require the theorem with a sorry for the existence part. The tactic will work at runtime but the proof contains sorry.

theorem LeanCert.Tactic.TestDiscovery.test_unique_sqrt2 : ∃! x : ℝ, x ∈ I_1_2 ∧ 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.TestDiscovery.test_unique_ln2 : ∃! x : ℝ, x ∈ I_0_1 ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).exp.add (Core.Expr.const 2).neg) = 0

interval_integrate Tests

The interval_integrate tactic proves goals of the form ∫ x in lo..hi, f(x) ∈ bound where the bound is computed via interval arithmetic.

theorem LeanCert.Tactic.TestDiscovery.test_integrate_x : ∫ (x : ℝ) in ↑I_0_1.lo..↑I_0_1.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0) ∈ Validity.Integration.integrateInterval1Core (Core.Expr.var 0) I_0_1 defaultCfg

theorem LeanCert.Tactic.TestDiscovery.test_integrate_const : ∫ (x : ℝ) in ↑I_0_1.lo..↑I_0_1.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.const 1) ∈ Validity.Integration.integrateInterval1Core (Core.Expr.const 1) I_0_1 defaultCfg

theorem LeanCert.Tactic.TestDiscovery.test_integrate_x2 : ∫ (x : ℝ) in ↑I_0_1.lo..↑I_0_1.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) ((Core.Expr.var 0).mul (Core.Expr.var 0)) ∈ Validity.Integration.integrateInterval1Core ((Core.Expr.var 0).mul (Core.Expr.var 0)) I_0_1 defaultCfg

theorem LeanCert.Tactic.TestDiscovery.test_integrate_exp : ∫ (x : ℝ) in ↑I_0_1.lo..↑I_0_1.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).exp ∈ Validity.Integration.integrateInterval1Core (Core.Expr.var 0).exp I_0_1 defaultCfg

theorem LeanCert.Tactic.TestDiscovery.test_integrate_sin : ∫ (x : ℝ) in ↑I_0_1.lo..↑I_0_1.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) (Core.Expr.var 0).sin ∈ Validity.Integration.integrateInterval1Core (Core.Expr.var 0).sin I_0_1 defaultCfg