11. Multiplicaiton & less-or-equal

11/11/22

import tactic
namespace l12
set_option pp.structure_projections false
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 [(+)],
    reflexivity,
    dsimp [(+)],
    rewrite ih,
end

theorem rneutr : 
  ∀ n : ℕ, n + 0 = n :=
begin
  assume n,
  dsimp [(+)],
  reflexivity,
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 [(+)],
  reflexivity,
  -- (l+m)+succ n'
  -- = succ ((l+m) + n')
  -- l+(m+succ n')
  -- = l+(succ (m + n'))
  -- = succ (l+(m+n'))
  dsimp [(+)],
  rewrite ih,
end

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

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

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

local notation (name := mult)
  m * n := mult m n 

#eval 2*3

-- (ℕ,*,1) is a commutative monoid
theorem mult_rneutr : 
  ∀ n : ℕ, n * 1 = n :=
begin
  sorry,
end

theorem mult_lneutr : 
  ∀ n : ℕ, 1 * n  = n :=
begin
  sorry,
end

theorem mult_assoc : ∀ l m n : ℕ , 
  (l * m) * n = l * (m * n) :=
begin
  sorry,
end

theorem mult_comm :  ∀ m n : ℕ ,
  m * n = n * m :=
begin
  sorry,
end


/-
actually + and * interact nicely. 
We have distributivity laws.

-/

theorem mult_zero_l : ∀ n : ℕ , 
  0 * n = 0 :=
begin
  sorry,
end

theorem mult_zero_r : ∀ n : ℕ , 
  n * 0 = 0 :=
begin
  sorry,
end

theorem mult_distr_l :  ∀ l m n : ℕ , 
  (m + n) * l = m * l + n * l :=
begin
  sorry,
end

theorem mult_distr_r :  ∀ l m n : ℕ , 
  l * (m + n) = l * m + l * n :=
begin
  sorry,
end

/-
(ℕ,+,0,*,1) are a semi-ring
(ℤ,+,0,minus,*,1) is a ring
(ℚ,+,0,minus,*,1,1/..) is a field
a-b = a+minus b
a/b = a * 1/b
-/

def le(m n : ℕ) : Prop 
:= ∃ k : ℕ, k + m = n 

local notation (name := le)
  m ≤ n := le m n 

example : 2 ≤ 3 :=
begin
  dsimp [(≤)],
  existsi 1,
  reflexivity,
end 

example : ¬ (3 ≤ 2) :=
begin
  assume h,
  dsimp [(≤)] at h,
  cases h with k hh,
  have h2 : k+2 = 1,
  injection hh,
  have h3:k+1 = 0,
  injection h2,
  contradiction,
end

-- ≤ is a partial order
-- preorder + antisymmetry
-- reflexive : n ≤ n
-- transitive :
--    m ≤ n → n ≤ l → m ≤ l
-- anti-symmetric :
--    m ≤ n → n ≤ m → m = n

theorem le_refl : ∀ n : ℕ, 
  n ≤ n :=
begin
  assume n,
  dsimp [(≤)],
  existsi 0,
  apply lneutr,
end 









end l12

theorem binom : ∀ x y : ℕ, 
(x + y)^2 = x^2 + 2*x*y + y^2 :=
begin
  assume x y,
  ring,
end 

#print binom