98 lines
2.6 KiB
Plaintext
98 lines
2.6 KiB
Plaintext
variable (p q r : Prop)
|
||
|
||
-- commutativity of ∧ and ∨
|
||
example : p ∧ q ↔ q ∧ p :=
|
||
Iff.intro (λ ⟨p,q⟩ => ⟨q,p⟩) (λ ⟨q,p⟩ => ⟨p,q⟩)
|
||
|
||
example : p ∨ q ↔ q ∨ p :=
|
||
Iff.intro
|
||
(λ
|
||
| Or.inl p => Or.inr p
|
||
| Or.inr q => Or.inl q)
|
||
(λ
|
||
| Or.inl q => Or.inr q
|
||
| Or.inr p => Or.inl p)
|
||
|
||
-- associativity of ∧ and ∨
|
||
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
|
||
Iff.intro
|
||
(λ ⟨⟨p,q⟩,r⟩ => ⟨p,⟨q,r⟩⟩)
|
||
(λ ⟨p,⟨q,r⟩⟩ => ⟨⟨p,q⟩,r⟩)
|
||
|
||
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
|
||
Iff.intro
|
||
(λ
|
||
| Or.inr r => Or.inr (Or.inr r)
|
||
| Or.inl (Or.inr q) => Or.inr (Or.inl q)
|
||
| Or.inl (Or.inl p) => Or.inl p)
|
||
(λ
|
||
| Or.inl p => Or.inl (Or.inl p)
|
||
| Or.inr (Or.inl q) => Or.inl (Or.inr q)
|
||
| Or.inr (Or.inr r) => Or.inr r)
|
||
|
||
-- distributivity
|
||
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
|
||
Iff.intro
|
||
(λ
|
||
| ⟨p, Or.inl q⟩ => Or.inl ⟨p,q⟩
|
||
| ⟨p, Or.inr r⟩ => Or.inr ⟨p,r⟩)
|
||
(λ
|
||
| Or.inl ⟨p,q⟩ => ⟨p,Or.inl q⟩
|
||
| Or.inr ⟨p,r⟩ => ⟨p,Or.inr r⟩)
|
||
|
||
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
|
||
Iff.intro
|
||
(λ
|
||
| Or.inl p => ⟨Or.inl p, Or.inl p⟩
|
||
| Or.inr ⟨q,r⟩ => ⟨Or.inr q, Or.inr r⟩)
|
||
(λ
|
||
| ⟨Or.inr q, Or.inr r⟩ => Or.inr ⟨q,r⟩
|
||
| ⟨Or.inl p, _⟩ => Or.inl p
|
||
| ⟨ _, Or.inl p⟩ => Or.inl p)
|
||
|
||
-- other properties
|
||
example : (p → (q → r)) ↔ (p ∧ q → r) :=
|
||
Iff.intro
|
||
(λ f ⟨p,q⟩ => f p q)
|
||
(λ f p q => f ⟨p,q⟩)
|
||
|
||
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
||
Iff.intro
|
||
(λ porqtor => And.intro (λ p => porqtor (Or.inl p)) (λ q => porqtor (Or.inr q)))
|
||
(λ
|
||
|⟨f, _⟩, Or.inl p => f p
|
||
|⟨_, g⟩, Or.inr q => g q)
|
||
|
||
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
|
||
Iff.intro
|
||
(λ nporq => And.intro (λ p => nporq (Or.inl p)) (λ q => nporq (Or.inr q)))
|
||
(λ
|
||
| ⟨np, _⟩, Or.inl p => np p
|
||
| ⟨_ ,nq⟩, Or.inr q => nq q)
|
||
|
||
example : ¬p ∨ ¬q → ¬(p ∧ q)
|
||
| Or.inl np, ⟨p,_⟩ => np p
|
||
| Or.inr nq, ⟨_,q⟩ => nq q
|
||
|
||
example : ¬(p ∧ ¬p) :=
|
||
λ ⟨p,np⟩ => np p
|
||
|
||
example : p ∧ ¬q → ¬(p → q) :=
|
||
λ ⟨p,nq⟩ ptoq => nq (ptoq p)
|
||
|
||
example : ¬p → (p → q) :=
|
||
λ np p => absurd p np
|
||
|
||
example : (¬p ∨ q) → (p → q)
|
||
| (Or.inl np), p => absurd p np
|
||
| (Or.inr q), _ => q
|
||
|
||
example : p ∨ False ↔ p :=
|
||
Iff.intro (λ porf => Or.elim porf id False.elim) (λ p => Or.inl p)
|
||
|
||
example : p ∧ False ↔ False :=
|
||
Iff.intro (λ ⟨_,f⟩ => f) (λ f => False.elim f)
|
||
|
||
example : (p → q) → (¬q → ¬p) :=
|
||
λ ptoq nq p => absurd (ptoq p) nq
|