Decision procedures

Plain-language version: Automation and its limits· Computation inside proofs

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

A decision procedure is an algorithm that settles every question in a fixed class, answering yes or no. In Lean such an algorithm is useful only when its yes comes with evidence that the Lean kernel accepts. This page treats five tactics that automate whole classes of goals in Lean 4.34.1: decide, omega, simp, grind and bv_decide. For each it says what the tactic covers, what evidence it hands to the Lean kernel, and what a reader must trust beyond the Lean kernel.

Three kinds of evidence

Every tactic ends by assigning a term to the goal's metavariable, as described on the tactic framework, and the Lean kernel checks that term when the theorem is added. The procedures below differ in the shape of the term.

1. An ordinary proof term. The tactic searches, then assembles a proof from library lemmas. omega, simp and grind work this way. The search is untrusted; only its output is checked.
2. Proof by reflection. A Boolean function is written in Lean and proved correct once. The tactic reduces the goal to the claim that this function returns true on some input, and the Lean kernel confirms the claim by evaluating the function during its definitional equality check. decide works this way.
3. An asserted evaluation. As in reflection, but the function is run by compiled code and its result is added to Lean's environment, its table of definitions and theorems, as a new axiom. bv_decide works this way. The Lean compiler then joins the trusted base.

The command #print axioms tells the three apart: the first two leave only Lean's standard axioms (described on the three axioms), the third leaves an extra one.

decide

A proposition p is decidable when there is an instance of the class Decidable p. The class is an inductive type with two constructors, one carrying a proof of p and one a proof of its negation:

#print Decidable
#synth Decidable (∀ x : Fin 4, x.val * x.val < 10)

Lean 4.34.1 prints:

inductive Decidable : Prop → Type
number of parameters: 1
constructors:
Decidable.isFalse : {p : Prop} → ¬p → Decidable p
Decidable.isTrue : {p : Prop} → p → Decidable p
Nat.decidableForallFin fun x => ↑x * ↑x < 10

Instances compose: a bounded quantifier over Fin 4 is decidable because each instance of its body is, and instance resolution (see type classes and instance resolution) assembles the instance. The tactic decide synthesises such an instance for the goal and reduces it; if it reaches isTrue h, then h proves the goal.

theorem small : 2 ^ 10 = 1024 ∧ 3 < 5 := by decide
#print small
#print axioms small

theorem small : 2 ^ 10 = 1024 ∧ 3 < 5 :=
of_decide_eq_true (id (Eq.refl true))
'small' does not depend on any axioms

The proof term is short because the work is moved into checking it. For Eq.refl true to have type decide p = true, the Lean kernel must reduce decide p to true, which is the computation itself. This is definitional equality put to use. On a false proposition the same evaluation yields a refutation, and the tactic reports it:

example : ∀ x : Fin 5, x.val * x.val < 10 := by decide

error: Tactic `decide` proved that the proposition
  ∀ (x : Fin 5), ↑x * ↑x < 10
is false

The limits follow from the method. The goal may contain no local variables or metavariables; on n + 0 = n for a variable n, Lean says Expected type must not contain free variables and suggests the option +revert, which first moves such variables into the goal as universally quantified ones. Instances defined by well-founded recursion may not reduce, and reduction can get stuck on instances built with rewriting tactics. The option decide +kernel hands the reduction to the Lean kernel directly, and decide +native runs compiled code and admits the result through an axiom. Its documentation says this can be significantly more efficient, but comes "at the cost of increasing the size of the trusted code base".

omega

omega proves goals in linear arithmetic over Int and Nat. It accepts hypotheses of the forms x = y, x < y, x ≤ y and k ∣ x for a literal k, with their negations; it splits both sides into linear combinations of atoms, and for x / k and x % k with a literal k it introduces a new variable together with the two inequalities that bound it.

theorem bound (x y : Nat) (h₁ : x + 2 * y ≤ 10) (h₂ : 3 < x) : y ≤ 3 := by
  omega

example (a b : Int) (h : 2 * a + 1 = 2 * b) : False := by
  omega

example (n : Nat) : n / 2 + n % 2 ≤ n := by
  omega

#print axioms bound

The last line prints 'bound' depends on axioms: [propext, Quot.sound]: the proof is an ordinary term. The method is William Pugh's omega test of 1991, an extension of Fourier–Motzkin variable elimination from the reals to the integers. Eliminating a variable from a set of integer inequalities yields Pugh's real shadow, which may have integer points that lift to no integer solution, and his dark shadow, whose integer points always lift; when the two coincide the elimination is exact.

