← More tactics

Index

Next: Exercises →

---

The goal is to show, for all a b : Nat, that a + b = b + a. Recall from Chapter 1 that Nat is built from zero and succ (successor), and that + is defined by recursion on its second argument:

\[a + 0 = a, \qquad a + \mathrm{succ}(k) = \mathrm{succ}(a + k)\]

The proof proceeds by induction on b, one step at a time.

Base case (b = 0). The goal becomes a + 0 = 0 + a.

• The left side, a + 0, reduces to a directly from the definition of + above (this fact is recorded in core Lean as the lemma Nat.add_zero).
• The right side, 0 + a, is not immediate from the definition, since the recursion is on the second argument, not the first. It therefore needs its own small lemma, Nat.zero_add : 0 + a = a, proved separately by induction on a.
• Combining both: a + 0 = a and 0 + a = a, hence a + 0 = 0 + a.

theorem my_add_comm (a b : Nat) : a + b = b + a := by
  induction b with
  | zero =>
    -- Goal: a + 0 = 0 + a
    rw [Nat.add_zero]   -- rewrites `a + 0` to `a`. Goal: a = 0 + a
    rw [Nat.zero_add]    -- rewrites `0 + a` to `a`. Goal: a = a, closed by rw automatically
  | succ k ih =>
    -- ih : a + k = k + a
    -- Goal: a + Nat.succ k = Nat.succ k + a
    rw [Nat.add_succ]     -- a + succ k  ~>  succ (a + k). Goal: succ (a + k) = succ k + a
    rw [ih]                -- use the induction hypothesis: a + k ~> k + a. Goal: succ (k + a) = succ k + a
    rw [Nat.succ_add]      -- succ k + a  ~>  succ (k + a). Goal: succ (k + a) = succ (k + a), closed

Walking through the inductive step slowly:

1. The statement is to be proved for b = Nat.succ k, assuming it already holds for k (that assumption is ih : a + k = k + a).
2. rw [Nat.add_succ] uses the defining equation a + succ k = succ (a + k) to rewrite the left-hand side of the goal.
3. rw [ih] uses the induction hypothesis to replace a + k with k + a inside the goal.
4. rw [Nat.succ_add] uses the equation succ k + a = succ (k + a) to rewrite the right-hand side, so both sides now read succ (k + a), which are literally identical. rw closes the goal automatically once the two sides match syntactically.

This is the pattern — base case, inductive step, explicit ih — that recurs, slowly and explicitly, for every proof about groups and rings.

Mathematical reading. This is the elementary proof that $(\mathbb{N}, +)$ is commutative, carried out by induction on the second argument from the recursive definition $a + 0 = a$, $a + \mathrm{succ}(k) = \mathrm{succ}(a + k)$. Writing $P(b) :\equiv (\forall a,\ a + b = b + a)$: the base case is $P(0)$, which needs the auxiliary fact $0 + a = a$ (proved separately since the recursion favors the right argument). The inductive step derives $P(k+1)$ from $P(k)$ via \(a + (k{+}1) = (a+k){+}1 \overset{\mathrm{ih}}{=} (k+a){+}1 = (k{+}1)+a.\) Each rw is one equational step in this chain. The whole proof is the standard textbook lemma, with the successor/zero cases spelled out in full, where written mathematics usually skips over them.

Programmer’s corner (Python). The two cases of induction b with | zero => ... | succ k ih => ... have exactly the shape of a recursive function over the same inductively-defined structure. Compare it to a hand-rolled Peano type in Python:

class Zero: pass
class Succ:
    def __init__(self, pred): self.pred = pred

def add(a, b):
    if isinstance(b, Zero):
        return a                          # base case, like `| zero =>`
    return Succ(add(a, b.pred))            # recursive call, like `| succ k ih =>`

add’s if isinstance(b, Zero) branch is the base case. Its recursive call add(a, b.pred) plays exactly the role ih plays in the succ branch: “assume it already works for the smaller case, build the answer for one Succ more.” The proof is not merely analogous to recursion, it is a recursion, one producing a proof term instead of a Succ value. This is why Lean can generate induction’s two cases automatically straight from Nat’s definition, the same way Python’s isinstance cases fall straight out of Nat’s two constructors.

---

← More tactics

Index

Next: Exercises →