91 lines
2.3 KiB
Plaintext
91 lines
2.3 KiB
Plaintext
open Or
|
||
open False renaming elim → negelim
|
||
variable (p q r : Prop)
|
||
|
||
-- commutativity of ∧ and ∨
|
||
example : p ∧ q ↔ q ∧ p :=
|
||
⟨λ ⟨p,q⟩ => ⟨q,p⟩, λ ⟨q,p⟩ => ⟨p,q⟩⟩
|
||
|
||
example : p ∨ q ↔ q ∨ p :=
|
||
⟨λ
|
||
| inl p => inr p
|
||
| inr q => inl q,
|
||
λ
|
||
| inl q => inr q
|
||
| inr p => inl p⟩
|
||
|
||
-- associativity of ∧ and ∨
|
||
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
|
||
⟨λ ⟨⟨p,q⟩,r⟩ => ⟨p,⟨q,r⟩⟩, λ ⟨p,⟨q,r⟩⟩ => ⟨⟨p,q⟩,r⟩⟩
|
||
|
||
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
|
||
⟨λ
|
||
| inr r => inr (inr r)
|
||
| inl (inr q) => inr (inl q)
|
||
| inl (inl p) => inl p,
|
||
λ
|
||
| inl p => inl (inl p)
|
||
| inr (inl q) => inl (inr q)
|
||
| inr (inr r) => inr r⟩
|
||
|
||
-- distributivity
|
||
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
|
||
⟨λ
|
||
| ⟨p, inl q⟩ => inl ⟨p,q⟩
|
||
| ⟨p, inr r⟩ => inr ⟨p,r⟩,
|
||
λ
|
||
| inl ⟨p,q⟩ => ⟨p,inl q⟩
|
||
| inr ⟨p,r⟩ => ⟨p,inr r⟩⟩
|
||
|
||
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
|
||
⟨λ
|
||
| inl p => ⟨inl p, inl p⟩
|
||
| inr ⟨q,r⟩ => ⟨inr q, inr r⟩,
|
||
λ
|
||
| ⟨inr q, inr r⟩ => inr ⟨q,r⟩
|
||
| ⟨inl p, _⟩ => inl p
|
||
| ⟨ _, inl p⟩ => inl p⟩
|
||
|
||
-- other properties
|
||
example : (p → (q → r)) ↔ (p ∧ q → r) :=
|
||
⟨λ f ⟨p,q⟩ => f p q,λ f p q => f ⟨p,q⟩⟩
|
||
|
||
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
||
⟨
|
||
λ f => ⟨λ p => f (inl p), λ q => f (inr q)⟩,
|
||
λ
|
||
|⟨f, _⟩, inl p => f p
|
||
|⟨_, g⟩, inr q => g q⟩
|
||
|
||
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
|
||
⟨λ f => ⟨λ p => f (inl p), λ q => f (inr q)⟩,
|
||
λ
|
||
| ⟨np, _⟩, inl p => np p
|
||
| ⟨_ ,nq⟩, inr q => nq q⟩
|
||
|
||
example : ¬p ∨ ¬q → ¬(p ∧ q)
|
||
| inl np, ⟨p,_⟩ => np p
|
||
| 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)
|
||
| (inl np), p => absurd p np
|
||
| (inr q), _ => q
|
||
|
||
example : p ∨ False ↔ p :=
|
||
⟨λ h => elim h id negelim, λ p => inl p⟩
|
||
|
||
example : p ∧ False ↔ False :=
|
||
⟨λ ⟨_,f⟩ => f, λ f => negelim f⟩
|
||
|
||
example : (p → q) → (¬q → ¬p) :=
|
||
λ f nq p => absurd (f p) nq
|