From 3eb2bdcf127f8c2dbe36a5a6dbcf5f45c0e2fb21 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Sat, 20 Apr 2024 20:41:17 +0900
Subject: [PATCH] (WIP) exercise

---
 prop_as_types.lean | 41 +++++++++++++++++++++++++++++++++++------
 1 file changed, 35 insertions(+), 6 deletions(-)

diff --git a/prop_as_types.lean b/prop_as_types.lean
index 1cb566b..620f001 100644
--- a/prop_as_types.lean
+++ b/prop_as_types.lean
@@ -197,15 +197,44 @@ example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
   have h2 : p ∨ (q ∨ r) → (p ∨ q) ∨ r :=
     (fun h =>
       h.elim
-        sorry
-        sorry)
+        (fun hp =>
+          Or.inl (Or.inl hp))
+        (fun hqr =>
+          hqr.elim
+            (fun hq => Or.inl (Or.inr hq))
+            (fun hr => Or.inr hr)))
   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) ∨ (p ∧ r) :=
+  have h1 : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) :=
+    (fun h =>
+      h.right.elim
+        (fun hq => Or.inl (And.intro h.left hq))
+        (fun hr => Or.inr (And.intro h.left hr)))
+  have h2 : (p ∧ q) ∨ (p ∧ r) → p ∧ (q ∨ r) :=
+    (fun h =>
+      h.elim
+        (fun hpq => And.intro hpq.left (Or.inl hpq.right))
+        (fun hpr => And.intro hpr.left (Or.inr hpr.right)))
+  Iff.intro h1 h2
+example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
+  have h1 :=
+    (fun h =>
+      h.elim
+        (fun h => ⟨Or.inl h, Or.inl h⟩)
+        (fun h => ⟨Or.inr h.left, Or.inr h.right⟩))
+  have h2 :=
+    (fun h =>
+      have h2l : p ∨ q := h.left
+      have h2r : p ∨ r := h.right
+      h2l.elim
+        (fun hp => Or.inl hp)
+        (fun hq =>
+          h2r.elim
+            (fun hp => Or.inl hp)
+            (fun hr => Or.inr (And.intro hq hr))))
+  Iff.intro h1 h2
 
 -- 他の性質
 example : (p → (q → r)) ↔ (p ∧ q → r) := sorry