--
-- 4. Quantifiers and Equality
--

-- The Universal Quantifier

example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y :=
  fun h : ∀ x : α, p x ∧ q x =>
  fun y : α =>
  show p y from (h y).left

variable (α : Type) (r : α → α → Prop)
variable (trans_r : ∀ {x y z}, r x y → r y z → r x z)

variable (a b c : α)
variable (hab : r a b) (hbc : r b c)

#check trans_r
#check @trans_r
#check trans_r hab
#check trans_r hab hbc

-- Equality

#check Eq.refl
#check Eq.symm
#check Eq.trans

universe u
#check @Eq.refl.{u}
#check @Eq.symm.{u}
#check @Eq.trans.{u}

variable (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
example : a = d := (hab.trans hcb.symm).trans hcd

variable (α β : Type)

example (f : α → β) (a : α) : (fun x => f x) a = f a := Eq.refl _
example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2

variable (α : Type)
variable (a b : α)
variable (f g : α → Nat)
variable (h₁ : a = b)
variable (h₂ : f = g)

example : f a = f b := congrArg f h₁
example : f a = g a := congrFun h₂ a

variable (a : Nat) in
example : a + 0 = a := Nat.add_zero a

-- Calculational Proofs
variable (a b c d : Nat) in
variable (h1 : a = b) in
variable (h2 : b = c + 1) in
variable (h3 : c = d) in
variable (h4 : e = 1 + d) in
theorem T : a = e :=
  calc
    a = b     := h1
    _ = c + 1 := h2
    _ = d + 1 := congrArg Nat.succ h3
    _ = 1 + d := Nat.add_comm d 1
    _ = e     := h4.symm

-- The Existential Quantifier
example : ∃ x : Nat, x > 0 :=
  have h : 1 > 0 := Nat.zero_lt_succ 0
  Exists.intro 1 h

variable (α : Type) (p q : α → Prop) in
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  Exists.elim h
    fun w =>
    fun hw : p w ∧ q w => 
    Exists.intro w ⟨hw.right, hw.left⟩

#check @Exists.elim.{u}

#check Sigma

variable (α : Type) (p q : α → Prop) in
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩


-- More on the Proof Language
variable (f : Nat → Nat)
variable (h : ∀ x : Nat, f x ≤ f (x + 1))

example : f 0 ≤ f 3 :=
  have : f 0 ≤ f 1 := h 0
  have : f 0 ≤ f 2 := Nat.le_trans (by assumption) (h 1)
  show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2)

example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
  fun _ : f 0 ≥ f 1 =>
  fun _ : f 1 ≥ f 2 =>
  have : f 0 ≥ f 2 := Nat.le_trans ‹f 1 ≥ f 2› ‹f 0 ≥ f 1›
  have : f 0 ≤ f 2 := Nat.le_trans (h 0) (h 1)
  show f 0 = f 2 from Nat.le_antisymm this ‹f 0 ≥ f 2›

-- Exercises
variable (α : Type) (p q : α → Prop)

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
  have h1 : (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x :=
    fun h =>
      have h11 : ∀ (x : α), p x :=
        fun x : α => (h x).left
      have h12 : ∀ (x : α), q x :=
        fun x : α => (h x).right
      And.intro h11 h12
  have h2 : ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x :=
    fun h =>
      fun x : α =>
        ⟨h.left x, h.right x⟩
  Iff.intro h1 h2
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
  fun h1 =>
  fun h2 =>
  fun x : α =>
    show q x from (h1 x) (h2 x)

example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
  fun h =>
    h.elim
      (fun hp =>
        fun x => Or.inl (hp x))
      (fun hq =>
        fun x => Or.inr (hq x))

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example : α → ((∀ x : α, r) ↔ r) :=
  fun hα =>
    have h1 := fun h => h hα
    have h2 := fun hr => fun _ => hr
    Iff.intro h1 h2
open Classical in
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
  have h1 : (∀ (x : α), p x ∨ r) → (∀ (x : α), p x) ∨ r :=
    fun h =>
      sorry
  have h2 : (∀ (x : α), p x) ∨ r → ∀ (x : α), p x ∨ r :=
    fun h =>
      h.elim
        (fun hl =>
          fun hx =>
            Or.inl (hl hx))
        (fun hr =>
          fun hx =>
            Or.inr hr)
  Iff.intro h1 h2

example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
  have h1 : (∀ (x : α), r → p x) → r → ∀ (x : α), p x :=
    fun h =>
      fun hr =>
        fun x =>
          (h x) hr
  have h2 : (r → ∀ (x : α), p x) → ∀ (x : α), r → p x :=
    fun h =>
      fun x =>
        fun hr =>
          (h hr) x
  Iff.intro h1 h2


variable (men : Type) (barber : men)
variable (shaves : men → men → Prop)

open Classical in
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False :=
  have hbarber : shaves barber barber ↔ ¬shaves barber barber :=
    h barber
  (em (shaves barber barber)).elim
    (fun hbarberself =>
      have hnbarbarself := hbarber.mp hbarberself
      hnbarbarself hbarberself)
    (fun hnbarbarself =>
      hnbarbarself (hbarber.mpr hnbarbarself))