import MyNat.Addition
import MyNat.Multiplication
import AdditionWorld.Level6 -- add_right_comm
namespace MyNat
open MyNat

Multiplication World

Level 6: succ_mul

We now begin our journey to mul_comm, the proof that a * b = b * a. We'll get there in level 8. Until we're there, it is frustrating but true that we cannot assume commutativity. We have mul_succ but we're going to need succ_mul (guess what it says -- maybe you are getting the hang of Lean's naming conventions).

Remember also that we have tools like

• add_right_comm a b c : a + b + c = a + c + b

These things are the tools we need to slowly build up the results which we will need to do mathematics "normally". We also now have access to Lean's simp tactic, which will solve any goal which just needs a bunch of rewrites of add_assoc and add_comm. Use if you're getting lazy!

Lemma

For all natural numbers a and b, we have succ a * b = ab + b.

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

Next up is Multiplication Level 7.