update progress 02.08.2026

Index.md

@@ -7,13 +7,24 @@
 |`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$$|
+|`basicLogic.p_or_p_equal_p` | `or_self` | $$(a \lor a) = a$$ |
+|`basicLogic.p_or_p_iff_p` | | $$a \lor a \iff a$$ |
+|`basicLogic.and_or_distributivity_left` | `and_or_left` | $$a \land (b \lor c) \iff (a \land b) \lor (a \land c)$$ |
+|`basicLogic.and_or_distributivity_right` | `and_or_right` | $$(a \land b) \lor c \iff (a \lor c) \land (b \lor c)$$ |
+|`basicLogic.p_and_true_equal_p` | `and_true` | $$(a \land True) = a$$ |
+|`basicLogic.p_and_true_iff_p` | | $$a \land True \iff a$$ |
+|`basicLogic.true_and_p_equal_p` | `true_and` | $$(True \land a) = a$$ |
+|`basicLogic.true_and_p_iff_p` | | $$True \land a \iff a$$ |
+|`basicLogic.p_or_false_equal_p` | `or_false` | $$(a \lor False) = a$$ |
+|`basicLogic.p_or_false_iff_p` | | $$a \lor False \iff a$$ |
+|`basicLogic.false_or_p_equal_p` | `false_or` | $$(False \lor a) = a$$ |
+|`basicLogic.false_or_p_iff_p` | | $$False \lor a \iff a$$ |
+|`basicLogic.and_false_equal_false` | `and_false` | $$(a \land False) = False$$ |
+|`basicLogic.and_false_iff_false` | | $$a \land False \iff False$$ |
+|`basicLogic.false_and_equal_false` | `false_and` | $$(False \land a) = False$$ |
+|`basicLogic.false_and_iff_false` | | $$False \land a \iff False$$ |
+|`basicLogic.or_true_equal_true` | `or_true` | $$(a \lor True) = True$$ |
+|`basicLogic.or_true_iff_true` | | $$a \lor True \iff True$$ |
+|`basicLogic.true_or_equal_true` | `true_or` | $$(True \lor a) = True$$ |
+|`basicLogic.true_or_iff_true` | | $$True \lor a \iff True$$ |
+

ZeroToLean/LearningLean/Basic.lean

@@ -195,10 +195,81 @@ theorem p_or_false_equal_p
     exact propext p_or_false_iff_p
 
 #check false_or
+theorem false_or_p_iff_p
+  : False ∨ P ↔ P := by
+    constructor
+    · intro false_or_p
+      cases false_or_p with
+      | inl f =>
+        exact False.elim f
+      | inr p =>
+        exact p
+    · intro p
+      exact Or.inr p
+theorem false_or_p_equal_p
+  : (False ∨ P) = P := by
+  exact propext false_or_p_iff_p
+
 #check and_false
+theorem and_false_iff_false
+  : P ∧ False ↔ False := by
+  constructor
+  · intro p_and_false
+    cases p_and_false with
+    | intro p f =>
+    exact f
+  · intro f
+    exact False.elim f
+theorem and_false_equal_false
+  : (P ∧ False) = False := by
+  exact propext and_false_iff_false
+
 #check false_and
+theorem false_and_iff_false
+  : False ∧ P ↔ False := by
+  constructor
+  · intro false_and_p
+    cases false_and_p with
+    | intro f p =>
+    exact f
+  · intro f
+    exact False.elim f
+theorem false_and_equal_false
+  : (False ∧ P) = False := by
+  exact propext false_and_iff_false
+
 #check or_true
+theorem or_true_iff_true
+  : P ∨ True ↔ True := by
+  constructor
+  · intro p_or_true
+    cases p_or_true with
+    | inr t =>
+      exact t
+    | inl p =>
+      trivial
+  · intro t
+    exact Or.inr t
+theorem or_true_equal_true
+  : (P ∨ True) = True := by
+  exact propext or_true_iff_true
+
 #check true_or
+theorem true_or_iff_true
+  : True ∨ P ↔ True := by
+  constructor
+  · intro true_or_p
+    cases true_or_p with
+    | inl t =>
+      exact t
+    | inr p =>
+      trivial
+  · intro t
+    exact Or.inl t
+theorem true_or_equal_true
+  : (True ∨ P) = True := by
+  exact propext true_or_iff_true
+
 #check not_or
 #check not_and_or