Multiplication distributes over addition

The distributive law connects addition and multiplication:

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

This is the property that makes arithmetic work as a coherent system. Without it, multiplication would just be a separate operation with no relationship to addition. With it, you get algebra.

In Lean 4, multiplication on natural numbers is defined by recursion on the second argument, just like addition:

def Nat.mul : Nat → Nat → Nat
  | _, Nat.zero   => Nat.zero
  | n, Nat.succ m => Nat.mul n m + n

So a * 0 = 0 by definition, and a * succ m = a * m + a. Proving distributivity requires combining everything we have learned: induction, associativity, commutativity, and careful rewriting.

Exercise

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

Hint 1

Induct on c, since both addition and multiplication recurse on the second argument. In the base case, a * (b + 0) = a * b + a * 0 simplifies by the definitions of addition and multiplication.

Hint 2

In the successor case, you need to show a * (b + succ c) = a * b + a * succ c. Start by rewriting b + succ c using Nat.add_succ, then unfold a * succ (...) using Nat.mul_succ. You will need associativity of addition to rearrange the terms, and the induction hypothesis to handle the recursive part.

Hint 3

The key lemma is Nat.mul_succ (a n : Nat) : a * succ n = a * n + a. Combined with Nat.add_succ and Nat.add_assoc, this gets you through the inductive step.

Solution (one-liner)

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

The omega tactic handles this because it is a linear arithmetic identity. But this teaches you nothing about how the proof actually works.

Solution (by induction)

theorem my_mul_add (a b c : Nat) : a * (b + c) = a * b + a * c := by
  induction c with
  | zero => simp
  | succ c ih =>
    simp [Nat.add_succ, Nat.mul_succ]
    rw [ih]
    omega

Or fully expanded, without omega in the inductive step:

theorem my_mul_add (a b c : Nat) : a * (b + c) = a * b + a * c := by
  induction c with
  | zero =>
    -- a * (b + 0) = a * b + a * 0
    simp [Nat.mul_zero, Nat.add_zero]
  | succ c ih =>
    -- Goal: a * (b + succ c) = a * b + a * succ c
    rw [Nat.add_succ]       -- a * succ (b + c) = ...
    rw [Nat.mul_succ]       -- a * (b + c) + a = ...
    rw [Nat.mul_succ]       -- ... = a * b + (a * c + a)
    rw [ih]                 -- a * b + a * c + a = a * b + (a * c + a)
    rw [Nat.add_assoc]      -- done

Each rw step transforms the goal using a single lemma. Reading this proof top to bottom, you can see exactly how the two sides are brought into alignment.

What you have proved

With distributivity, you now have the core of semiring arithmetic for natural numbers. Across this track you have established:

0 + n = n (additive identity, left)
(a + b) + c = a + (b + c) (associativity of addition)
a + b = b + a (commutativity of addition)
0 < 2 ^ n (positivity via induction)
a * (b + c) = a * b + a * c (left distributivity)

These are not just exercises — they are the actual foundations of arithmetic, proved from nothing but the definition of natural numbers and the principle of induction.

Key takeaways

Distributivity combines everything. This proof uses induction, definitional unfolding, associativity, and careful rewriting. It is a mini-capstone for natural number arithmetic.

rw gives you fine control. Unlike simp, which applies many lemmas at once, rw applies exactly one lemma at a time. This makes proofs longer but more transparent.

The ring tactic can also prove identities like this for any commutative semiring. Once you know the theory, automation becomes a tool rather than a crutch.

← Induction Back to all tracks →