Lean Tactics Reference

Complete reference for all LeanCert tactics.

Bound Proving

`certify_bound`

Proves universal bounds over intervals using rational interval arithmetic.

import LeanCert.Tactic.IntervalAuto

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

-- With Taylor depth (higher = tighter bounds, slower)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 2.72 := by certify_bound 15

-- Lower bounds
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ Real.exp x := by certify_bound

-- Strict inequalities
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x < 3 := by certify_bound

Note: interval_bound is an alias for backward compatibility.

Parameters:

Parameter	Type	Default	Description
`depth`	`ℕ`	10	Taylor series depth for transcendentals

Supported functions: +, -, *, /, ^ (rational exponents), abs, max, min, sin, cos, exp, sqrt, sinh, cosh, tanh, atan, arsinh, atanh, sinc, erf, log, inv

Note on rational exponents: general rational exponents like x^(1/3) are lowered to exp(log(x) * q), which requires the base to be provably positive from interval bounds.

`certify_kernel`

Proves bounds using dyadic arithmetic. Attempts kernel-only verification (decide) first, falls back to native_decide.

import LeanCert.Tactic.DyadicAuto

-- Default precision (53 bits)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, x * x ≤ 2 := by certify_kernel

-- Custom precision (bits)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 2.72 := by certify_kernel 100

-- Convenience variants
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 2.72 := by certify_kernel_precise  -- 100 bits
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, x * x ≤ 2 := by certify_kernel_quick           -- 30 bits

Note: fast_bound is an alias for backward compatibility.

Trust levels:

Verification	Trusted Components
`decide` (kernel)	Lean kernel only
`native_decide` (fallback)	Lean kernel + compiler

Diagnostics: Enable set_option trace.certify_kernel true to see why kernel verification fails.

`interval_decide`

Proves point inequalities involving specific numbers (transcendentals like π, e).

import LeanCert.Tactic.IntervalAuto

example : Real.pi < 3.15 := by interval_decide
example : Real.exp 1 < 3 := by interval_decide
example : Real.sin 1 + Real.cos 1 < 1.5 := by interval_decide
example : Real.sqrt 2 < 1.42 := by interval_decide

Use this for concrete values. For universally quantified bounds, use certify_bound.

Counter-Example Search

`interval_refute`

Searches for counter-examples to disprove false bounds.

import LeanCert.Tactic.Refute

-- This bound is false (x² can reach 4 on [-2, 2])
example : ∀ x ∈ Set.Icc (-2 : ℝ) 2, x * x ≤ 3 := by
  interval_refute
  -- Output: Counter-example found at x ≈ ±2, where x² = 4 > 3

Output types:

Result	Meaning
`Verified`	Rigorous proof that bound fails at this point
`Candidate`	Likely counter-example (may be precision artifact)

Configuration:

-- With custom settings
example : ... := by
  interval_refute (config := { maxIterations := 100, tolerance := 1e-6 })

Discovery Tactics

`interval_minimize` / `interval_maximize`

Proves existence of global minimum/maximum via branch-and-bound optimization.

import LeanCert.Tactic.Discovery

-- Find and prove a lower bound exists
example : ∃ m, ∀ x ∈ Set.Icc (0 : ℝ) 2, x * x - x ≥ m := by
  interval_minimize

-- With Taylor depth
example : ∃ m, ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.sin x ≥ m := by
  interval_minimize 15

`interval_roots`

Proves root existence via sign change detection (Intermediate Value Theorem).

Native syntax (recommended):

import LeanCert.Tactic.Discovery

-- Prove √2 exists in [1, 2]
example : ∃ x ∈ Set.Icc (1 : ℝ) 2, x^2 - 2 = 0 := by
  interval_roots

-- Also supports f(x) = c form
example : ∃ x ∈ Set.Icc (1 : ℝ) 2, x^2 = 2 := by
  interval_roots

