12. Deciding Equality of Natural Numbers (ℕ)

14/11/22

namespace l13
set_option pp.structure_projections false
open nat

def eqb : ℕ → ℕ → bool 
  | zero zero := tt
  | (succ m) zero := ff
  | zero (succ n) := ff
  | (succ m) (succ n) := eqb m n

#eval (eqb 2 2)

-- decides equality (=)
variables A B : Type

example : ∀ f : A → B, ∀ x y, x = y → f x = f y :=
begin
  assume f x y h,
  rewrite h,
end
/-
example : ∀ f : A → B, ∀ x y, f x = f y → x = y :=
-/

lemma eqb_sound : ∀ n : ℕ, eqb n n = tt :=
begin
  assume n,
  induction n with n' ih,
  refl,
  
  dsimp[eqb],
  exact ih,
end

lemma eqb_compl : ∀ m n : ℕ, eqb m n = tt → m = n :=
begin
  assume m,
  induction m with m' ih_m,
  assume n,
  cases n with n',
  assume h,
  refl,
  assume h,
  dsimp[eqb] at h,
  contradiction,
  assume n,
  cases n with n',
  dsimp[eqb],
  assume h,
  contradiction,
  assume h,
  apply congr_arg succ,
  apply ih_m,
  dsimp[eqb] at h,
  exact h,
end

theorem eqb_ok : ∀ m n : ℕ, eqb m n = tt ↔ m = n :=
begin
  assume m n,
  constructor,
  apply eqb_compl,
  
  assume h,
  rewrite h,
  apply eqb_sound,
end

-- we say eqb *decides* = 
-- P : A → Prop
-- f : A → bool
-- f *decides* P means
-- ∀ a:A, P a ↔ f a = tt
-- Prime : ℕ → Prop
-- is_prime : ℕ → bool
-- can we decide any predicate? 


def Hard (f : ℕ → bool) : Prop :=
  ∀ n : ℕ, f n = tt


-- is there
-- hard : (ℕ → bool) → bool
-- decides Hard?


end l13