Commutative and Associative Laws of Multiplication in Lean

In this post, we will define multiplication on MyNat and prove the distributive, commutative, and associative laws. We will continue using "Introduction to Lean from Scratch: Hands-on Formal Mathematics Library Development" as our learning material.

Definition of Multiplication

First, let's define multiplication. We can define m × n as repeating the addition of m for n times. In other words, it can be defined as m * 0 = 0 and m * (n + 1) = m * n + m.

def MyNat.mul (m n : MyNat) : MyNat :=
  match n with
  | 0 => 0
  | n + 1 => MyNat.mul m n + m

By using the instance keyword, we make it possible to handle standard integer multiplication as MyNat.

instance : Mul MyNat where
  mul := MyNat.mul

Proving Basic Theorems

From here, we will prove some basic theorems in order to eventually prove the commutative law of multiplication, m * n = n * m.

First, let's prove m * (n + 1) = m * n + m. Since this is equivalent to the definition itself, it can be proven using the reflexivity tactic, rfl.

theorem MyNat.mul_add_one (m n : MyNat) : m * (n + 1) = m * n + m := by
  rfl

For the case of (m + 1) * n = m * n + n, a recursive proof is required. It can be proven as follows using mul_add_one along with the commutative and associative laws of addition.

theorem MyNat.add_one_mul (m n : MyNat) : (m + 1) * n = m * n + n := by
  induction n with
  | zero =>
    rfl
  | succ n ih => calc --ih : (m + 1) * n = m * n + n ⊢ (m + 1) * (n + 1) = m * (n + 1) + (n + 1)
    _ = (m + 1) * (n + 1) := by rfl
    _ = (m + 1) * n + (m + 1) := by rw [MyNat.mul_add_one]
    _ = m * n + n + (m + 1) := by rw [ih]
    _ = m * n + m + (n + 1) := by ac_rfl
    _ = m * (n + 1) + (n + 1) := by rw [MyNat.mul_add_one]

Multiplication by 0 or 1 can also be proven using the theorems above.

@[simp] theorem MyNat.mul_zero (m : MyNat) : m * 0 = 0 := by
  rfl

@[simp] theorem MyNat.zero_mul (n : MyNat) : 0 * n = 0 := by
  induction n
  case zero => rfl
  case succ n ih => --  0 * n = 0 ⊢ 0 * (n + 1) = 0
    simp [MyNat.mul_add_one, ih]

@[simp] theorem MyNat.mul_one (n : MyNat) : n * 1 = n := calc
  _ = n * (0 + 1) := by simp
  _ = n * 0 + n := by rw [MyNat.mul_add_one]
  _ = n := by simp

@[simp] theorem MyNat.one_mul (n : MyNat) : 1 * n = n := calc
  _ = (0 + 1) * n := by simp
  _ = 0 * n + n := by rw [MyNat.add_one_mul]
  _ = n := by simp

Commutative, Distributive, and Associative Laws

Now we arrive at the main goals: the commutative, distributive, and associative laws of multiplication.

First is the commutative law, m * n = n * m. This can be proven through a recursive proof by utilizing the theorems we have established so far.

theorem MyNat.mul_comm (m n : MyNat) : m * n = n * m := by
  induction n with
  | zero => simp
  | succ n ih => calc
  -- ih : m * n = n * m
  -- ⊢ m * (n + 1) = (n + 1) * m
    _ = m * (n + 1) := by rfl
    _ = m * n + m := by rw [MyNat.mul_add_one]
    _ = n * m + m := by rw [ih]
    _ = (n + 1) * m := by rw [MyNat.add_one_mul]

Next is the distributive law. This is also a recursive proof using our previous theorems.

theorem MyNat.add_mul (l m n : MyNat) : (l + m) * n = l * n + m * n := by
  induction n with
  | zero => rfl
  | succ n ih => calc
  -- ih : (l + m) * n = l * n + m * n
  -- ⊢ (l + m) * (n + 1) = l * (n + 1) + m * (n + 1)
  _ = (l + m) * (n + 1) := by rfl
  _ = (l + m) * n + (l + m) := by rw [MyNat.mul_add_one]
  _ = l * n + m * n + (l + m) := by rw [ih]
  _ = (l * n + l) + (m * n + m) := by ac_rfl
  _ = l * (n + 1) + m * (n + 1) := by simp [MyNat.mul_add_one]

The left distributive law can be proven by fully utilizing the commutative law.

theorem MyNat.mul_add (l m n : MyNat) : l * (m + n) = l * m + l * n := calc
  _ = (m + n) * l := by rw [MyNat.mul_comm]
  _ = m * l + n * l := by rw [MyNat.add_mul]
  _ = l * m + l * n := by simp [MyNat.mul_comm]

The associative law can be proven using the distributive law.

theorem MyNat.mul_assoc (l m n : MyNat) : l * m * n = l * (m * n) := by
  induction n with
  | zero => rfl
  | succ n ih =>
  -- ih : l * m * n = l * (m * n)
  -- ⊢ l * m * (n + 1) = l * (l * (n + 1))
    simp [MyNat.mul_add, ih]