In Lean 4, the natural numbers are defined as an inductive type with exactly two constructors:
inductive Nat where | zero : Nat | succ (n : Nat) : Nat
Every natural number is either Nat.zero (which we write as 0) or Nat.succ n for some natural number n (which is n + 1). There is nothing else. The number 3, for instance, is Nat.succ (Nat.succ (Nat.succ Nat.zero)).
Addition on natural numbers is defined recursively. In Lean 4's core library, Nat.add is defined by pattern matching on the second argument:
def Nat.add : Nat → Nat → Nat | n, Nat.zero => n | n, Nat.succ m => Nat.succ (Nat.add n m)
This means n + 0 reduces to n by definition. But 0 + n does not reduce directly — it requires a proof. This is a subtle but important point: definitional equality depends on which argument the recursion is over.
Let's first verify that Lean understands concrete numbers. The rfl tactic proves any goal of the form a = a — it checks that both sides are definitionally equal.
example : Nat.succ (Nat.succ Nat.zero) = 2 := by rfl
Both sides reduce to the same thing, so rfl closes the goal immediately.
Now prove that adding zero on the left does nothing. This is the theorem Nat.zero_add from Lean's core library. Since addition recurses on the second argument, 0 + n does not simplify by definition — you need a tactic.
theorem zero_add (n : Nat) : 0 + n = n := by sorry
The simp tactic can close this goal. It applies a collection of simplification lemmas, including Nat.zero_add from the library.
You can also prove this by induction on n. The base case 0 + 0 = 0 holds by rfl, and the inductive step follows from the definition of addition plus the induction hypothesis.
The simplest proof:
theorem zero_add (n : Nat) : 0 + n = n := by simp
Or, citing the library lemma directly:
theorem zero_add (n : Nat) : 0 + n = n := by exact Nat.zero_add n
Or, by induction — the proof Lean's library essentially uses:
theorem zero_add (n : Nat) : 0 + n = n := by induction n with | zero => rfl | succ n ih => simp [Nat.add_succ, ih]
rfl proves goals where both sides are definitionally equal — no lemmas needed, just computation.
simp applies a library of simplification lemmas to rewrite the goal. It is powerful but sometimes opaque — you don't always see what it did.
Definitional equality is asymmetric in practice. Because Nat.add recurses on its second argument, n + 0 = n is true by rfl, but 0 + n = n requires a proof.