-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := Iff.intro
(fun hpq => ⟨ hpq.right, hpq.left⟩ )
(fun hqp => ⟨ hqp.right, hqp.left ⟩ )
example : p ∨ q ↔ q ∨ p := Iff.intro
(fun (hpq: p ∨ q) => Or.elim hpq (fun hp => Or.inr hp) (fun hq => Or.inl hq))
(fun (hqp: q ∨ p) => Or.elim hqp (fun hq => Or.inr hq) (fun hp => Or.inl hp))
-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := ⟨
fun (h: (p ∧ q) ∧ r) =>
have hpq := h.left
have hr := h.right
have hp := hpq.left
have hq := hpq.right
⟨ hp, hq, hr⟩,
fun (h: p ∧ (q ∧ r)) =>
have hp := h.left
have hqr := h.right
have hq := hqr.left
have hr := hqr.right
⟨ ⟨ hp, hq⟩ , hr ⟩⟩
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := ⟨
fun (h: (p ∨ q) ∨ r) => Or.elim h
(show p ∨ q → p ∨ (q ∨ r) from fun hpq =>
(Or.elim hpq
(fun hp => Or.inl hp)
(fun hq => Or.inr (Or.inl hq))))
(show r → p ∨ (q ∨ r) from fun hr => Or.inr (Or.inr hr)),
fun (h: p ∨ (q ∨ r)) => Or.elim h
(show p → (p ∨ q) ∨ r from fun hp => Or.inl (Or.inl hp))
(show q ∨ r → (p ∨ q) ∨ r from fun hqr =>
(Or.elim hqr
(fun hq => Or.inl (Or.inr hq))
(fun hr => Or.inr hr)))⟩
-- distributivity
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := ⟨
fun (h: p ∧ (q ∨ r)) =>
have hp : p := h.left
have hqr : q ∨ r := h.right
Or.elim hqr
(fun hq => Or.inl ⟨hp, hq⟩)
(fun hr => Or.inr ⟨hp, hr⟩),
fun (h: (p ∧ q) ∨ (p ∧ r)) =>
Or.elim h
(fun hpq: p ∧ q =>
have hp := hpq.left
have hq := hpq.right
⟨hp, Or.inl hq⟩)
(fun hpr: p ∧ r =>
have hp := hpr.left
have hr := hpr.right
⟨hp, Or.inr hr⟩
)⟩
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := ⟨
fun (h: p ∨ (q ∧ r)) => Or.elim h
(fun hp => ⟨Or.inl hp, Or.inl hp⟩)
(fun hqr =>
have hq := hqr.left
have hr := hqr.right
⟨Or.inr hq, Or.inr hr⟩),
fun (h: (p ∨ q) ∧ (p ∨ r)) =>
have hpq := h.left
have hpr := h.right
Or.elim hpq
(fun hp => Or.inl hp)
(fun hq => Or.elim hpr
(fun hp => Or.inl hp)
(fun hr => Or.inr ⟨hq, hr⟩))
⟩
-- other properties
example : (p → (q → r)) ↔ (p ∧ q → r) := ⟨
fun (h: p → (q → r)) => fun (hpq: p∧q) => h hpq.left hpq.right,
fun (h: p ∧ q → r) => fun (hp: p) => fun (hq: q) => h ⟨hp, hq⟩⟩
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := ⟨
fun (h: (p ∨ q) → r) =>
⟨fun (hp: p) => h (Or.inl hp), fun (hq: q) => h (Or.inr hq)⟩,
fun (h: (p → r) ∧ (q → r)) => fun hpq: p ∨ q => Or.elim hpq
(fun hp => h.left hp)
(fun hq => h.right hq)⟩
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := ⟨
fun (h: ¬(p ∨ q)) => ⟨fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)⟩,
fun (h: ¬p ∧ ¬q) => fun (hpq: p ∨ q) => Or.elim hpq
(fun hp => And.left h hp)
(fun hq => And.right h hq)⟩
example : ¬p ∨ ¬q → ¬(p ∧ q) :=
fun (h: ¬p ∨ ¬q) => fun (hpq: p ∧ q) =>
Or.elim h
(fun nhp => nhp hpq.left)
(fun nhq => nhq hpq.right)
example : ¬(p ∧ ¬p) := fun h => h.right h.left
example : p ∧ ¬q → ¬(p → q) :=
fun h => fun hp_to_hq => h.right (hp_to_hq h.left)
example : ¬p → (p → q) :=
fun nhp => fun hp => absurd hp nhp
example : (¬p ∨ q) → (p → q) :=
fun h => fun hp => Or.elim h (fun hnp => absurd hp hnp) id
example : p ∨ False ↔ p := ⟨fun h => Or.elim h id False.elim,Or.inl⟩
example : p ∧ False ↔ False := ⟨And.right, fun f => ⟨False.elim f, f⟩⟩
example : (p → q) → (¬q → ¬p) :=
fun hpq => fun hnq => fun hp => hnq (hpq hp)
-- Classical
open Classical
variable (p q r : Prop)
-- #check em
example : (p → q ∨ r) → ((p → q) ∨ (p → r)) :=
fun h => em
example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry
example : ¬(p → q) → p ∧ ¬q := sorry
example : (p → q) → (¬p ∨ q) := sorry
example : (¬q → ¬p) → (p → q) := sorry
example : p ∨ ¬p := sorry
example : (((p → q) → p) → p) := sorry