WIP

prop_as_types.lean

@@ -96,3 +96,126 @@ example (hp : p) (hnp : ¬p) : q := absurd hp hnp
 example (hnp : ¬p) (hq : q) (hqp : q → p) : r :=
   absurd (hqp hq) hnp
 
+-- Logical Equivalence
+theorem and_swap : p ∧ q ↔ q ∧ p :=
+  Iff.intro
+    (fun h : p ∧ q =>
+     show q ∧ p from And.intro h.right h.left)
+    (fun h : q ∧ p =>
+     show p ∧ q from ⟨h.right, h.left⟩)
+
+example : p ∧ q ↔ q ∧ p :=
+  ⟨fun h => ⟨h.right, h.left⟩, fun h => ⟨h.right, h.left⟩⟩
+
+#check and_swap p q
+#check and_swap q p
+
+variable (h : p ∧ q)
+example : q ∧ p := (and_swap p q).mp h
+
+-- Introducing Auxiliary Subgoals
+example (h : p ∧ q) : q ∧ p :=
+  have hp : p := h.left
+  have hq : q := h.right
+  show q ∧ p from And.intro hq hp
+
+example (h : p ∧ q) : q ∧ p :=
+  have hp : p := h.left
+  suffices hq : q from And.intro hq hp
+  show q from And.right h
+
+-- Classical Logic
+open Classical in
+#check em p
+
+open Classical in
+theorem dne {p : Prop} (h : ¬¬p) : p :=
+  Or.elim (em p)
+    (fun hp : p => hp)
+    (fun hnp : ¬p => absurd hnp h)
+
+open Classical in
+example (h : ¬¬p) : p :=
+  byCases
+    (fun h1 : p => h1)
+    (fun h2 : ¬p => absurd h2 h)
+
+open Classical in
+example (h : ¬¬p) : p :=
+  byContradiction
+    (fun h1 : ¬p =>
+     show False from h h1)
+
+open Classical in
+example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
+  Or.elim (em p)
+    (fun hp : p =>
+     Or.inr
+       (show ¬q from
+         fun hq : q =>
+         h ⟨hp, hq⟩))
+    (fun hp : ¬p =>
+     Or.inl hp)
+
+-- Exercises
+-- ∧ と ∨ の可換性
+example : p ∧ q ↔ q ∧ p :=
+  Iff.intro
+    (fun h : p ∧ q =>
+      ⟨h.right, h.left⟩)
+    (fun h : q ∧ p =>
+      ⟨h.right, h.left⟩)
+example : p ∨ q ↔ q ∨ p :=
+  Iff.intro
+    (fun h : p ∨ q =>
+      h.elim
+        (fun h : p => Or.inr h)
+        (fun h : q => Or.inl h))
+    (fun h : q ∨ p =>
+      h.elim
+        (fun h : q => Or.inr h)
+        (fun h : p => Or.inl h))
+
+-- ∧ と ∨ の結合性
+example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
+  have h1 : (p ∧ q) ∧ r → p ∧ (q ∧ r) :=
+    (fun h =>
+      ⟨h.left.left, ⟨h.left.right, h.right⟩⟩)
+  have h2 : p ∧ (q ∧ r) → (p ∧ q) ∧ r :=
+    (fun h =>
+      ⟨⟨h.left, h.right.left⟩, h.right.right⟩)
+  ⟨h1, h2⟩
+example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
+  have h1 : (p ∨ q) ∨ r → p ∨ (q ∨ r) :=
+    (fun h =>
+      h.elim
+        (fun hpq =>
+          hpq.elim
+            (fun hp => Or.inl hp)
+            (fun hq => Or.inr (Or.inl hq)))
+        (fun hr => Or.inr (Or.inr hr)))
+  have h2 : p ∨ (q ∨ r) → (p ∨ q) ∨ r :=
+    (fun h =>
+      h.elim
+        sorry
+        sorry)
+  Iff.intro h1 h2
+example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
+  sorry
+
+-- 分配性
+example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
+example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry
+
+-- 他の性質
+example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
+example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
+example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
+example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
+example : ¬(p ∧ ¬p) := sorry
+example : p ∧ ¬q → ¬(p → q) := sorry
+example : ¬p → (p → q) := sorry
+example : (¬p ∨ q) → (p → q) := sorry
+example : p ∨ False ↔ p := sorry
+example : p ∧ False ↔ False := sorry
+example : (p → q) → (¬q → ¬p) := sorry