more basicLogic

Index.md

@@ -7,3 +7,13 @@
 |`basicLogic.double_negation` | `not_not_intro`| $$a\to\neg\neg a$$ |
 |`basicLogic.and_associative` | `and_assoc`| $$a\land (b\land c) \iff (a\land b) \land c$$|
 |`basicLogic.contrapositive` | `contrapose` | $$(a \to b) \to (\neg b \to \neg a)$$|
+|`basicLogic.p_or_p_equal_p` | `or_self` | $$(a \or a) = a$$|
+|`basicLogic.p_or_p_iff_p` | | $$a \or a \iff a$$|
+|`basicLogic.and_or_distributivity_left` | `and_or_left` | $$a \and (b \or c) \iff a \and b \or a \and c$$|
+|`basicLogic.and_or_distributivity_right` | `and_or_right` | $$a \and b \or c \iff (a \or c) \and (b \or c)$$ |
+|`basicLogic.p_and_true_equal_p` | `and_true` | $$(a \and True) = a$$|
+|`basicLogic.p_and_true_iff_p` | | $$a \and True \iff a$$|
+|`basicLogic.true_and_p_equal_p` | `true_and` | $$(True \and a) = a$$|
+|`basicLogic.true_and_p_iff_p` | | $$True \and a \iff a$$|
+|`basicLogic.p_or_false_equal_p` | `or_false` | $$(a \or False) = a$$|
+|`basicLogic.p_or_false_iff_p` | | $$a \or False \iff a$$|

ZeroToLean/LearningLean/Basic.lean

@@ -1,6 +1,6 @@
 -- see note of 2026-07-30 im trying to prove trivial things. Note I did ask ChatGPT for a list of things to prove.
 
--- note we should really get both sides implication (↔)for a lot of them
+import Mathlib
 
 namespace basicLogic
 variable {P: Prop}
@@ -14,7 +14,6 @@ theorem p_and_q_implie_p
     cases hp with
     | intro hP =>
       exact hP
-end 
 
 theorem p_implies_p_or_q
   : P → P ∨ Q := by
@@ -32,6 +31,7 @@ theorem and_commutative
     | intro hq hp =>
       exact ⟨hp,hq⟩
 
+#check or_comm
 theorem or_commutative
   : P ∨ Q ↔ Q ∨ P := by
     constructor
@@ -56,12 +56,14 @@ theorem p_imples_q_and_q_implies_r_Implies_p_implies_r
       intro hp
       exact q_implies_r (p_implies_q hp)
 
+#check not_not_intro
 theorem double_negation
   : P → ¬¬P := by
     intro hp
     intro hnotp
     exact hnotp hp
 
+#check and_comm
 theorem and_associative
   : P ∧ (Q ∧ R) ↔ (P ∧ Q) ∧ R := by
     constructor
@@ -84,4 +86,120 @@ theorem contrapositive
     intro not_q
     intro p
     exact not_q (p_implies_q p)
+
+#check or_self
+theorem p_or_p_iff_p
+  : P ∨ P ↔ P := by
+  constructor
+  · intro p_or_p
+    cases p_or_p with
+    | inr p =>
+      exact p
+    | inl p =>
+      exact p
+  · intro p
+    exact Or.inl p
+theorem p_or_p_equal_p
+  : (P ∨ P) = P := by
+    exact propext p_or_p_iff_p
+
+#check and_or_left
+theorem and_or_distributivity_left
+  : P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R := by
+  constructor
+  · intro p_and_q_or_r
+    cases p_and_q_or_r with
+    | intro p q_or_r =>
+      cases q_or_r with
+      | inl q =>
+        exact Or.inl ⟨p, q⟩
+      | inr r =>
+        exact Or.inr ⟨p, r⟩
+  · intro p_and_q_or_p_and_r
+    cases p_and_q_or_p_and_r with
+    | inl p_and_q =>
+      cases p_and_q with
+      | intro p q =>
+        exact ⟨p, Or.inl q⟩
+    | inr p_and_r =>
+      cases p_and_r with
+      | intro p r =>
+        exact ⟨p, Or.inr r⟩
+
+#check and_or_right
+theorem and_or_distributivity_right
+  : P ∧ Q ∨ R ↔ (P ∨ R) ∧ (Q ∨ R) := by
+    constructor
+    · intro p_and_q_or_r
+      cases p_and_q_or_r with
+      | inl p_and_q =>
+        cases p_and_q with
+        | intro p q =>
+          exact ⟨Or.inl p, Or.inl q⟩
+      | inr r =>
+        exact ⟨Or.inr r, Or.inr r⟩
+    · intro p_or_r_and_q_or_r
+      cases p_or_r_and_q_or_r with
+      | intro p_or_r q_or_r =>
+        cases p_or_r with
+        | inl p =>
+          cases q_or_r with
+          | inl q =>
+            exact Or.inl ⟨p, q⟩
+          | inr r =>
+            exact Or.inr r
+        | inr r =>
+          exact Or.inr r
+
+#check and_true
+theorem p_and_true_iff_p
+  : p ∧ True ↔ p := by
+    constructor
+    · intro p_and_true
+      cases p_and_true with
+      | intro p true =>
+        exact p
+    · intro p
+      exact ⟨p, True.intro⟩
+theorem p_and_true_equal_true
+  : (p ∧ True) = p := by
+    exact propext p_and_true_iff_p
+#check true_and
+theorem true_and_p_iff_p
+  : True ∧ p ↔ p := by
+    constructor
+    · intro true_and_p
+      cases true_and_p with
+      | intro t p =>
+        exact p
+    · intro p
+      exact ⟨True.intro, p⟩
+theorem true_and_p_equal_p
+  : (True ∧ p) = p := by
+    exact propext true_and_p_iff_p
+
+#check or_false
+theorem p_or_false_iff_p
+  : P ∨ False ↔ P := by
+  constructor
+  · intro p_or_false
+    cases p_or_false with
+    | inl p =>
+      exact p
+    | inr f =>
+      exact False.elim f
+  · intro p
+    exact Or.inl p
+theorem p_or_false_equal_p
+  : (P ∨ False) = P := by
+    exact propext p_or_false_iff_p
+
+#check false_or
+#check and_false
+#check false_and
+#check or_true
+#check true_or
+#check not_or
+#check not_and_or
+
 end basicLogic