-- Transcendental roots
example : ∃ x ∈ Set.Icc (1 : ℝ) 2, Real.cos x = 0 := by
  interval_roots

Expr AST syntax (also supported):

open LeanCert.Core

def I12 : IntervalRat := ⟨1, 2, by norm_num⟩

example : ∃ x ∈ I12, Expr.eval (fun _ => x)
    (Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.neg (Expr.const 2))) = 0 := by
  interval_roots

How it works: 1. Evaluates expression at interval endpoints 2. Detects sign change (f(lo) < 0 < f(hi) or vice versa) 3. Applies IVT to prove existence

`interval_unique_root`

Proves root uniqueness via Newton contraction mapping.

Native syntax (recommended):

import LeanCert.Tactic.Discovery

-- Prove there's exactly one root of x² - 2 in [1, 2]
example : ∃! x ∈ Set.Icc (1 : ℝ) 2, x^2 - 2 = 0 := by
  interval_unique_root

Expr AST syntax (also supported):

open LeanCert.Core

def I12 : IntervalRat := ⟨1, 2, by norm_num⟩
def expr_x2_minus_2 : Expr := Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.neg (Expr.const 2))

example : ∃! x ∈ I12, Expr.eval (fun _ => x) expr_x2_minus_2 = 0 := by
  interval_unique_root

How it works: 1. Computes Newton operator N(x) = x - f(x)/f'(x) 2. Verifies N maps interval into itself 3. Verifies |N'(x)| < 1 (contraction) 4. Banach fixed-point theorem gives uniqueness

`interval_integrate`

Proves bounds on definite integrals via verified Riemann sums.

import LeanCert.Tactic.Discovery

open LeanCert.Core LeanCert.Validity.Integration

def I01 : IntervalRat := ⟨0, 1, by norm_num⟩

-- Prove integral is contained in computed interval
example : ∫ x in (I01.lo : ℝ)..(I01.hi : ℝ),
    Expr.eval (fun _ => x) (Expr.mul (Expr.var 0) (Expr.var 0)) ∈
    integrateInterval1Core (Expr.mul (Expr.var 0) (Expr.var 0)) I01 {} := by
  interval_integrate

How it works: 1. Partitions interval into subintervals 2. Computes interval bounds on each partition 3. Sums (width × bound) for rigorous over/under-approximation

Note: The tactic proves membership in the computed interval, not a direct inequality.

Interactive Commands

These commands are for exploration in the editor, not for proofs. Use them to discover bounds before writing theorems.

`#bounds`

Find both minimum and maximum of a function on an interval.

import LeanCert.Discovery.Commands

#bounds (fun x => x^2 + Real.sin x) on [-2, 2]

Output:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
#bounds Results
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
  f(x) ∈ [-5, 5]

  Minimum: -5 (± 4.77)
  Maximum: 5 (± 0.91)

  Total iterations: 32
  Verified: ✓
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

`#find_min` / `#find_max`

Find the minimum or maximum separately, with optional precision control.

import LeanCert.Discovery.Commands

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

-- Higher precision for tighter bounds
#find_max (fun x => Real.exp x) on [0, 1] precision 20

Syntax:

#find_min <function> on [<lo>, <hi>]
#find_min <function> on [<lo>, <hi>] precision <n>

Parameters: - function: A lambda (fun x => ...) with the expression - lo, hi: Integer bounds (rationals not supported in syntax) - precision: Optional Taylor depth (default: 10)

`#explore`

Interactive function analysis in the editor. Shows range, extrema, and roots.

import LeanCert.Tactic.Discovery

-- Explore sin(x) on [0, 4]
#explore (Expr.sin (Expr.var 0)) on [0, 4]

Output includes: - Domain and computed range - Global minimum and maximum with locations - Sign changes (potential roots) - Monotonicity information

Comparison Table

