import MyNat.Addition
import MyNat.Multiplication
import MultiplicationWorld.Level1 -- zero_mul
import MultiplicationWorld.Level4 -- mul_add
namespace MyNat
open MyNat

Multiplication World

Level 5: mul_assoc

We now have enough to prove that multiplication is associative.

Random tactic hints

Did you know you can repeat a tactic as many times as necessary to complete the goal?

Lemma

Multiplication is associative. In other words, for all natural numbers a, b and c, we have (ab)c = a(bc).

lemma 
mul_assoc: ∀ (a b c : MyNat), a * b * c = a * (b * c)
mul_assoc (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : (
a: MyNat
a * 
b: MyNat
b) * 
c: MyNat
c = 
a: MyNat
a * (
b: MyNat
b * 
c: MyNat
c) := by
a, b, c: MyNat
a * b * c = a * (b * c)
  induction 
c: MyNat
c with
a, b, c: MyNat
a * b * c = a * (b * c)
  | 
zero: MyNat
zero =>
a, b: MyNat
zero
a * b * zero = a * (b * zero)
    rw [
a, b: MyNat
zero
a * b * zero = a * (b * zero)
zero_is_0: zero = 0
zero_is_0
a, b: MyNat
zero
a * b * 0 = a * (b * 0)]
a, b: MyNat
zero
a * b * 0 = a * (b * 0)
    repeat
a, b: MyNat
zero
a * b * 0 = a * (b * 0)
      rw [
a, b: MyNat
zero
a * b * 0 = a * (b * 0)
mul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zero
Goals accomplished! 🐙]
a, b: MyNat
zero
0 = a * 0
  | 
succ: MyNat → MyNat
succ 
c: MyNat
c 
ih: a * b * c = a * (b * c)
ih =>
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * succ c = a * (b * succ c)
    rw [
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * succ c = a * (b * succ c)
mul_succ: ∀ (a b : MyNat), a * succ b = a * b + a
mul_succ
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * c + a * b = a * (b * succ c)]
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * c + a * b = a * (b * succ c)
    rw [
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * c + a * b = a * (b * succ c)
mul_succ: ∀ (a b : MyNat), a * succ b = a * b + a
mul_succ
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * c + a * b = a * (b * c + b)]
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * c + a * b = a * (b * c + b)
    rw [
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * b * c + a * b = a * (b * c + b)
ih: a * b * c = a * (b * c)
ih
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * (b * c) + a * b = a * (b * c + b)]
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * (b * c) + a * b = a * (b * c + b)
    rw [
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * (b * c) + a * b = a * (b * c + b)
mul_add: ∀ (t a b : MyNat), t * (a + b) = t * a + t * b
mul_add
a, b, c: MyNat
ih: a * b * c = a * (b * c)
succ
a * (b * c) + a * b = a * (b * c) + a * b]
Goals accomplished! 🐙

A mathematician could now remark that you have proved that the natural numbers form a monoid under multiplication.

-- instance : AddMonoid MyNat where
--   add_zero := add_zero
--   zero_add := zero_add
--   add_assoc := add_assoc
--   nsmul :=  λ x y => (myNatFromNat x) * y
--   nsmul_zero' := zero_mul
--   nsmul_succ' n x := by
--     simp

-- BUGBUG: complete these instances...

Next up is Multiplication Level 6.