160 lines
4.1 KiB
Plaintext
160 lines
4.1 KiB
Plaintext
variable (p q r : Prop)
|
||
|
||
-- commutativity of ∧ and ∨
|
||
example : p ∧ q ↔ q ∧ p := by
|
||
apply Iff.intro
|
||
· intro pandq
|
||
apply And.intro
|
||
· apply And.right pandq
|
||
· apply And.left pandq
|
||
· intro qandp
|
||
apply And.intro
|
||
· apply And.right qandp
|
||
· apply And.left qandp
|
||
|
||
example : p ∨ q ↔ q ∨ p := by
|
||
apply Iff.intro
|
||
· intro porq
|
||
cases porq with
|
||
| inl p => exact Or.inr p
|
||
| inr q => exact Or.inl q
|
||
· intro qorp
|
||
cases qorp with
|
||
| inl q => exact Or.inr q
|
||
| inr p => exact Or.inl p
|
||
|
||
-- associativity of ∧ and ∨
|
||
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
|
||
apply Iff.intro
|
||
· intro pqandr
|
||
apply And.intro
|
||
· exact And.left (And.left pqandr)
|
||
· apply And.intro
|
||
· exact And.right (And.left pqandr)
|
||
· exact And.right pqandr
|
||
· intro pandqr
|
||
apply And.intro
|
||
· apply And.intro
|
||
· exact And.left pandqr
|
||
· exact And.left (And.right pandqr)
|
||
· exact And.right (And.right pandqr)
|
||
|
||
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
|
||
apply Iff.intro
|
||
· intro pqorr
|
||
cases pqorr with
|
||
| inr r => apply Or.inr (Or.inr r)
|
||
| inl porq => cases porq with
|
||
| inl p => apply Or.inl p
|
||
| inr q => apply Or.inr (Or.inl q)
|
||
· intro porqr
|
||
cases porqr with
|
||
| inl p => apply Or.inl (Or.inl p)
|
||
| inr qorr => cases qorr with
|
||
| inr r => apply Or.inr r
|
||
| inl q => apply Or.inl (Or.inr q)
|
||
|
||
-- distributivity
|
||
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
|
||
apply Iff.intro
|
||
· intro pandqorr
|
||
cases pandqorr with
|
||
| intro p qor => cases qor with
|
||
| inl q => apply Or.inl (And.intro p q)
|
||
| inr r => apply Or.inr (And.intro p r)
|
||
· intro pandqorpandr
|
||
cases pandqorpandr with
|
||
| inl pandq => apply And.intro (And.left pandq) (Or.inl (And.right pandq))
|
||
| inr pandr => apply And.intro (And.left pandr) (Or.inr (And.right pandr))
|
||
|
||
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
|
||
apply Iff.intro
|
||
· intro porqandr
|
||
cases porqandr with
|
||
| inl p => apply And.intro (Or.inl p) (Or.inl p)
|
||
| inr qandr => apply And.intro (Or.inr (And.left qandr)) (Or.inr (And.right qandr))
|
||
· intro porqandporr
|
||
cases And.left porqandporr with
|
||
| inl p => apply Or.inl p
|
||
| inr q => cases And.right porqandporr with
|
||
| inl p => apply Or.inl p
|
||
| inr r => apply Or.inr (And.intro q r)
|
||
|
||
-- other properties
|
||
example : (p → (q → r)) ↔ (p ∧ q → r) := by
|
||
apply Iff.intro
|
||
· intro ptoqtor
|
||
intro pandq
|
||
exact ptoqtor (And.left pandq) (And.right pandq)
|
||
· intro pandqtor
|
||
intro p
|
||
intro q
|
||
exact pandqtor (And.intro p q)
|
||
|
||
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := by
|
||
apply Iff.intro
|
||
· intro porqtor
|
||
apply And.intro
|
||
· intro p
|
||
exact porqtor (Or.inl p)
|
||
· intro q
|
||
exact porqtor (Or.inr q)
|
||
· intro ptorandqtor
|
||
intro porq
|
||
cases porq with
|
||
| inl p => exact (And.left ptorandqtor) p
|
||
| inr q => exact (And.right ptorandqtor) q
|
||
|
||
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
|
||
apply Iff.intro
|
||
· intro nporq
|
||
apply And.intro
|
||
· intro p
|
||
exact nporq (Or.inl p)
|
||
· intro q
|
||
exact nporq (Or.inr q)
|
||
· intro npandnq
|
||
intro porq
|
||
cases porq with
|
||
| inl p => exact (And.left npandnq) p
|
||
| inr q => exact (And.right npandnq) q
|
||
|
||
example : ¬p ∨ ¬q → ¬(p ∧ q) := by
|
||
intro npornq
|
||
cases npornq with
|
||
| inl np => intro pandq; exact np (And.left pandq)
|
||
| inr nq => intro pandq; exact nq (And.right pandq)
|
||
|
||
example : ¬(p ∧ ¬p) := by
|
||
intro pandnp
|
||
exact (And.right pandnp) (And.left pandnp)
|
||
|
||
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 := by
|
||
apply Iff.intro
|
||
· intro porf
|
||
apply Or.elim porf id False.elim
|
||
· intro p
|
||
apply Or.inl p
|
||
|
||
|
||
example : p ∧ False ↔ False := by
|
||
apply Iff.intro
|
||
· intro ⟨p,f⟩
|
||
exact f
|
||
· intro f
|
||
apply False.elim f
|
||
|
||
|
||
example : (p → q) → (¬q → ¬p) :=
|
||
λ ptoq nq p => absurd (ptoq p) nq
|