Tactic	Purpose	Trust	Speed
`certify_bound`	Prove bounds	`native_decide`	Medium
`certify_kernel`	Prove bounds	`decide` / fallback	Fast
`interval_decide`	Point inequalities	`native_decide`	Fast
`interval_refute`	Find counter-examples	Verified	Slow
`interval_roots`	Prove root exists	`native_decide`	Medium
`interval_unique_root`	Prove root unique	`native_decide`	Slow
`interval_minimize`	Prove min exists	`native_decide`	Slow
`interval_maximize`	Prove max exists	`native_decide`	Slow
`interval_integrate`	Prove integral bounds	`native_decide`	Medium
`discover`	Auto-route min/max	`native_decide`	Slow
`interval_minimize_mv`	Multivariate min	`native_decide`	Slow
`interval_maximize_mv`	Multivariate max	`native_decide`	Slow
`multivariate_bound`	N-dim bounds	`native_decide`	Medium
`root_bound`	Prove f(x) ≠ 0	`native_decide`	Medium
`interval_bound_subdiv`	Tight bounds via subdivision	`native_decide`	Slow
`interval_argmax`	Find maximizer point	`native_decide`	Slow
`interval_argmin`	Find minimizer point	`native_decide`	Slow
`vec_simp`	Simplify vector indexing	`dsimp`	Fast
`finsum_expand`	Expand finite sums	`native_decide`	Fast

Additional Tactics

`discover`

Meta-tactic that analyzes the goal and automatically routes to interval_minimize or interval_maximize.

import LeanCert.Tactic.Discovery

-- Automatically detects ≥ m and calls interval_minimize
example : ∃ m : ℚ, ∀ x ∈ I, f(x) ≥ m := by discover

-- Automatically detects ≤ M and calls interval_maximize
example : ∃ M : ℚ, ∀ x ∈ I, f(x) ≤ M := by discover

`interval_minimize_mv` / `interval_maximize_mv`

Multivariate versions of minimize/maximize for N-dimensional domains.

import LeanCert.Tactic.Discovery

-- Find minimum over 2D domain
example : ∃ m : ℚ, ∀ x ∈ Set.Icc (0:ℝ) 1, ∀ y ∈ Set.Icc (0:ℝ) 1,
    x*x + y*y ≥ m := by
  interval_minimize_mv

-- Find maximum over 2D domain
example : ∃ M : ℚ, ∀ x ∈ Set.Icc (0:ℝ) 1, ∀ y ∈ Set.Icc (0:ℝ) 1,
    x + y ≤ M := by
  interval_maximize_mv

Uses more samples (300) and iterations (2000) than univariate versions.

`multivariate_bound`

Proves bounds over multi-variable domains directly.

import LeanCert.Tactic.IntervalAuto

-- Prove x + y ≤ 2 on [0,1] × [0,1]
example : ∀ x ∈ Set.Icc (0:ℝ) 1, ∀ y ∈ Set.Icc (0:ℝ) 1,
    x + y ≤ (2 : ℚ) := by
  multivariate_bound

`root_bound`

Proves absence of roots by showing a function is strictly positive or negative.

Native syntax (recommended):

import LeanCert.Tactic.IntervalAuto

-- x² + 1 ≠ 0 on [0, 1] (always positive)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, x * x + 1 ≠ 0 := by
  root_bound

-- exp(x) ≠ 0 on [0, 1]
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≠ 0 := by
  root_bound 15

Expr AST syntax (also supported):

open LeanCert.Core

def I01 : IntervalRat := ⟨0, 1, by norm_num⟩

example : ∀ x ∈ I01, Expr.eval (fun _ => x)
    (Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.const 1)) ≠ (0 : ℝ) := by
  root_bound

`interval_bound_subdiv`

Proves bounds using progressive subdivision when direct interval evaluation is too loose.

import LeanCert.Tactic.IntervalAuto

