proposition and proofs

prop_as_types.lean

@@ -237,10 +237,59 @@ example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
   Iff.intro h1 h2
 
 -- 他の性質
-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 → (q → r)) ↔ (p ∧ q → r) :=
+  have h1 : (p → q → r) → p ∧ q → r :=
+    (fun h =>
+      fun hpq =>
+        (h hpq.left) hpq.right)
+  have h2 : (p ∧ q → r) → p → q → r :=
+    (fun h =>
+      fun hp =>
+        fun hq =>
+          h ⟨hp, hq⟩)
+  Iff.intro h1 h2
+example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
+  have h1 : (p ∨ q → r) → (p → r) ∧ (q → r) :=
+    fun h =>
+      have hpr :=
+        (fun hp =>
+          h (Or.inl hp))
+      have hqr :=
+        (fun hq =>
+          h (Or.inr hq))
+      And.intro hpr hqr
+  have h2 : (p → r) ∧ (q → r) → p ∨ q → r :=
+    fun h =>
+      fun h' : p ∨ q =>
+        h'.elim
+          (fun hp => h.left hp)
+          (fun hq => h.right hq)
+  Iff.intro h1 h2
+example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
+  have h1 : ¬(p ∨ q) → ¬p ∧ ¬q :=
+    fun h =>
+      have hnp : ¬p :=
+        fun hp =>
+          show False from h (Or.inl hp)
+      have hnq : ¬q :=
+        fun hq =>
+          show False from h (Or.inr hq)
+      And.intro hnp hnq
+  have h2 : ¬p ∧ ¬q → ¬(p ∨ q) := 
+    fun h =>
+      fun hpq : p ∨ q =>
+        show False from
+          hpq.elim
+            (fun hp => h.left hp)
+            (fun hq => h.right hq)
+  Iff.intro h1 h2
+example : ¬p ∨ ¬q → ¬(p ∧ q) :=
+  fun h =>
+    h.elim
+      (fun hnp =>
+        fun hpq =>
+          show False from hnp (hpq.left))
+      (fun hnq => sorry)
 example : ¬(p ∧ ¬p) := sorry
 example : p ∧ ¬q → ¬(p → q) := sorry
 example : ¬p → (p → q) := sorry
@@ -248,3 +297,32 @@ example : (¬p ∨ q) → (p → q) := sorry
 example : p ∨ False ↔ p := sorry
 example : p ∧ False ↔ False := sorry
 example : (p → q) → (¬q → ¬p) := sorry
+
+open Classical in
+example : (p → q ∨ r) → ((p → q) ∨ (p → r)) :=
+  fun h =>
+    (em q).elim
+      (fun hq =>
+        Or.inl (fun hp => hq))
+      (fun hnq =>
+        have h1 : p → r :=
+          fun hp : p =>
+            (h hp).elim
+              (fun hq =>
+                absurd hq hnq)
+              (fun hr => hr)
+        Or.inr h1)
+open Classical in
+example : ¬(p ∧ q) → ¬p ∨ ¬q :=
+  fun hnpq =>
+    sorry
+open Classical in
+example : ¬(p → q) → p ∧ ¬q := sorry
+open Classical in
+example : (p → q) → (¬p ∨ q) := sorry
+open Classical in
+example : (¬q → ¬p) → (p → q) := sorry
+open Classical in
+example : p ∨ ¬p := sorry
+open Classical in
+example : (((p → q) → p) → p) := sorry