10. Addition & commutative monoid

07/11/22

/-
natural numbers ℕ : {0,1,2,..}

Piano Arithmetic
  zero : ℕ 
  succ : ℕ → ℕ 

suc(suc(suc(zer0))) 3
structural recursion 
induction

double ℕ → ℕ 
  double zero = zero
  double (succ n) = succ(succ(double n))

half ℕ → ℕ  

-/

namespace l11
set_option pp.structure_projections true
open nat

def add : ℕ → ℕ → ℕ
| n zero := n
| n (succ m) := succ (add n m)

#reduce (add 7 3)

local notation (name := add)
  m + n := add m n

#reduce (7+3)

theorem lneutr: ∀ n : ℕ , 0 + n = n :=
begin
  assume n,
  induction n with n' ih,
  dsimp[(+),add],
  refl,
  dsimp[(+),add],
  rewrite ih,
  
end

theorem rneutr: ∀ n : ℕ , n + 0 = n :=
begin
  assume n,
  dsimp[(+), add],
  refl,
end


theorem assoc : ∀ l m n : ℕ, (l + m) + n = l + (m + n) :=
begin
  assume l m n,
  induction n with n' ih,
  -- (l+m)+0 = l+m
  -- l+(m+0) = l+m
  dsimp[(+),add],
  refl,

  -- (l + m) + succ n' = succ((l+m) + n')
  -- l + (m + succ n') = l+(succ (m + n'))
  -- = succ (l + (m + n'))
  dsimp[(+),add],
  rewrite ih,
end

lemma add_succ : ∀ m n : ℕ, (succ m) + n = succ (m + n) :=
begin
  assume m n,
  induction n with n' ih,
  dsimp[(+),add],
  refl,

  dsimp[(+),add],
  rewrite ih,
  
end

theorem comm : ∀ m n : ℕ, m + n = n + m :=
begin
  assume m n,
  induction n with n' ih,
  dsimp[(+),add],
  rewrite lneutr,
  
  rewrite add_succ,
  dsimp[(+),add],
  rewrite ih,
end

end l11