-- Tighter bound requiring subdivision
example : ∀ x ∈ Set.Icc (0:ℝ) 1, Real.exp x ≤ (272/100 : ℚ) := by
  interval_bound_subdiv 15 3  -- Taylor depth 15, subdivision depth 3

Parameters:

Parameter	Type	Default	Description
`depth`	`ℕ`	10	Taylor series depth
`subdivDepth`	`ℕ`	2	Number of subdivision levels

`interval_argmax` / `interval_argmin`

Find the point where a function achieves its maximum/minimum.

interval_argmax - Native syntax (recommended):

import LeanCert.Tactic.Discovery

-- Find the maximizer of x² on [-1,1] (argmax at endpoints x = ±1)
example : ∃ x ∈ Set.Icc (-1 : ℝ) 1, ∀ y ∈ Set.Icc (-1 : ℝ) 1,
    y * y ≤ x * x := by
  interval_argmax

-- Linear function: max of 2x+1 on [0,1] (argmax at x=1)
example : ∃ x ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ Set.Icc (0 : ℝ) 1,
    2 * y + 1 ≤ 2 * x + 1 := by
  interval_argmax

interval_argmin - Native syntax (recommended):

-- Find the minimizer of x on [0,1] (argmin at x=0)
example : ∃ x ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ Set.Icc (0 : ℝ) 1,
    x ≤ y := by
  interval_argmin

Expr AST syntax (also supported):

open LeanCert.Core

def I_neg1_1 : IntervalRat := ⟨-1, 1, by norm_num⟩
def I01 : IntervalRat := ⟨0, 1, by norm_num⟩

-- Argmax with Expr AST
example : ∃ x ∈ I_neg1_1, ∀ y ∈ I_neg1_1,
    Expr.eval (fun _ => y) (Expr.mul (Expr.var 0) (Expr.var 0)) ≤
    Expr.eval (fun _ => x) (Expr.mul (Expr.var 0) (Expr.var 0)) := by
  interval_argmax

-- Argmin with Expr AST
example : ∃ x ∈ I01, ∀ y ∈ I01,
    Expr.eval (fun _ => x) (Expr.var 0) ≤
    Expr.eval (fun _ => y) (Expr.var 0) := by
  interval_argmin

How it works: 1. Runs branch-and-bound optimization to find candidate optimizer xOpt 2. Evaluates f(xOpt) to get a concrete bound c 3. For argmax: Proves ∀ y ∈ I, f(y) ≤ c and c ≤ f(xOpt), then applies transitivity 4. For argmin: Proves ∀ y ∈ I, c ≤ f(y) and f(xOpt) ≤ c, then applies transitivity

Limitations: - Works best when the argmax/argmin is at a rational point (e.g., interval endpoints) - For transcendental functions, may require higher Taylor depth - For interior optima at irrational points, consider using interval_maximize/interval_minimize instead

Low-Level Manual Tactics

For fine-grained control, use these macros from LeanCert.Tactic.Interval:

import LeanCert.Tactic.Interval

open LeanCert.Core LeanCert.Engine

def xSq : Expr := Expr.mul (Expr.var 0) (Expr.var 0)
def xSq_supp : ExprSupportedCore xSq :=
  ExprSupportedCore.mul (ExprSupportedCore.var 0) (ExprSupportedCore.var 0)

-- Manual bounds with explicit AST and support proof
example : ∀ x ∈ I01, Expr.eval (fun _ => x) xSq ≤ (1 : ℚ) := by
  interval_le xSq, xSq_supp, I01, 1

example : ∀ x ∈ I01, (0 : ℚ) ≤ Expr.eval (fun _ => x) xSq := by
  interval_ge xSq, xSq_supp, I01, 0

Macro	Purpose
`interval_le`	`∀ x ∈ I, f(x) ≤ c`
`interval_ge`	`∀ x ∈ I, c ≤ f(x)`
`interval_lt`	`∀ x ∈ I, f(x) < c`
`interval_gt`	`∀ x ∈ I, c < f(x)`
`interval_le_pt`	Pointwise `f(x) ≤ c` given `x ∈ I`
`interval_ge_pt`	Pointwise `c ≤ f(x)` given `x ∈ I`

