Induction, as the machine sees it

Technical version: Inductive types and recursors· Structural and well-founded recursion

Proof by induction is the standard way to prove something about every natural number. In Lean it is not a separate rule added to the logic. It is the recursion principle of building things from constructors, put to work on proofs. This page shows the two cases, the tactic that sets them up, and what Lean records once the proof is finished.

The familiar form

To prove that a statement holds for every natural number, two things are enough. First, prove it for 0: the base case. Second, prove that whenever it holds for a number k, it also holds for k + 1: the induction step, in which "it holds for k" is the induction hypothesis. Then the statement holds for 0, so for 1, so for 2, and so on, with no number left out.

Why it is the recursion principle

The natural numbers in Lean are made by two rules: zero, and the successor of a number already made. From those rules Lean derives a recursion principle: to produce something for every number, give it for zero, and give a way to go from what it is for n to what it is for n + 1. Now let the thing produced be a proof of the statement about n. The principle then says: given a proof for zero, and a way to turn a proof for k into a proof for k + 1, there is a proof for every number. That is induction, word for word. Theorem Proving in Lean 4 describes the induction principle as just a special case of the recursion principle, the case in which what is produced is a proof.

Induction is therefore not an extra axiom. It comes with the type of natural numbers, derived from its two constructors, and the same holds for every type defined by constructors.

Two equations that look alike

Addition in Lean is defined by recursion on the second number: n + 0 is n, and n + (m + 1) is (n + m) + 1. That makes one equation true by computation alone. rfl is the proof that says "both sides compute to the same thing", and Lean accepts it here:

example (n : Nat) : n + 0 = n := rfl

The mirror image is refused:

example (n : Nat) : 0 + n = n := by rfl

Lean 4.34.1 replies Tactic `rfl` failed: The left-hand side, then that 0 + n "is not definitionally equal to the right-hand side" n. The reason is plain once the definition is in view. To compute 0 + n, Lean must know whether n is zero or a successor, and n is unknown. Both statements are true; only the first is true by computation. The second needs induction.

The induction tactic

theorem zero_add' (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ, ih]

#print zero_add'

The line induction n replaces one task by two, one for each way a natural number can be made, and adds an induction hypothesis wherever a constructor takes a number of the same type. Inside the two cases, Lean's display of what remains to be proved reads:

case zero
⊢ 0 + 0 = 0

case succ
k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

The symbol ⊢ marks what must be shown; the lines above it are what may be used. The base case, 0 + 0 = 0, holds by computation, and rfl closes it. In the step, Lean has named the number k and the induction hypothesis ih. The tactic rw rewrites the goal with an equation. First it uses Nat.add_succ, the fact that n + (m + 1) equals (n + m) + 1, which turns the goal into (0 + k) + 1 = k + 1. Then it uses ih to replace 0 + k by k. The two sides now agree, and rw closes the goal by itself. How goals are displayed and filled is the subject of holes and goals.

What Lean records

The #print line shows the proof that Lean actually kept:

theorem zero_add' : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Nat.add_succ 0 k)))
        (Eq.mpr (id (congrArg (fun _a => _a.succ = k + 1) ih)) (Eq.refl k.succ)))
    n

The tactic script is gone. In its place is a single expression, and at its head stands Nat.recAux. Asked to print that name, Lean shows that it is Nat.rec, the recursion principle itself, written with 0 and n + 1 in place of the constructor names. Its first argument, Eq.refl (0 + 0), is the base case: 0 + 0 computes to 0, so the equation is an instance of a thing being equal to itself. Its second, fun k ih => ..., is the step: a function that takes a number k and a proof for k and returns a proof for k + 1. The rest of the step records the two rewrites. This expression, and not the script, is what the Lean kernel checks.

A formula from school

The sum 1 + 2 + ... + n is half of n(n + 1). In whole numbers it is cleaner to say that twice the sum is n(n + 1):

def sumTo : Nat → Nat
  | 0     => 0
  | n + 1 => (n + 1) + sumTo n

#eval sumTo 100

theorem two_mul_sumTo (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [sumTo, Nat.mul_add, Nat.add_mul] at *
    omega

The #eval line prints 5050, which is half of 100 × 101. The proof has the same two cases. The base case holds by computation. In the step, simp only unfolds sumTo once and multiplies out the brackets, in the goal and in the induction hypothesis alike, and omega, an arithmetic procedure described in automation and its limits, finishes the sum.

Other types, other inductions

Every type defined by constructors has its own recursor, so every such type has its own induction. For lists: prove the statement for the empty list, then prove it for a list with an item in front, assuming it for the rest. For the trees of building things from constructors: prove it for a leaf, then for a node, assuming it for both subtrees, since the recursor for trees supplies a hypothesis for each. The induction tactic works the same way for all of them.

Next

• Tactics: what the commands after by are, and what they produce.
• Inductive types and recursors: the technical treatment.