Choosing the Right Tactic

Quick reference for picking the right LeanCert tactic for a direct automation goal. For the overall proof-shape chooser, start with Choosing A Proof Shape.

Having issues? See the Troubleshooting Guide for common errors and solutions.

Decision Flowchart

What do you want to prove?
│
├─► "∀ x ∈ I, f(x) ≤ c" or "∀ x ∈ I, f(x) ≥ c"
│   │
│   ├─► Single variable? ──► certify_bound
│   │                        (or certify_kernel for kernel-only trust)
│   │
│   └─► Multiple variables? ──► multivariate_bound
│
├─► "∀ x ∈ I, f(x) ≠ 0"
│   └─► root_bound
│
├─► "∃ x ∈ I, f(x) = 0"
│   └─► interval_roots
│
├─► "∃! x ∈ I, f(x) = 0"
│   └─► interval_unique_root
│
├─► "∃ m, ∀ x ∈ I, f(x) ≥ m" (find minimum)
│   │
│   ├─► Single variable? ──► interval_minimize
│   └─► Multiple variables? ──► interval_minimize_mv
│
├─► "∃ M, ∀ x ∈ I, f(x) ≤ M" (find maximum)
│   │
│   ├─► Single variable? ──► interval_maximize
│   └─► Multiple variables? ──► interval_maximize_mv
│
├─► "∃ x ∈ I, ∀ y ∈ I, f(x) ≤ f(y)" (find argmin)
│   └─► interval_argmin
│
├─► "∃ x ∈ I, ∀ y ∈ I, f(y) ≤ f(x)" (find argmax)
│   └─► interval_argmax
│
├─► Point inequality (π < 3.15, etc.)
│   └─► interval_decide
│
├─► Integral bound
│   └─► interval_integrate
│
├─► Simplify vector/matrix indexing (![a,b,c] ⟨1,h⟩ → b)
│   └─► vec_simp
│
└─► Expand finite sum (∑ k ∈ Icc 1 3, f k → f 1 + f 2 + f 3)
    └─► finsum_expand

Quick Reference Table

I want to prove...	Tactic	Example
Upper bound on interval	certify_bound	∀ x ∈ Set.Icc 0 1, exp x ≤ 3
Lower bound on interval	certify_bound	∀ x ∈ Set.Icc 0 1, 0 ≤ exp x
Bound with kernel-only trust	certify_kernel	Same goals, higher trust
Multivariate bound	multivariate_bound	∀ x ∈ I, ∀ y ∈ J, x + y ≤ 2
Function has no roots	root_bound	∀ x ∈ I, x² + 1 ≠ 0
Root exists	interval_roots	∃ x ∈ I, x² - 2 = 0
Unique root exists	interval_unique_root	∃! x ∈ I, x² - 2 = 0
Minimum exists	interval_minimize	∃ m, ∀ x ∈ I, f x ≥ m
Maximum exists	interval_maximize	∃ M, ∀ x ∈ I, f x ≤ M
Find the minimizer	interval_argmin	∃ x ∈ I, ∀ y ∈ I, f x ≤ f y
Find the maximizer	interval_argmax	∃ x ∈ I, ∀ y ∈ I, f y ≤ f x
Point inequality	interval_decide	π < 3.15
Disprove a bound	interval_refute	Find counterexample
Simplify vector indexing	vec_simp	![a,b,c] ⟨1, h⟩ = b
Expand finite sums	finsum_expand	∑ k ∈ Icc 1 3, f k = f 1 + f 2 + f 3
Integral bound	interval_integrate	∫ x in a..b, f x ∈ I

Trust Levels

Tactic	Verification	When to use
certify_kernel	decide (kernel-only)	Maximum trust, slower
certify_kernel_fallback	decide, then native_decide	Explicit opt-in native fallback
certify_bound	native_decide	Good balance of trust/speed
certify_kernel_quick	decide (30 bits)	Fast, lower precision
certify_kernel_precise	decide (100 bits)	Tight bounds needed

Common Patterns

"My bound is too tight and fails"

-- Try 1: Increase Taylor depth
example : ∀ x ∈ Set.Icc 0 1, exp x ≤ 2.72 := by certify_bound 20

-- Try 2: Use subdivision
example : ∀ x ∈ Set.Icc 0 1, exp x ≤ 2.72 := by interval_bound_subdiv 15 3

-- Try 3: Use higher precision dyadic
example : ∀ x ∈ Set.Icc 0 1, exp x ≤ 2.72 := by certify_kernel_precise

"I don't know what bound to use"

Use discovery tactics to find bounds first:

-- Find the actual minimum/maximum
example : ∃ m, ∀ x ∈ Set.Icc 0 1, x^2 + sin x ≥ m := by interval_minimize
example : ∃ M, ∀ x ∈ Set.Icc 0 1, x^2 + sin x ≤ M := by interval_maximize

Or use interactive commands:

import LeanCert.Discovery.Commands

#find_min (fun x => x^2 + Real.sin x) on [0, 1]
#find_max (fun x => x^2 + Real.sin x) on [0, 1]

"I want to prove both upper and lower bounds"

Prove them separately and combine:

theorem exp_lower : ∀ x ∈ Set.Icc (0:ℝ) 1, 1 ≤ Real.exp x := by certify_bound
theorem exp_upper : ∀ x ∈ Set.Icc (0:ℝ) 1, Real.exp x ≤ 3 := by certify_bound

theorem exp_bounded : ∀ x ∈ Set.Icc (0:ℝ) 1, 1 ≤ Real.exp x ∧ Real.exp x ≤ 3 :=
  fun x hx => ⟨exp_lower x hx, exp_upper x hx⟩

"Native syntax vs Expr AST"

Most tactics support native syntax, but some require Expr AST:

Tactic	Native Syntax	Expr AST
certify_bound	✓ Recommended	✓ Supported
multivariate_bound	✓ Recommended	✓ Supported
interval_minimize/maximize	✓ Recommended	✓ Supported
interval_roots	✓ Supported	✓ Works well
root_bound	✓ Supported	✓ Works well
interval_le/ge (low-level)	✗	✓ Required

Native syntax (recommended when it works):

example : ∀ x ∈ Set.Icc (0:ℝ) 1, x * x ≤ 1 := by certify_bound
example : ∀ x ∈ Set.Icc (0:ℝ) 1, Real.exp x ≤ 3 := by certify_bound 15

Expr AST syntax (more control, always works):

open LeanCert.Core in
def I01 : IntervalRat := ⟨0, 1, by norm_num⟩

open LeanCert.Core in
example : ∀ x ∈ I01, Expr.eval (fun _ => x) (Expr.mul (Expr.var 0) (Expr.var 0)) ≤ (1 : ℚ) := by
  certify_bound

When native syntax fails: If you get unification errors with complex expressions (especially with numeric coefficients like 2 * x * x), switch to Expr AST. See Troubleshooting for details.

"I have a sum over vectors/matrices"

Chain simplification tactics to reduce structured expressions before proving bounds:

-- Expand finite sum, simplify vector indexing, then close with ring
example (a : Fin 3 → ℝ) :
    ∑ k ∈ Finset.Icc 0 2, (![a 0, a 1, a 2] : Fin 3 → ℝ) ⟨k, by omega⟩ =
    a 0 + a 1 + a 2 := by
  finsum_expand; vec_simp

Common combinations: - finsum_expand; ring — expand sum, simplify arithmetic - finsum_expand; vec_simp; ring — expand sum, reduce vector indexing, simplify - vec_simp; certify_bound — simplify indexing, then prove bounds