import MyNat.Addition
import MyNat.Multiplication
import AdditionWorld.Level1 -- zero_add
import AdditionWorld.Level2 -- add_assoc
namespace MyNat
open MyNat

Multiplication World

Level 4: mul_add

Where are we going? Well we want to prove mul_comm and mul_assoc, i.e. that a * b = b * a and (a * b) * c = a * (b * c). But we also want to establish the way multiplication interacts with addition, i.e. we want to prove that we can "expand out the brackets" and show a * (b + c) = (a * b) + (a * c). The technical term for this is "left distributivity of multiplication over addition" (there is also right distributivity, which we'll get to later).

Note the name of this proof -- mul_add. And note the left hand side -- a * (b + c), a multiplication and then an addition. I think mul_add is much easier to remember than "left_distrib", an alternative name for the proof of this lemma.

Lemma

Multiplication is distributive over addition. In other words, for all natural numbers a, b and t, we have t(a + b) = ta + tb.

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

def 
left_distrib: ∀ (t a b : MyNat), t * (a + b) = t * a + t * b
left_distrib := 
mul_add: ∀ (t a b : MyNat), t * (a + b) = t * a + t * b
mul_add -- the "proper" name for this lemma

Next up is Multiplication Level 5.