8. Booleans (2)

31/10/22

variable P : Prop
variables A B : Type
variable R : A → B → Prop
variable PP : A → Prop
variable QQ : A → Prop

open classical

theorem raa : ¬ ¬ P → P := 
begin
  assume nnp,
  cases (em P) with p np,
    exact p,
    have f : false,
      apply nnp,
      exact np,
    cases f,
end



/- 
inductive bool : Tyoe
| tt : bool
| ff : bool

tt and ff are the only elements of ∀ x : bool, x=tt ∨ x=ff
tt ≠ ff

-/

-- suits = {diamond, heats, spades, clubs}

inductive suit : Type
| diamond : suit
| hearts : suit
| spades : suit
| clubs : suit 

-- suit.diamond

open suit

-- diamond

-- define color = {black, red}
-- has_color : suit → color

inductive false : Prop

inductive empty : Type


def is_tt : bool → Prop
| tt := true
| ff := false

example : tt ≠ ff :=
begin
  assume h,
  change (is_tt ff),
  rewrite← h,
  dsimp [is_tt],
  constructor,
end


example : tt ≠ ff :=
begin
  assume h,
  contradiction,
end


-- local notation x && y := band x y,

theorem dm2_b :
∀ x y : bool, bnot (band x y) = bor (bnot x) (bnot y) := -- ! (x & y) = !x | !y
begin
  assume x y,
  cases x,
  -- ! (ff & y) = ! ff = tt
  -- ! ff | !y = tt | !y = tt
  dsimp [bnot,band,bor],
  reflexivity,
  -- !(tt & y) = ! y
  -- ! tt | ! y == ff | ! y = !y
  dsimp [bnot,band,bor],
  reflexivity,
end

theorem and_ok : ∀ x y : bool,
  is_tt (band x y)
  ↔ is_tt x ∧ is_tt y :=
begin
  assume x y,
  constructor,
  cases x,
  assume h,
  dsimp [band,is_tt] at h,
  cases h,

  assume h,
  dsimp [band] at h,
  constructor,
  dsimp [is_tt],
  constructor,

  exact h,

  assume h,
  cases h with hx hy,
  cases x,
  cases hx,
  
  dsimp [band],
  exact hy,

end

-- classical logic Prop = bool

/-
isPrime : ℕ → Prop
isPrimeB : ℕ → bool

∀ n : ℕ, isPrime n ↔ is_tt (isPrimeB n)

halts : Prog → Prop
-- halts p = program will terminate
-- Prog = Turning machine

haltsB : Prop → bool
∀ p : Prog, halts p ↔ is_tt (haltsB p)

Turning : there 

-/