3. Induction: Proof by Induction🔗

This chapter shows how to carry out proofs by induction, one of the most fundamental reasoning tools in computer science and mathematics, in Lean.

3.1. Separate Compilation🔗

Lean will first need to compile Basics.lean so it can be imported here — detailed instructions are in the full version of this chapter...

import LF.Basics

3.2. Review🔗

We reopen the namespace from the previous chapter to group this chapter's definitions and theorems with the custom natural-number development and keep their names distinct from the standard library.

Now let's review what we learned in Basics using some quiz questions and an exercise.

namespace NatPlayground.Nat

Quiz

Recall the definition of or, which has notation || and is not marked @[irreducible]:

def or (b1 : Bool) (b2 : Bool) : Bool :=
  match b1 with
  | true => true
  | false => b2

To prove the following theorem, which tactics will we need besides rfl?

theorem review₁ : (true || false) = true

(A) none

(B) rewrite

(D) both rewrite and cases

(E) can't be done with the tactics we've seen.

Show solution

theorem review₁ : (true || false) = true := by⊢ (true || false) = true rflAll goals completed! 🐙

Quiz

What about the next one?

theorem review₂ (b : Bool) : (true || b) = true

Which tactics do we need besides rfl?

(A) none

(B) rewrite

(D) both rewrite and cases

(E) can't be done with the tactics we've seen.

Show solution

theorem review₂ (b : Bool) : (true || b) = true := byb:Bool⊢ (true || b) = true rflAll goals completed! 🐙

Quiz

What if we change the order of the arguments of ||?

theorem review₃ (b : Bool) : (b || true) = true

Which tactics do we need besides rfl?

(A) none

(B) rewrite

(D) both rewrite and cases

(E) can't be done with the tactics we've seen.

Show solution

theorem review₃ (b : Bool) : (b || true) = true := byb:Bool⊢ (b || true) = true
  cases b with
  | false =>false⊢ (false || true) = true rflAll goals completed! 🐙
  | true  =>true⊢ (true || true) = true rflAll goals completed! 🐙

def add (n : Nat) (m : Nat) : Nat :=
  match m with
  | zero => n
  | succ m' => succ (add n m')

add_zero : ∀ n : Nat, n + zero = nadd_succ : ∀ n m : Nat, n + (succ m) = succ (n + m)

Quiz

What about this one? Recall that our add function has notation + and is marked @[irreducible].

theorem review₄ (n : Nat) : n + zero = n

(A) none

(B) rewrite

(D) both rewrite and cases

(E) can't be done with the tactics we've seen.

Show solution

theorem review₄ (n : Nat) : n + zero = n := byn:Nat⊢ n + zero = n
  rewrite [add_zeron:Nat⊢ n = n]n:Nat⊢ n = n
  rflAll goals completed! 🐙

Quiz

What about this?

theorem review₅ (n : Nat) : zero + n = n

(A) none

(B) rewrite

(D) both rewrite and cases

(E) can't be done with the tactics we've seen.

Show solution

