Mathematical Induction in Lean

So far, we have dealt with propositions regarding the MyNat type that can be proven directly from definitions using rfl. In this post, we will explore how to use mathematical induction in Lean 4 for propositions that cannot be proven by rfl alone. We will continue using "Introduction to Lean from Scratch: Hands-on Development of Formal Mathematics Libraries" as our learning material.

When rfl Works, and When It Fails

First, the following proposition can be proven without any issues:

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

However, the next proposition, which seemingly just swaps the left and right sides, cannot be proven using rfl in the same way.

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

Even though the expressions look almost identical, why does one pass while the other fails? To understand this, let's look at the definition of MyNat.add.

Why rfl Fails

MyNat.add is defined as follows:

def MyNat.add (m n : MyNat) : MyNat :=
  match n with
  | .zero => m
  | .succ n => succ (add m n)

The key point here is that the pattern matching with match is done on the second argument n, not the first argument m.

In the case of n + 0, the second argument of add is .zero, so the match immediately returns m (which is n itself). Since this is structurally determined prior to any evaluation, rfl can fully reduce it.

On the other hand, in the case of 0 + n, the second argument of add is the variable n. Lean cannot determine whether n is .zero or .succ ... without knowing its concrete value, so it cannot expand the match any further. In other words, the goal cannot be fully reduced to n through simple definitional reduction via rfl.

If we actually reduce both expressions using the #reduce command, this difference becomes glaringly obvious.

#reduce fun (n : MyNat) => n + 0
-- fun n => n

#reduce fun (n : MyNat) => 0 + n
-- fun n => (MyNat.rec ⟨MyNat.zero, PUnit.unit⟩
--   (fun n n_ih => ⟨MyNat.succ n_ih.1, n_ih⟩) n).1

While n + 0 reduces to the simple form n, 0 + n remains a complex expression that uses MyNat.rec (the recursor). This indicates that because the variable n itself is undetermined, the recursive structure cannot be broken down any further.

Mathematical Induction with the induction Tactic

Since rfl alone cannot handle the case where n is .succ, this is where mathematical induction comes into play. In Lean 4, applying the induction tactic allows us to use induction on types defined with the inductive keyword.

Since MyNat is an inductive type with two constructors—zero and succ—using the induction tactic splits the goal into the following two cases:

• The zero case: Show that 0 + MyNat.zero = MyNat.zero
• The succ n' case: Show that 0 + n'.succ = n'.succ using the inductive hypothesis (ih), which is "0 + n' = n'"

The zero case can be proven with rfl as before, because 0 + 0 directly reduces to 0 by definition.

The real issue lies in the succ n' case. Here, we need to transform the expression 0 + n'.succ into the form (0 + n').succ, and then apply the inductive hypothesis ih : 0 + n' = n'. To perform this "transformation," we use the following lemma, which can be proven directly from the definition of MyNat.add.

theorem MyNat.add_succ (m n : MyNat) : m + .succ n = .succ (m + n) := by
  rfl

Since add_succ itself is the definition of MyNat.add itself, it can be proven with rfl. By using this with the rw (rewrite) tactic, we can rewrite the succ case into a form where ih can be applied.

The Flow of the Entire Proof

Based on the above steps, the proof for 0 + n = n looks like this:

example (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n' ih =>
    -- ih : 0 + n' = n' ⊢ 0 + n'.succ = n'.succ
    rw [MyNat.add_succ] -- (0 + n').succ = n'.succ
    rw [ih] -- n'.succ = n'.succ

Let's examine each step one by one.

The zero case: The goal is 0 + MyNat.zero = MyNat.zero. By the definition of MyNat.add, this holds definitionally, so it can be proven by rfl.

The succ case: We are given ih : 0 + n' = n' as the inductive hypothesis, and the goal becomes 0 + n'.succ = n'.succ.

First, rw [MyNat.add_succ] rewrites the left-hand side of the goal, 0 + n'.succ, into (0 + n').succ. This changes the goal to (0 + n').succ = n'.succ.

Next, rw [ih] uses ih (0 + n' = n') to substitute 0 + n' in the goal with n'. This turns the goal into the trivial identity n'.succ = n'.succ, and the rw tactic automatically closes it using rfl.

Summary

In this post, sparked by the seemingly strange phenomenon where n + 0 = n can be proven by rfl but 0 + n = n cannot, we learned about the definition of MyNat.add (pattern matching on the second argument) and how to use mathematical induction with the induction tactic.

Understanding that the scope of rfl depends on the structural design of definitions, and learning how to rewrite expressions using lemmas like add_succ to leverage inductive hypotheses, will serve as a foundational workflow when proving more complex theorems in the future.