Extended (noncomputable) versions for expressions with exp: interval_ext_le, interval_ext_ge, interval_ext_lt, interval_ext_gt

These reduce the goal to a rational inequality that must be proved manually.

Simplification Tactics

`vec_simp`

Simplifies vector indexing expressions with explicit Fin.mk constructors using a custom dsimproc that extracts the natural number from Fin.mk n proof and walks the vecCons chain directly.

import LeanCert.Tactic.VecSimp

-- Basic indexing: reduces ![a, b, c] ⟨i, proof⟩ to the i-th element
example : (![1, 2, 3] : Fin 3 → ℕ) ⟨0, by omega⟩ = 1 := by vec_simp
example : (![1, 2, 3] : Fin 3 → ℕ) ⟨1, by omega⟩ = 2 := by vec_simp
example : (![1, 2, 3] : Fin 3 → ℕ) ⟨2, by omega⟩ = 3 := by vec_simp

-- Symbolic elements
example (a b c : ℝ) : (![a, b, c] : Fin 3 → ℝ) ⟨1, by omega⟩ = b := by vec_simp

-- Longer vectors
example : (![1, 2, 3, 4, 5] : Fin 5 → ℕ) ⟨3, by omega⟩ = 4 := by vec_simp

-- In expressions (simplifies all vector indexing)
example (a b c : ℝ) : (![a, b, c] : Fin 3 → ℝ) ⟨0, by omega⟩ + 1 = a + 1 := by vec_simp

-- Combines well with ring for algebraic manipulation
example (a₀ a₁ : ℝ) :
    (![a₀, a₁] : Fin 2 → ℝ) ⟨0, by omega⟩ * (![a₀, a₁] : Fin 2 → ℝ) ⟨1, by omega⟩ +
    (![a₀, a₁] : Fin 2 → ℝ) ⟨1, by omega⟩ * (![a₀, a₁] : Fin 2 → ℝ) ⟨0, by omega⟩ = 2 * a₀ * a₁ := by
  vec_simp; ring

Why this exists: Mathlib's cons_val simproc uses int? to extract indices, which only matches numeric literals like 0, 1, 2. It doesn't match explicit Fin.mk applications like ⟨0, by omega⟩, which commonly appear in proofs (e.g., from finsum_expand or matrix indexing). The vec_simp dsimproc fills that gap by pattern-matching on Fin.mk directly.

How it works: A dsimproc (VecSimp.vecConsFinMk) matches applications of vecCons to a Fin.mk n proof index, extracts n, and recursively traverses the cons chain to return the n-th element. This is combined with standard Mathlib vector lemmas (cons_val_zero, cons_val_one, head_cons).

`finsum_expand`

Expands finite sums over Finsets into explicit additions.

import LeanCert.Tactic.FinSumExpand

-- Interval finsets (Icc = closed-closed)
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Icc 1 3, f k = f 1 + f 2 + f 3 := by finsum_expand

-- Single element
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Icc 5 5, f k = f 5 := by finsum_expand

-- Ico (closed-open)
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Ico 1 4, f k = f 1 + f 2 + f 3 := by finsum_expand

-- Ioc (open-closed)
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Ioc 1 3, f k = f 2 + f 3 := by finsum_expand

-- Ioo (open-open)
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Ioo 1 4, f k = f 2 + f 3 := by finsum_expand

-- Iic (unbounded below, closed) - for ℕ, means [0, n]
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Iic 2, f k = f 0 + f 1 + f 2 := by finsum_expand

-- Iio (unbounded below, open) - for ℕ, means [0, n)
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Iio 3, f k = f 0 + f 1 + f 2 := by finsum_expand