This one cannot be proved by rfl, cases, or rewriting alone — it needs induction! (We'll see why below.)

Exercise★(succ_eq_add_one)

One more warm-up exercise. Prove the following theorem, using theorems from Basics:

theorem declaration uses `sorry`succ_eq_add_one (n : Nat) : succ n = n + one := byn:Nat⊢ succ n = n + one
  sorryAll goals completed! 🐙

3.3. Proof by Induction🔗

We will introduce proofs by induction on natural numbers, first motivating why induction is needed, and then explaining what it is and how you do it in Lean.

3.3.1. Motivation🔗

For the add_zero simplification rule, we were able to prove that zero is a neutral element for + on the right using just rfl.

But the proof that it is also a neutral element on the left gets stuck...

example (n : Nat) : zero + n = n := byn:Nat⊢ zero + n = n
  Tactic `rfl` failed: The left-hand side
  zero + n
is not definitionally equal to the right-hand side
  n

n:Nat⊢ zero + n = nrfln:Nat⊢ zero + n = n    -- doesn't work here!

Tactic `rfl` failed: The left-hand side
  zero + n
is not definitionally equal to the right-hand side
  n

n:Nat⊢ zero + n = n

And reasoning by cases using cases on n doesn't get us much further: the branch of the case analysis where we assume n = zero goes through just fine, but in the branch where n = n' + 1 for some n' we get stuck in exactly the same way.

example (n : Nat) : zero + n = n := unsolved goals
succn':Nat⊢ zero + succ n' = succ n'byn:Nat⊢ zero + n = n
  cases n with
  | zero =>zero⊢ zero + zero = zero /- n = zero -/
    rewrite [add_zerozero⊢ zero = zero]zero⊢ zero = zero
    rflAll goals completed! 🐙
    -- so far so good...
  | succ n' =>   /- n = succ n' -/
    _     -- ...but we're stuck on zero + n'

unsolved goals
succn':Nat⊢ zero + succ n' = succ n'

3.3.2. Induction: In Principle and in Lean🔗

We need a bigger hammer: the principle of induction over natural numbers:

If P(n) is some proposition involving a natural number n, and we want to show that P holds for all numbers, we can reason like this:

show that P(zero) holds
show that, if P(n') holds, then so does P(succ n')
conclude that P(n) holds for all n.

For example...

theorem zero_add (n : Nat) : zero + n = n := byn:Nat⊢ zero + n = n
  induction n with
  | zero =>zero⊢ zero + zero = zero /- n = zero -/
    rewrite [add_zerozero⊢ zero = zero]zero⊢ zero = zero
    rflAll goals completed! 🐙
  | succ n' ih =>succn':Natih:zero + n' = n'⊢ zero + succ n' = succ n' /- n = succ n' -/
    /-
      Goal: zero + (succ n') = succ n'
      We can rewrite `zero + (succ n')` to `succ (zero + n')`.
      Then we can rewrite with the induction hypothesis.
    -/
    rewrite [add_succ,succn':Natih:zero + n' = n'⊢ succ (zero + n') = succ n' ihsuccn':Natih:zero + n' = n'⊢ succ n' = succ n']succn':Natih:zero + n' = n'⊢ succ n' = succ n'
    rflAll goals completed! 🐙

Let's try this one together:

theorem declaration uses `sorry`beq_self (n : Nat) : (n == n) = true := byn:Nat⊢ (n == n) = true
  sorryAll goals completed! 🐙

Exercise★★(basic_induction)

Here's another related fact about addition, which we'll need later. (The proof is left as an exercise.)

theorem declaration uses `sorry`add_comm (n m : Nat) :
    n + m = m + n := byn:Natm:Nat⊢ n + m = m + n
  sorryAll goals completed! 🐙

3.3.3. Tip: The `rw` Tactic🔗

As you've probably noticed, a common pattern in Lean proofs is rewrite [...] followed by rfl. Lean also provides a tactic that combines these two steps: rw [...] will automatically close the goal if the rewrite makes the goal true by definition. For example, instead of

rewrite [double_zero]; rfl

we could write this:

rw [double_zero]

If rw leaves a goal that looks definitionally true, try adding rfl after it.

set_option pp.fieldNotation false

3.4. Proofs Within Proofs🔗

New tactic: have.

theorem mul_zero_add' (n m : Nat) :
    ((zero + n) + zero) * m = n * m := byn:Natm:Nat⊢ (zero + n + zero) * m = n * m
  have h : (zero + n) + zero = n := by
    rw [zero_add,n:Natm:Nat⊢ n + zero = n add_zeron:Natm:Nat⊢ n = n]n:Natm:Nath:zero + n + zero = n⊢ (zero + n + zero) * m = n * m
  rw [hn:Natm:Nath:zero + n + zero = n⊢ n * m = n * m]All goals completed! 🐙

example (n m p q : Nat) :
   (n + m) + (p + q) = (m + n) + (p + q) := unsolved goals
n m p q:Nat⊢ p + q + (n + m) = m + n + (p + q)byn:Natm:Natp:Natq:Nat⊢ n + m + (p + q) = m + n + (p + q)
  /-
    We just need to swap (n + m) for (m + n)... seems
    like add_comm should do the trick!
    But `rw [add_comm]` might rewrite the wrong `+`!
  -/
  rw [add_commn:Natm:Natp:Natq:Nat⊢ p + q + (n + m) = m + n + (p + q)]n:Natm:Natp:Natq:Nat⊢ p + q + (n + m) = m + n + (p + q)

unsolved goals
n m p q:Nat⊢ p + q + (n + m) = m + n + (p + q)

To use add_comm at the point where we need it, we can supply explicit arguments: rw [add_comm n m] tells Lean exactly which + to rewrite. (We can also use have to establish the specific equation we want, then rewrite with it.)

theorem add_rearrange (n m p q : Nat) :
    (n + m) + (p + q) = (m + n) + (p + q) := byn:Natm:Natp:Natq:Nat⊢ n + m + (p + q) = m + n + (p + q)
  rw [add_comm n mn:Natm:Natp:Natq:Nat⊢ m + n + (p + q) = m + n + (p + q)]All goals completed! 🐙

3.5. Formal vs. Informal Proof🔗

"Informal proofs are algorithms; formal proofs are code."

3.6. Aside: Using Code Actions to Generate Match Skeletons🔗

Lean's language server can suggest code actions, which are small editor commands that modify the source code.

In VS Code, a lightbulb icon appears on the left when a code action is available at your cursor.

Let's look at a code action for induction. Suppose we start with the following incomplete proof:

example (n : Nat) : Nat.beq n n = true := unsolved goals
zero⊢ (zero == zero) = true

succn✝:Natn_ih✝:(n✝ == n✝) = true⊢ (succ n✝ == succ n✝) = truebyn:Nat⊢ (n == n) = true
  induction nzero⊢ (zero == zero) = truesuccn✝:Natn_ih✝:(n✝ == n✝) = true⊢ (succ n✝ == succ n✝) = true

Put your cursor on induction n and open the code action menu.

Click the lightbulb.

This gives us the basic structure of the proof without requiring us to write each branch by hand. We can then focus on proving each case.

Let's do the proof!

declaration uses `sorry`example (n : Nat) : Nat.beq n n = true := byn:Nat⊢ (n == n) = true
  sorryAll goals completed! 🐙

The same trick also works for match expressions. For example, suppose we start with

def isZero (n : Nat) : Bool :=
  match n
unexpected end of input; expected 'with'

Lean can generate the missing branches:

def isZero (n : Nat) : Bool :=
  match n with
  | .zero => don't know how to synthesize placeholder
context:
n:Nat⊢ Bool_
  | .succ n => don't know how to synthesize placeholder
context:
n✝ n:Nat⊢ Bool_

One note: Sometimes the variables the code action chooses are not ideal, so you might want to change them.

3.7. More Exercises🔗

Exercise★(mul_one)

theorem declaration uses `sorry`mul_one (p : Nat) :
    one * p = p := byp:Nat⊢ one * p = p
  sorryAll goals completed! 🐙

By default, rewrite and rw rewrite left to right, i.e., they transform the goal (or a hypothesis) from the form on the left side of the equality to the right side. To rewrite from right to left, use rewrite [← h] or rw [← h], where ← is entered as \l or \<-.

These exercises state facts that will be used later. We don't need to work them in class.

Exercise★★★(mul_comm)

Use have (or rw with explicit arguments) to help prove add_shuffle3. You don't need to use induction.

theorem declaration uses `sorry`add_shuffle3 (n m p : Nat) : n + m + p = n + p + m := byn:Natm:Natp:Nat⊢ n + m + p = n + p + m
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`succ_mul (m n : Nat) :
    (succ n) * m = (n * m) + m := bym:Natn:Nat⊢ succ n * m = n * m + m
  sorryAll goals completed! 🐙

Now prove commutativity of multiplication.

theorem declaration uses `sorry`mul_comm (m n : Nat) :
    m * n = n * m := bym:Natn:Nat⊢ m * n = n * m
  sorryAll goals completed! 🐙

Exercise★★★(more_exercises) (Optional)

Take a piece of paper. For each of the following theorems, first think about whether (a) it can be proved using only simplification and rewriting, (b) it also requires case analysis (cases), or (c) it also requires induction. Write down your prediction. Then fill in the proof. (There is no need to turn in your piece of paper; this is just to encourage you to reflect before you hack!)

theorem declaration uses `sorry`ble_refl (n : Nat) :
    Nat.ble n n = true := byn:Nat⊢ ble n n = true
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`andb_false (b : Bool) :
    (b && false) = false := byb:Bool⊢ (b && false) = false
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`all3_spec (b c : Bool) :
    ((b && c) || ((!b) || (!c))) = true := byb:Boolc:Bool⊢ (b && c || (!b || !c)) = true
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`right_distrib (n m p : Nat) :
    (n + m) * p = (n * p) + (m * p) := byn:Natm:Natp:Nat⊢ (n + m) * p = n * p + m * p
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`left_distrib (n m p : Nat) :
    p * (n + m) = (p * n) + (p * m) := byn:Natm:Natp:Nat⊢ p * (n + m) = p * n + p * m
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`mul_assoc (n m p : Nat) :
    n * (m * p) = (n * m) * p := byn:Natm:Natp:Nat⊢ n * (m * p) = n * m * p
  sorryAll goals completed! 🐙

3.8. A New Tactic Combinator: `<;>`🔗

New tactic combinator: t₁ <;> t₂ runs t₁, then runs t₂ on every subgoal produced by t₁.

example (b : Bool) : (b || true) = true := byb:Bool⊢ (b || true) = true
  cases bfalse⊢ (false || true) = truetrue⊢ (true || true) = true <;>false⊢ (false || true) = truetrue⊢ (true || true) = true rflAll goals completed! 🐙

This is short for:

example (b : Bool) : (b || true) = true := byb:Bool⊢ (b || true) = true
  cases b with
  | false =>false⊢ (false || true) = true rflAll goals completed! 🐙
  | true  =>true⊢ (true || true) = true rflAll goals completed! 🐙

We can also chain <;>s.

example (b c : Bool) : (b && c) = (c && b) := byb:Boolc:Bool⊢ (b && c) = (c && b)
  cases bfalsec:Bool⊢ (false && c) = (c && false)truec:Bool⊢ (true && c) = (c && true) <;>falsec:Bool⊢ (false && c) = (c && false)truec:Bool⊢ (true && c) = (c && true) cases ctrue.false⊢ (true && false) = (false && true)true.true⊢ (true && true) = (true && true) <;>false.false⊢ (false && false) = (false && false)false.true⊢ (false && true) = (true && false)true.false⊢ (true && false) = (false && true)true.true⊢ (true && true) = (true && true) rflAll goals completed! 🐙

3.9. Nat to Bin and Back🔗

3.10. Bin to Nat and Back (Advanced)🔗

Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

3. Induction: Proof by Induction🔗

3.1. Separate Compilation🔗

3.2. Review🔗

3.3. Proof by Induction🔗

3.3.1. Motivation🔗

3.3.2. Induction: In Principle and in Lean🔗

3.3.3. Tip: The rw Tactic🔗

3.4. Proofs Within Proofs🔗

3.5. Formal vs. Informal Proof🔗

3.6. Aside: Using Code Actions to Generate Match Skeletons🔗

3.7. More Exercises🔗

3.8. A New Tactic Combinator: <;>🔗

3.9. Nat to Bin and Back🔗

3.10. Bin to Nat and Back (Advanced)🔗

3.3.3. Tip: The `rw` Tactic🔗

3.8. A New Tactic Combinator: `<;>`🔗