Induction

Mathematical induction is the most important proof technique for natural numbers. The idea is simple but profound: to prove a property P(n) holds for every natural number, you prove two things:

Base case: P(0) is true.

Inductive step: For any n, if P(n) is true then P(n + 1) is true.

Why does this work? Because every natural number is reached from zero by applying successor finitely many times. The base case covers zero; the inductive step covers every successor. Together, they cover everything.

In Lean 4, induction on a natural number n looks like this:

induction n with
| zero =>
  -- prove the base case here
| succ n ih =>
  -- ih : P(n)   (the induction hypothesis)
  -- prove P(n + 1) here

The ih in the successor branch is the induction hypothesis — the assumption that the property holds for n. You get to use it for free when proving the property for n + 1.

Exercise

Prove that 2 ^ n is always positive. This is a clean example of induction where the base case is a concrete computation and the inductive step requires a small arithmetic argument.

theorem pow_two_pos (n : Nat) : 0 < 2 ^ n := by
  sorry

Hint 1

Start with induction n. In the base case, 2 ^ 0 = 1 by definition, and 0 < 1 is true.

Hint 2

In the successor case, 2 ^ (n + 1) = 2 * 2 ^ n. Since 2 ^ n > 0 by the induction hypothesis, 2 * 2 ^ n > 0 as well. The omega tactic or simp with appropriate lemmas can handle the arithmetic.

Solution

theorem pow_two_pos (n : Nat) : 0 < 2 ^ n := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp [Nat.pow_succ, Nat.mul_comm]
    omega

Alternatively, a shorter proof using positivity-style reasoning:

theorem pow_two_pos (n : Nat) : 0 < 2 ^ n := by
  exact Nat.pos_pow_of_pos n (by omega)

Or simply:

theorem pow_two_pos (n : Nat) : 0 < 2 ^ n := by
  induction n with
  | zero => decide
  | succ n ih =>
    calc 0 < 2 ^ n := ih
    _ < 2 ^ n + 2 ^ n := Nat.lt_add_of_pos_right ih
    _ = 2 ^ (n + 1) := by ring

The calc block lets you chain inequalities step by step, making the proof readable.

The shape of an induction proof

Every induction proof follows the same pattern:

Identify which variable to induct on.
Prove the base case (usually the easy part).
In the inductive step, figure out how to use ih to bridge the gap from n to n + 1.

The hard part is almost always step 3. The induction hypothesis gives you something about n, and you need to connect it to a statement about n + 1. This often requires unfolding definitions or applying lemmas to transform the goal into a form where ih applies.

Key takeaways

Induction is pattern matching on proofs. Just as you pattern match on Nat to define functions, you pattern match on Nat to prove properties. The induction tactic in Lean makes this explicit.

decide can prove any decidable proposition about concrete values. For the base case 0 < 2 ^ 0, it just computes and checks.

calc blocks let you write proofs as chains of equalities or inequalities, making complex arguments readable.

← Addition is commutative Next: Multiplication distributes over addition →