168 lines
4.4 KiB
Plaintext
168 lines
4.4 KiB
Plaintext
/-! # Avigad.Chapter3
|
||
|
||
Propositions and Proofs
|
||
-/
|
||
|
||
/-! ### Exercise 1
|
||
|
||
Prove the following identities.
|
||
-/
|
||
|
||
namespace Avigad.Chapter3
|
||
|
||
namespace ex1
|
||
|
||
open or
|
||
|
||
variable (p q r : Prop)
|
||
|
||
-- Commutativity of ∧ and ∨
|
||
theorem and_comm' : p ∧ q ↔ q ∧ p :=
|
||
Iff.intro
|
||
(fun ⟨hp, hq⟩ => show q ∧ p from ⟨hq, hp⟩)
|
||
(fun ⟨hq, hp⟩ => show p ∧ q from ⟨hp, hq⟩)
|
||
|
||
theorem or_comm' : p ∨ q ↔ q ∨ p :=
|
||
Iff.intro
|
||
(fun h => h.elim Or.inr Or.inl)
|
||
(fun h => h.elim Or.inr Or.inl)
|
||
|
||
-- Associativity of ∧ and ∨
|
||
theorem and_assoc : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
|
||
Iff.intro
|
||
(fun ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, hq, hr⟩)
|
||
(fun ⟨hp, hq, hr⟩ => ⟨⟨hp, hq⟩, hr⟩)
|
||
|
||
theorem or_assoc' : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
|
||
Iff.intro
|
||
(fun h₁ => h₁.elim
|
||
(fun h₂ => h₂.elim Or.inl (Or.inr ∘ Or.inl))
|
||
(Or.inr ∘ Or.inr))
|
||
(fun h₁ => h₁.elim
|
||
(Or.inl ∘ Or.inl)
|
||
(fun h₂ => h₂.elim (Or.inl ∘ Or.inr) Or.inr))
|
||
|
||
-- Distributivity
|
||
theorem and_or_left : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
|
||
Iff.intro
|
||
(fun ⟨hp, hqr⟩ => hqr.elim (Or.inl ⟨hp, ·⟩) (Or.inr ⟨hp, ·⟩))
|
||
(fun h₁ => h₁.elim
|
||
(fun ⟨hp, hq⟩ => ⟨hp, Or.inl hq⟩)
|
||
(fun ⟨hp, hr⟩ => ⟨hp, Or.inr hr⟩))
|
||
|
||
theorem or_and_left : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
|
||
Iff.intro
|
||
(fun h => h.elim
|
||
(fun hp => ⟨Or.inl hp, Or.inl hp⟩)
|
||
(fun ⟨hq, hr⟩ => ⟨Or.inr hq, Or.inr hr⟩))
|
||
(fun ⟨h₁, h₂⟩ => h₁.elim
|
||
Or.inl
|
||
(fun hq => h₂.elim Or.inl (fun hr => Or.inr ⟨hq, hr⟩)))
|
||
|
||
-- Other properties
|
||
theorem imp_imp_iff_and_imp : (p → (q → r)) ↔ (p ∧ q → r) :=
|
||
Iff.intro
|
||
(fun h ⟨hp, hq⟩ => h hp hq)
|
||
(fun h hp hq => h ⟨hp, hq⟩)
|
||
|
||
theorem or_imp : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
||
Iff.intro
|
||
(fun h =>
|
||
have h₁ : p → r := h ∘ Or.inl
|
||
have h₂ : q → r := h ∘ Or.inr
|
||
show (p → r) ∧ (q → r) from ⟨h₁, h₂⟩)
|
||
(fun ⟨h₁, h₂⟩ h => h.elim h₁ h₂)
|
||
|
||
theorem nor_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
|
||
Iff.intro
|
||
(fun h => ⟨h ∘ Or.inl, h ∘ Or.inr⟩)
|
||
(fun h₁ h₂ => h₂.elim (absurd · h₁.left) (absurd · h₁.right))
|
||
|
||
theorem not_and_or_mpr : ¬p ∨ ¬q → ¬(p ∧ q) :=
|
||
fun h₁ h₂ => h₁.elim (absurd h₂.left ·) (absurd h₂.right ·)
|
||
|
||
theorem and_not_self : ¬(p ∧ ¬p) :=
|
||
fun h => absurd h.left h.right
|
||
|
||
theorem not_imp_o_and_not : p ∧ ¬q → ¬(p → q) :=
|
||
fun ⟨hp, nq⟩ hpq => absurd (hpq hp) nq
|
||
|
||
theorem false_elim_self : ¬p → (p → q) :=
|
||
fun np hp => absurd hp np
|
||
|
||
theorem not_or_imp_imp : (¬p ∨ q) → (p → q) :=
|
||
fun npq hp => npq.elim (absurd hp ·) id
|
||
|
||
theorem or_false_iff : p ∨ False ↔ p :=
|
||
Iff.intro (fun hpf => hpf.elim id False.elim) Or.inl
|
||
|
||
theorem and_false_iff : p ∧ False ↔ False :=
|
||
Iff.intro (fun ⟨_, hf⟩ => hf) False.elim
|
||
|
||
theorem imp_imp_not_imp_not : (p → q) → (¬q → ¬p) :=
|
||
fun hpq nq hp => absurd (hpq hp) nq
|
||
|
||
end ex1
|
||
|
||
/-! ### Exercise 2
|
||
|
||
Prove the following identities. These require classical reasoning.
|
||
-/
|
||
|
||
namespace ex2
|
||
|
||
open Classical
|
||
|
||
variable (p q r s : Prop)
|
||
|
||
theorem imp_or_mp (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
|
||
fun h => (h hp).elim
|
||
(fun hr => Or.inl (fun _ => hr))
|
||
(fun hs => Or.inr (fun _ => hs))
|
||
|
||
theorem not_and_iff_or_not : ¬(p ∧ q) → ¬p ∨ ¬q :=
|
||
fun npq => (em p).elim
|
||
(fun hp => (em q).elim
|
||
(fun hq => False.elim (npq ⟨hp, hq⟩))
|
||
Or.inr)
|
||
Or.inl
|
||
|
||
theorem not_imp_mp : ¬(p → q) → p ∧ ¬q :=
|
||
fun h =>
|
||
have lhs : p := byContradiction
|
||
fun np => h (fun (hp : p) => absurd hp np)
|
||
⟨lhs, fun hq => h (fun _ => hq)⟩
|
||
|
||
theorem not_or_of_imp : (p → q) → (¬p ∨ q) :=
|
||
fun hpq => (em p).elim (fun hp => Or.inr (hpq hp)) Or.inl
|
||
|
||
theorem not_imp_not_imp_imp : (¬q → ¬p) → (p → q) :=
|
||
fun h hp => byContradiction
|
||
fun nq => absurd hp (h nq)
|
||
|
||
theorem or_not : p ∨ ¬p := em p
|
||
|
||
theorem imp_imp_imp : (((p → q) → p) → p) :=
|
||
fun h => byContradiction
|
||
fun np =>
|
||
suffices hp : p from absurd hp np
|
||
h (fun (hp : p) => absurd hp np)
|
||
|
||
end ex2
|
||
|
||
/-! ### Exercise 3
|
||
|
||
Prove `¬(p ↔ ¬p)` without using classical logic.
|
||
-/
|
||
|
||
namespace ex3
|
||
|
||
variable (p : Prop)
|
||
|
||
theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) :=
|
||
fun h => absurd hp (Iff.mp h hp)
|
||
|
||
end ex3
|
||
|
||
end Avigad.Chapter3
|