-- Empty intervals
example (f : ℕ → ℝ) : ∑ k ∈ Finset.Ico 5 5, f k = 0 := by finsum_expand

-- Explicit finsets
example (f : ℕ → ℝ) : ∑ k ∈ ({1, 3, 7} : Finset ℕ), f k = f 1 + f 3 + f 7 := by finsum_expand

-- Combines with ring for evaluation
example : ∑ k ∈ Finset.Icc 1 4, (fun n : ℕ => (n : ℝ)) k = 10 := by finsum_expand; ring

-- Power series patterns
example (a : ℕ → ℝ) (r : ℝ) : ∑ n ∈ Finset.Icc 1 3, |a n| * r ^ n =
    |a 1| * r ^ 1 + |a 2| * r ^ 2 + |a 3| * r ^ 3 := by finsum_expand

Supported interval types:

Interval	Meaning	Example
`Finset.Icc a b`	[a, b] closed-closed	`Icc 1 3` → {1, 2, 3}
`Finset.Ico a b`	[a, b) closed-open	`Ico 1 4` → {1, 2, 3}
`Finset.Ioc a b`	(a, b] open-closed	`Ioc 1 3` → {2, 3}
`Finset.Ioo a b`	(a, b) open-open	`Ioo 1 4` → {2, 3}
`Finset.Iic n`	[0, n] for ℕ	`Iic 2` → {0, 1, 2}
`Finset.Iio n`	[0, n) for ℕ	`Iio 3` → {0, 1, 2}
`{a, b, ...}`	Explicit set	`{1, 3, 7}`
`∑ i : Fin n, f i`	Fin univ	`Fin 3` → {0, 1, 2}

How it works: Uses Finset.sum_cons and Finset.sum_empty rewriting combined with native_decide to evaluate finset membership. For Fin n sums, uses Fin.sum_univ_ofNat when n is a literal.

Why this exists: When proving bounds involving finite sums, you often need to expand them for arithmetic simplification. Without this tactic, you'd need to manually define "bridge lemmas" for each specific range.

Common Patterns

Proving a function is bounded

-- Upper and lower bound
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ Real.sin x ∧ Real.sin x ≤ 1 := by
  constructor <;> certify_bound

Proving a root exists and is unique

-- First existence, then uniqueness
example : ∃ x ∈ I, f x = 0 := by interval_roots
example : ∃! x ∈ I, f x = 0 := by interval_unique_root

Debugging failed proofs

set_option trace.certify_bound true    -- See computation details
set_option trace.certify_kernel true   -- See kernel verification status

-- If bound too tight, try:
-- 1. Increase Taylor depth: certify_bound 20
-- 2. Use certify_kernel_precise for more bits
-- 3. Use interval_refute to check if bound is actually false

Lean Tactics Reference

Bound Proving

certify_bound

certify_kernel

interval_decide

Counter-Example Search

interval_refute

Discovery Tactics

interval_minimize / interval_maximize

interval_roots

interval_unique_root

interval_integrate

Interactive Commands

#bounds

#find_min / #find_max

#explore

Comparison Table

Additional Tactics

discover

interval_minimize_mv / interval_maximize_mv

multivariate_bound

root_bound

interval_bound_subdiv

interval_argmax / interval_argmin

Low-Level Manual Tactics

Simplification Tactics

vec_simp

finsum_expand

Common Patterns

Proving a function is bounded

Proving a root exists and is unique

Debugging failed proofs

`certify_bound`

`certify_kernel`

`interval_decide`

`interval_refute`

`interval_minimize` / `interval_maximize`

`interval_roots`

`interval_unique_root`

`interval_integrate`

`#bounds`

`#find_min` / `#find_max`

`#explore`

`discover`

`interval_minimize_mv` / `interval_maximize_mv`

`multivariate_bound`

`root_bound`

`interval_bound_subdiv`

`interval_argmax` / `interval_argmin`

`vec_simp`

`finsum_expand`