17. The grind tactic
The grind tactic uses techniques inspired by modern SMT solvers to automatically construct proofs.
It produces proofs by incrementally collecting sets of facts, deriving new facts from the existing ones using a set of cooperating techniques.
Behind the scenes, all proofs are by contradiction, so there is no operational distinction between the expected conclusion and the premises; grind always attempts to derive a contradiction.
Picture a virtual whiteboard.
Every time grind discovers a new equality, inequality, or Boolean literal it writes that fact on the board, merges equivalent terms into buckets, and invites each engine to read from—and add back to—the shared whiteboard.
In particular, because all true propositions are equal to True and all false propositions are equal to False, grind tracks a set of known facts as part of tracking equivalence classes.
The cooperating engines are:
-
guided case analysis, and
-
a suite of satellite theory solvers, including both linear integer arithmetic and commutative rings.
Like other tactics, grind produces ordinary Lean proof terms for every fact it adds.
Lean’s standard library is already annotated with @[grind] attributes, so common lemmas are discovered automatically.
grind is not designed for goals whose search space explodes combinatorially—think large‑n pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints.
Such encodings require thousands (or millions) of case‑splits that overwhelm grind’s branching search.
For bit‑level or pure Boolean combinatorial problems, use bv_decide. The bv_decide tactic calls a state‑of‑the‑art SAT solver (e.g. CaDiCaL or Kissat) and then returns a compact, machine‑checkable certificate.
All heavy search happens outside Lean; the certificate is replayed and verified inside Lean, so trust is preserved (verification time scales with certificate size).
Congruence Closure
Algebraic Reasoning
This proof uses grind's commutative ring solver.
example [CommRing α] [NoNatZeroDivisors α] (a b c : α) :
a + b + c = 3 →
a ^ 2 + b ^ 2 + c ^ 2 = 5 →
a ^ 3 + b ^ 3 + c ^ 3 = 7 →
a ^ 4 + b ^ 4 = 9 - c ^ 4 := α:Type u_1inst✝¹:CommRing αinst✝:NoNatZeroDivisors αa:αb:αc:α⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 = 9 - c ^ 4
All goals completed! 🐙
Finite-Field Reasoning
Arithmetic operations on Fin overflow, wrapping around to 0 when the result would be outside the bound.
grind can use this fact to prove theorems such as this:
example (x y : Fin 11) :
x ^ 2 * y = 1 →
x * y ^ 2 = y →
y * x = 1 := x:Fin 11y:Fin 11⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1
All goals completed! 🐙
Linear Integer Arithmetic with Case Analysis
