9. Natural numbers & Peano arithmetic

04/11/22

/- 
Peano Arithmetic
0 is a natural number
if n is a naturl number
then 0(succ)+n is a natural number

inductive ind: Type
| zero : not
| succ : not → not

∀ n : ℕ, succ ≠ succ n
∀ m n : ℕ, succ m = succ n → m = n
∀ n : ℕ, n = 0 ∨ n = ℕ ∨ n = 2 ∨ ....


Principle of induction
∀ ‽ ℕ → Prop, P O → (∀ ℕ, P n → (suc n)) → ∀ n : ℕ, P n

-/


namespace l09
set_option pp.structure_instances false

open nat

#check (succ (succ (succ zero)))
#check 3
#check 101

example : ∀ n : ℕ, 0 ≠ succ n :=
begin
  assume n h,
  contradiction,
end 

def pred : ℕ → ℕ 
| zero := zero
| (succ m) := m

#eval (pred 7)

example : ∀ m n : ℕ, succ m = succ n → m = n := 
begin
  assume m n h,
  change (pred (succ m)) = n,
  rewrite h,
  dsimp [pred],
  reflexivity,
end

example : ∀ m n : ℕ, succ m = succ n → m = n := 
begin
  assume m n h,
  injection h,
end

example : ∀ P : ℕ → Prop,
  P zero
  → (∀ n : ℕ, P n → P (succ n))
  → ∀ m : ℕ, P m := 
  begin
    assume P p0 ps m,
    induction m with m' ih,
    exact p0,
    apply ps,
    exact ih,
  end

def double : ℕ → ℕ 
| zero := zero
| (succ m) := succ (succ (double m))

#eval double 10

def half : ℕ → ℕ 
| zero := zero
| (succ zero) := zero
| (succ (succ m)) := succ (half m)

#eval half 10

example : ∀ n : ℕ, half(double n) = n := -- proof by induction
begin
  assume n,
  induction n with n' ih,
  dsimp [double],
  dsimp [half],
  reflexivity,

  dsimp [double],
  dsimp [half],
  rewrite ih,
end

example : ∀ n : ℕ, double(half n) = n :=
begin
  sorry,
end



end l09