pingu/lean
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Even more clean

Browse Source
This commit is contained in:
pingu
2025-01-30 19:13:33 +01:00
parent b5497fbe3e
commit e9a3863eaf
1 changed files with 32 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files

73
Example.lean
View File

@ -2,73 +2,64 @@ variable (p q r : Prop)
-- commutativity of ∧ and ∨ -- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := example : p ∧ q ↔ q ∧ p :=
Iff.intro (λ ⟨p,q⟩ => ⟨q,p⟩) (λ ⟨q,p⟩ => ⟨p,q⟩) ⟨λ ⟨p,q⟩ => ⟨q,p⟩, λ ⟨q,p⟩ => ⟨p,q⟩⟩
example : p ∨ q ↔ q ∨ p := example : p ∨ q ↔ q ∨ p :=
Iff.intro ⟨λ
(λ | Or.inl p => Or.inr p
| Or.inl p => Or.inr p | Or.inr q => Or.inl q,
| Or.inr q => Or.inl q) λ
(λ | Or.inl q => Or.inr q
| Or.inl q => Or.inr q | Or.inr p => Or.inl p⟩
| Or.inr p => Or.inl p)
-- associativity of ∧ and ∨ -- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
Iff.intro ⟨λ ⟨⟨p,q⟩,r⟩ => ⟨p,⟨q,r⟩⟩, λ ⟨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) := example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
Iff.intro ⟨λ
(λ
| Or.inr r => Or.inr (Or.inr r) | Or.inr r => Or.inr (Or.inr r)
| Or.inl (Or.inr q) => Or.inr (Or.inl q) | Or.inl (Or.inr q) => Or.inr (Or.inl q)
| Or.inl (Or.inl p) => Or.inl p) | Or.inl (Or.inl p) => Or.inl p,
(λ λ
| Or.inl p => Or.inl (Or.inl p) | Or.inl p => Or.inl (Or.inl p)
| Or.inr (Or.inl q) => Or.inl (Or.inr q) | Or.inr (Or.inl q) => Or.inl (Or.inr q)
| Or.inr (Or.inr r) => Or.inr r) | Or.inr (Or.inr r) => Or.inr r⟩
-- distributivity -- distributivity
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
Iff.intro ⟨λ
(λ
| ⟨p, Or.inl q⟩ => Or.inl ⟨p,q⟩ | ⟨p, Or.inl q⟩ => Or.inl ⟨p,q⟩
| ⟨p, Or.inr r⟩ => Or.inr ⟨p,r⟩) | ⟨p, Or.inr r⟩ => Or.inr ⟨p,r⟩,
(λ λ
| Or.inl ⟨p,q⟩ => ⟨p,Or.inl q⟩ | Or.inl ⟨p,q⟩ => ⟨p,Or.inl q⟩
| Or.inr ⟨p,r⟩ => ⟨p,Or.inr r⟩) | Or.inr ⟨p,r⟩ => ⟨p,Or.inr r⟩⟩
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
Iff.intro ⟨λ
(λ
| Or.inl p => ⟨Or.inl p, Or.inl p⟩ | Or.inl p => ⟨Or.inl p, Or.inl p⟩
| Or.inr ⟨q,r⟩ => ⟨Or.inr q, Or.inr r⟩) | Or.inr ⟨q,r⟩ => ⟨Or.inr q, Or.inr r⟩,
(λ λ
| ⟨Or.inr q, Or.inr r⟩ => Or.inr ⟨q,r⟩ | ⟨Or.inr q, Or.inr r⟩ => Or.inr ⟨q,r⟩
| ⟨Or.inl p, _⟩ => Or.inl p | ⟨Or.inl p, _⟩ => Or.inl p
| ⟨ _, Or.inl p⟩ => Or.inl p) | ⟨ _, Or.inl p⟩ => Or.inl p⟩
-- other properties -- other properties
example : (p → (q → r)) ↔ (p ∧ q → r) := example : (p → (q → r)) ↔ (p ∧ q → r) :=
Iff.intro ⟨λ f ⟨p,q⟩ => f p q,λ f p q => f ⟨p,q⟩⟩
(λ f ⟨p,q⟩ => f p q)
(λ f p q => f ⟨p,q⟩)
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
Iff.intro ⟨
(λ porqtor => And.intro (λ p => porqtor (Or.inl p)) (λ q => porqtor (Or.inr q))) λ f => ⟨λ p => f (Or.inl p), λ q => f (Or.inr q)⟩,
(λ λ
|⟨f, _⟩, Or.inl p => f p |⟨f, _⟩, Or.inl p => f p
|⟨_, g⟩, Or.inr q => g q) |⟨_, g⟩, Or.inr q => g q⟩
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
Iff.intro ⟨λ f => ⟨λ p => f (Or.inl p), λ q => f (Or.inr q)⟩,
(λ nporq => And.intro (λ p => nporq (Or.inl p)) (λ q => nporq (Or.inr q))) λ
(λ | ⟨np, _⟩, Or.inl p => np p
| ⟨np, _⟩, Or.inl p => np p | ⟨_ ,nq⟩, Or.inr q => nq q⟩
| ⟨_ ,nq⟩, Or.inr q => nq q)
example : ¬p ∨ ¬q → ¬(p ∧ q) example : ¬p ∨ ¬q → ¬(p ∧ q)
| Or.inl np, ⟨p,_⟩ => np p | Or.inl np, ⟨p,_⟩ => np p
@ -88,10 +79,10 @@ example : (¬p ∨ q) → (p → q)
| (Or.inr q), _ => q | (Or.inr q), _ => q
example : p ∨ False ↔ p := example : p ∨ False ↔ p :=
Iff.intro (λ porf => Or.elim porf id False.elim) (λ p => Or.inl p) ⟨λ h => Or.elim h id False.elim, λ p => Or.inl p⟩
example : p ∧ False ↔ False := example : p ∧ False ↔ False :=
Iff.intro (λ ⟨_,f⟩ => f) (λ f => False.elim f) ⟨λ ⟨_,f⟩ => f, λ f => False.elim f⟩
example : (p → q) → (¬q → ¬p) := example : (p → q) → (¬q → ¬p) :=
λ ptoq nq p => absurd (ptoq p) nq λ f nq p => absurd (f p) nq