Lean's implementation states its own limits. Its notes say that it follows Pugh's paper closely but leaves out the dark and grey shadows, so when the real shadow is satisfiable it fails rather than deciding. It prefers to eliminate a variable for which elimination is exact: all upper bounds, or all lower bounds, with unit coefficient. The notes record that failures from the missing shadows appear to be rare in practice. The tactic's documentation accordingly calls it "not yet a full decision procedure". Each derived constraint carries a record of how it was obtained, and when a contradiction appears that record is turned into the proof term.

Products of variables are outside the fragment. omega treats x * y as an atom, an unknown like any other, and, on failure, prints constraints that a counterexample might satisfy:

example (x y : Nat) (h : x * y = 6) : x ≤ 6 := by
  omega

error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  a ≥ 7
where
 a := ↑x

simp

simp is not a decision procedure. It is a rewriting engine: the reference manual describes it as performing inside-out rewriting of terms from a database of simplification rules. The database is the simp set: every theorem marked @[simp], read as an equation to be used from left to right, together with any lemmas named in the call. A goal is closed when it rewrites to True. The option trace.Meta.Tactic.simp.rewrite shows each step:

def rev : List α → List α
  | [] => []
  | a :: as => rev as ++ [a]

@[simp] theorem rev_nil : rev ([] : List α) = [] := rfl
@[simp] theorem rev_cons (a : α) (as : List α) :
    rev (a :: as) = rev as ++ [a] := rfl

set_option trace.Meta.Tactic.simp.rewrite true in
example (a b : Nat) : rev [a, b] = [b, a] := by
  simp

[Meta.Tactic.simp.rewrite] rev_cons:1000:
      rev [a, b]
    ==>
      rev [b] ++ [a]
[Meta.Tactic.simp.rewrite] rev_cons:1000:
      rev [b]
    ==>
      rev [] ++ [b]
[Meta.Tactic.simp.rewrite] rev_nil:1000:
      rev []
    ==>
      []
[Meta.Tactic.simp.rewrite] List.nil_append:1000:
      [] ++ [b]
    ==>
      [b]
[Meta.Tactic.simp.rewrite] List.cons_append:1000:
      [b] ++ [a]
    ==>
      b :: ([] ++ [a])
[Meta.Tactic.simp.rewrite] List.nil_append:1000:
      [] ++ [a]
    ==>
      [a]
[Meta.Tactic.simp.rewrite] eq_self:1000:
      [b, a] = [b, a]
    ==>
      True

The number after each lemma name is its priority. Two of the lemmas come from this page, the rest from Lean's library. The variant simp? reports a simp only [...] call naming just the lemmas used; pasted in its place, it makes the proof independent of later changes to the library's simp set. Whether simp succeeds depends on the simp set as much as on the goal: it answers no question by itself. Its proof is assembled from the lemmas it used and is checked by the Lean kernel like any other term.

grind

