Strategy: Proof by induction

Pattern recognition

When you see: a goal about all natural numbers (or any inductive type)

Strategy: Prove the base case, then prove the inductive step using the induction hypothesis.

Tactic: induction n with

Induction is the workhorse of natural number proofs. The idea: prove P(0), then prove that P(n) implies P(n+1). Together, these cover every natural number.

The key insight is which variable to induct on. Usually, you induct on the same variable that the relevant function recurses on. If addition recurses on the second argument, induct on the second argument.

Watch the strategy in action

The rule

Goal shape:  ∀ n : Nat, P(n)    (or a goal containing n : Nat)
Action:      induction n with
Effect:      Two subgoals:
             | zero =>       prove P(0)
             | succ n ih =>  ih : P(n), prove P(n+1)
Think:       "Base case + inductive step = all natural numbers."

Your turn

Prove that the sum 0 + 1 + 2 + ... + n = n * (n + 1) / 2. In Lean, we avoid division and prove the doubled version: 2 * sum n = n * (n + 1).

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

theorem gauss_sum (n : Nat) : 2 * sum_to n = n * (n + 1) := by
  sorry

Hint

Induct on n. The base case is 2 * 0 = 0 * 1, which is rfl. For the inductive step, unfold sum_to and use ring or omega to handle the arithmetic after applying ih.

Solution

theorem gauss_sum (n : Nat) : 2 * sum_to n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp [sum_to]
    omega

See also: Numbers §04 — Induction

← Contradiction Existential witness →