import MyNat.Addition -- imports addition.
namespace MyNat
open MyNat

Addition world

Level 2: add_assoc -- associativity of addition.

It's well-known that (1 + 2) + 3 = 1 + (2 + 3) -- if you have three numbers to add up, it doesn't matter which of the additions you do first. This fact is called associativity of addition by mathematicians, and it is not obvious. For example, subtraction really is not associative: (6 - 2) - 1 is really not equal to 6 - (2 - 1). We are going to have to prove that addition, as defined the way we've defined it, is associative.

To prove associativity of addition it is handy to recall that addition was defined by recursion on the right-most variable. This means you can use induction on the right-most variable (try other variables at your peril!). Note that when Lean writes a + b + c, it means (a + b) + c. If it wants to talk about a + (b + c) it will put the brackets in explicitly.

Reminder: you are done when you see "Goals accomplished 🎉" in the InfoView, and no errors in the VS Code Problems list.

Lemma

On the set of natural numbers, addition is associative. In other words, for all natural numbers a, b and c, we have (a + b) + c = a + (b + c).

lemma 
add_assoc: ∀ (a b c : MyNat), a + b + c = a + (b + c)
add_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 + 0 = a + (b + 0)
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)
    rw [
a, b: MyNat
zero
a + b + 0 = a + (b + 0)
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, b: MyNat
zero
a + b = a + (b + 0)]
a, b: MyNat
zero
a + b = a + (b + 0)
    rw [
a, b: MyNat
zero
a + b = a + (b + 0)
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, b: MyNat
zero
a + b = a + b]
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
c: MyNat
c 
ih: a + b + c = a + (b + c)
ih =>
    -- ⊢ (a + b) + succ d = a + (b + succ d)
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)
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = a + (b + succ c)]
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = a + (b + succ c)
    rw [
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = a + (b + succ c)
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = a + succ (b + c)]
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = a + succ (b + c)
    rw [
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = a + succ (b + c)
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = succ (a + (b + c))]
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = succ (a + (b + c))
    rw [
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + b + c) = succ (a + (b + c))
ih: a + b + c = a + (b + c)
ih
a, b, c: MyNat
ih: a + b + c = a + (b + c)
succ
succ (a + (b + c)) = succ (a + (b + c))]
Goals accomplished! 🐙

On to Level 3.