Addition is associative

Associativity says that when you add three numbers, it doesn't matter where you place the parentheses:

(a + b) + c = a + (b + c)

This feels obvious, but it has to be proved from the definition of addition. Since Nat.add is defined by recursion on its second argument, the natural strategy is to induct on c.

In the base case (c = 0), both sides reduce to the same thing by the definition of addition: (a + b) + 0 = a + b and a + (b + 0) = a + b.

In the inductive step (c = succ c), we unfold the definition of addition on successors and use the induction hypothesis.

The `omega` tactic

Lean 4 includes the omega tactic, which automatically decides linear arithmetic over natural numbers and integers. It can prove any true statement involving addition, subtraction, multiplication by constants, and comparisons. For a theorem like associativity, omega closes the goal instantly.

But using omega on everything is like using a calculator in a maths class — you get the answer but miss the lesson. In this exercise, try the manual proof first.

Exercise

theorem my_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  sorry

Hint 1

Induct on c. Remember that addition is defined by recursion on the second argument, so inducting on c lets you unfold the definition.

Hint 2

In the successor case, the key fact is Nat.add_succ, which says n + Nat.succ m = Nat.succ (n + m). Apply it to both sides, then use the induction hypothesis.

Solution (one-liner)

theorem my_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  omega

Solution (by induction)

theorem my_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  induction c with
  | zero => rfl
  | succ c ih =>
    simp [Nat.add_succ]
    exact ih

In the base case, both sides reduce to the same expression because n + 0 = n by definition. In the successor case, Nat.add_succ rewrites x + succ c to succ (x + c) on both sides, and then the induction hypothesis ih finishes the job.

Key takeaways

omega is a decision procedure for linear arithmetic. It will prove any true linear equation or inequality over Nat or Int. Use it when you want to move fast.

Induction on the recursion variable is the fundamental technique. When a function is defined by recursion on an argument, proving properties of that function usually requires induction on the same argument.

← Zero and successor Next: Addition is commutative →