/-
COMP2065-IFR Exercise 04
(Booleans) 

    This exercise has 2 parts.

    The first part is "logic chess" which has slightly different rules
    than logic poker but see below. The 2nd part asks you to prove that
    orb on booleans corresponds to the logical or and define an operation
    to compute existential quantification on booleans and prove it correct. 

    Don't worry, if you can't do the existential quantification part. 
    This is intended as a challenge and only counts for 20% of the 
    exercise. 
-/

namespace ex04
def bnot : bool → bool 
| tt := ff
| ff := tt 

def band : bool → bool → bool 
| tt b := b
| ff b := ff

def bor : bool → bool → bool 
| tt b := tt
| ff b := b

/- --- Do not add/change anything above this line --- -/


local notation (name := band) x && y := band x y 
local notation (name := bor) x || y := bor x y
/-
If you get an error update your lean or use:
local notation x && y := band x y 
local notation x || y := bor x y
-/


prefix `!`:90 := bnot

/-
PART I (60%)
============
Logic chess

Unlike logic poker in logic chess there is no guessing. You either
prove the proposition or you prove its negation.

Consider the following examples:
-/
def Ch0 := ∀ x : bool, x=x
def Ch00 := ∀ x : bool, x ≠ x

/- the first one is provable, hence we prove it -/

theorem ch0 : Ch0 :=
begin
  assume x,
  reflexivity
end

/- the second one is false, hence we prove its negation -/

theorem ch00 : ¬ Ch00 :=
begin
  assume h,
  have g : tt ≠ tt,
  apply h,
  apply g,
  reflexivity,
end


def Ch01 := ∀ x : bool, ! x = x
def Ch02 := ∀ x:bool,∃ y:bool, x = y
def Ch03 := ∃ x:bool,∀ y:bool, x = y
def Ch04 := ∀ x y : bool, x = y → ! x = ! y
def Ch05 := ∀ x y : bool, !x = !y → x = y
def Ch06 := ∀ x y z : bool, x=y ∨ y=z 
def Ch07 := ∃ b : bool, ∀ y:bool, b || y = y 
def Ch08 := ∃ b : bool, ∀ y:bool, b || y = b
def Ch09 := ∀ x : bool, (∀ y : bool, x && y = y) ↔ x = tt 
def Ch10 := ∀ x y : bool, x && y = y ↔ x = ff

/-
Name your theorems ch01, ch02, ..., ch10. chXX should either
be a proof of ChXX or a proof of ¬ ChXX, so either delete the
? or replace it by a ¬.
-/

theorem ch01 : ¬ Ch01 :=
begin
  assume h,
  have g: !tt = tt,
  apply h,
  dsimp[bnot] at g,
  contradiction,
end

theorem ch02 : Ch02 :=
begin
  assume x,
  existsi x,
  reflexivity,
end

theorem ch03 : ¬ Ch03 :=
begin
  assume h,
  cases h with x h1,
  have g: x = tt,
  apply h1,
  have f: x = ff,
  apply h1,
  rewrite g at f,
  contradiction,
end

theorem ch04 : Ch04 :=
begin
  assume x y h,
  rewrite h,
end

theorem ch05 : Ch05 :=
begin
  assume x y h,
  cases x,
  cases y,
  reflexivity,
  dsimp[bnot] at h,
  contradiction,
  cases y,
  dsimp[bnot] at h,
  contradiction,
  reflexivity,
end

theorem ch06 : ¬ Ch06 :=
begin
  assume h,
  have g: tt = ff ∨ ff = tt,
  apply h,
  cases g,
  contradiction,
  contradiction,
end

theorem ch07 : Ch07 :=
begin
  existsi ff,
  assume y,
  cases y,
  dsimp[bor],
  reflexivity,
  dsimp[bor],
  reflexivity,
end

theorem ch08 : Ch08 :=
begin
  existsi tt,
  assume y,
  dsimp[bor],
  reflexivity,
end

theorem ch09 : Ch09 :=
begin
  assume x,
  cases x,
  have h1: (∀ (y : bool), ff&&y = y) → ff = tt,
  assume h,
  have g: ff&&tt = tt,
  apply h,
  dsimp[band] at g,
  contradiction,
  have h2: ff = tt → (∀ (y : bool), ff&&y = y),
  assume h,
  contradiction,
  constructor,
  apply h1,
  apply h2,
  have h1: (∀ (y : bool), tt&&y = y) → tt = tt,
  assume h,
  reflexivity,
  have h2: tt = tt → (∀ (y : bool), tt&&y = y),
  assume h,
  assume y,
  dsimp[band],
  reflexivity,
  constructor,
  apply h1,
  apply h2,
end

theorem ch10 : ¬ Ch10 :=
begin
  assume h,
  have g: tt&&tt = tt,
  dsimp[band],
  reflexivity,
  have t: tt&&tt = tt ↔ tt = ff,
  apply h,
  have m: tt&&tt = tt → tt = ff,
  cases t with t_mp t_mpr,
  exact t_mp,
  have n: tt = ff,
  apply m,
  exact g,
  contradiction,
end

/- 
PART II (40%)
=============

Show that 
(∀ x : A, PP x ∨  QQ x) →  ((∀ x : A, PP x) ∨  (∀ x : A, QQ x)
is not a tautology by constructing a counterexample. 
Tha is prove the following theorem:
-/
theorem cex : 
  ¬ ∀ A : Type, ∀ PP QQ : A → Prop,
   ((∀ x : A, PP x ∨  QQ x) →  ((∀ x : A, PP x) ∨  (∀ x : A, QQ x))) :=
begin
   sorry  
end

/- --- Do not add/change anything below this line --- -/
end ex04

solve cex. only use the tactics that have been introduced in the file.