grind is part of core Lean in version 4.34.1 and needs no import. Its documentation calls it inspired by modern SMT solvers. It keeps one shared collection of facts, groups terms known to be equal by congruence closure, instantiates theorems by E-matching (matching a theorem's pattern modulo the equalities known so far), splits cases, and passes facts to specialised solvers for linear integer arithmetic, for commutative rings and fields, and for linear arithmetic (its linarith component). The reference manual states that it "produces ordinary Lean proof terms for every fact it adds".

def f (a : Nat) : Nat := a + 1
def g (a : Nat) : Nat := a - 1

@[grind =] theorem g_f (x : Nat) : g (f x) = x := by
  simp [f, g]

theorem grind_demo {a b : Nat} (h : f b = a) : g a = b := by
  grind

example {x y : Int} : 2 * x + 4 * y ≠ 5 := by
  grind

#print axioms grind_demo

The attribute @[grind =] makes the left side g (f x) a pattern. The goal mentions g a, not g (f b); but h puts a and f b in one equality class, so the pattern matches modulo that equality and congruence closure finishes the proof. The second example, taken from the tactic's documentation, is linear integer arithmetic: 2 * x + 4 * y is even and 5 is not. The last line prints 'grind_demo' depends on axioms: [propext, Classical.choice, Quot.sound], the standard three and nothing more. Its documentation warns that grind is not designed for problems whose search space explodes combinatorially, and points to bv_decide for bit-level and combinatorial problems.

bv_decide

bv_decide closes goals about fixed-width bit vectors (BitVec n) and Bool: the Lean counterpart of the SMT-LIB logic QF_BV. It needs import Std.Tactic.BVDecide, and on failure it prints a counterexample. Its implementation notes give the steps. It starts a proof by contradiction, normalises the hypotheses with a simp set, and represents the problem as a Lean value of a syntax-tree type. A verified bit-blaster turns that value into an and-inverter graph and then into a formula in conjunctive normal form. The SAT solver CaDiCaL, which is shipped beside the lean executable, is asked for an LRAT proof that the formula is unsatisfiable. That proof is checked by an LRAT checker with a soundness proof in Lean, and the proofs so far are chained back to the goal.

import Std.Tactic.BVDecide

theorem add_as_xor (x y : BitVec 8) :
    x + y = (x ^^^ y) + ((x &&& y) <<< 1) := by
  bv_decide

#print axioms add_as_xor
#print add_as_xor._native.bv_decide.ax_1_5

'add_as_xor' depends on axioms: [propext, Classical.choice, Quot.sound, add_as_xor._native.bv_decide.ax_1_5]
axiom add_as_xor._native.bv_decide.ax_1_5 : Std.Tactic.BVDecide.Reflect.verifyBVExpr add_as_xor._expr_def_1_1
    add_as_xor._cert_def_1_1 =
  true

The output states the trust story exactly. The fourth axiom says that one Boolean function, verifyBVExpr, returns true on the encoded problem and on the certificate string the solver produced. In Lean's library, verifyBVExpr bit-blasts the problem and checks the certificate against the resulting formula, and the theorem unsat_of_verifyBVExpr_eq_true proves that a true result means the problem is unsatisfiable. So the result relies on three things: the Lean kernel, which checks the soundness theorems and the chain of reasoning around the axiom; the compiled evaluation of verifyBVExpr, which is what the axiom asserts; and therefore the Lean compiler that produced that code, together with any definition whose compiled form is replaced by another implementation through @[implemented_by], a dependency the documentation of decide +native spells out for the same mechanism. The implementation notes say so: the result of the compiled check is added as an axiom, "thus adding the Lean compiler to the trusted code base". The SAT solver is not trusted. A wrong certificate makes the check return false and the tactic fails. The Lean kernel does not repeat the bit-level computation itself.

The reference manual's page on validating proofs records that up to version 4.28.0 every such use showed up in #print axioms as one shared axiom, Lean.trustCompiler, and that since 4.29.0 these tactics instead introduce one dedicated axiom for each computation, as above. In 4.34.1 the older primitive Lean.ofReduceBool still exists; #check @Lean.ofReduceBool answers with the warning that native reduction inside the Lean kernel is deprecated. For the older mechanism the manual states that external checkers cannot check such proofs, having no access to the Lean compiler, and that proofs needing that level of checking must avoid native evaluation. Under the newer one a checker sees, in the list of axioms, exactly which computation it is asked to take on trust. Proof export and independent checkers takes this up.

A false bit-vector claim is refuted with values:

import Std.Tactic.BVDecide

example (x y : BitVec 4) : x * y = x + y := by
  bv_decide

error: The prover found a counterexample, consider the following assignment:
x = 15#4
y = 15#4

Indeed 15 × 15 = 225, which is 1 modulo 16, while 15 + 15 = 30, which is 14.

Side by side

Tactic	Covers	Evidence	Trusted beyond the Lean kernel
decide	propositions with a Decidable instance that reduces	reflection, evaluated by the Lean kernel	nothing
omega	linear arithmetic over Int and Nat (incomplete)	ordinary proof term	nothing
simp	whatever the simp set rewrites to True	ordinary proof term	nothing
grind	equalities, theorem instances, case splits, arithmetic	ordinary proof term	nothing
bv_decide	fixed-width bit vectors and Bool	asserted evaluation of a verified checker	the Lean compiler and the compiled code

In every row the search can be wrong without harm: a mistaken search produces a term the Lean kernel rejects, or no term. Only the last row moves part of the checking out of the Lean kernel.

Next

Syntax extension and hygienic macros shows how new notation, and new tactics, are added to the language.