first little proofs

Index.md

@@ -0,0 +1,9 @@
+### Basic logic
+
+| Name | Mathlib equivalent | Proposition |
+|---------------|--------------------|-------------|
+|`basicLogic.and_commutative` | `and_comm` | $$a\land b \iff b \land a$$ |
+|`basicLogic.or_commutative` | `or_comm` | $$a\lor b \iff b \lor a$$ |
+|`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)$$|

README.md

@@ -17,3 +17,5 @@ Lean4 is much more complex than what I thought. Not only I need to learn a new s
 I also watch a [video](https://www.youtube.com/watch?v=0QZI_m8WZ0Q) and followed step by step. I've learned better than in my few hours of reading _Theorem Proving in Lean 4_ (I switched to the video after not entierly understanding the fifth paragraph of the subchapter "What makes dependent type theory dependent" of the second chapter of the book.
 
 I am bit bored by copying examples and following books. I'm gonna try the same methode I used to learn C and Python. Set myself goals (in this case small basic proofs) and when I don't know or don't understand it google it (I won't use a LLM not because I'm against it, but because I don't want to become reliant on it).
+
+I tried and got successfully a few basic logic results I'm gonna try to organize them into Index.md.

ZeroToLean/LearningLean/Basic.lean

@@ -1 +1,68 @@
-def hello := "world"
+-- 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
+
+namespace basicLogic
+variable {P: Prop}
+variable {Q: Prop}
+variable {R: Prop}
+
+
+theorem p_and_q_implie_p
+  : P ∧ Q → P := by
+    intro hp
+    cases hp with
+    | intro hP =>
+      exact hP
+end 
+
+theorem p_implies_p_or_q
+  : P → P ∨ Q := by
+    intro hp
+    exact Or.inl hp 
+theorem and_commutative
+  : P ∧ Q → Q ∧ P := by
+  intro hpq
+  cases hpq with
+  | intro hp hq =>
+    exact ⟨hq,hp⟩
+
+theorem or_commutative
+  : P ∨ Q → Q ∨ P := by
+    intro p_or_q
+    cases p_or_q with
+    | inl hp  =>
+      exact Or.inr hp
+    | inr hq =>
+      exact Or.inl hq
+
+theorem p_imples_q_and_q_implies_r_Implies_p_implies_r
+  : (P→Q) ∧ (Q→R) → (P→R) := by
+    intro mainHypothesis
+    cases mainHypothesis with
+    | intro p_implies_q q_implies_r =>
+      intro hp
+      exact q_implies_r (p_implies_q hp)
+
+theorem double_negation
+  : P → ¬¬P := by
+    intro hp
+    intro hnotp
+    exact hnotp hp
+
+theorem and_associative
+  : P ∧ (Q ∧ R) → (P ∧ Q) ∧ R := by
+    intro h
+    cases h with
+    | intro p q_and_r =>
+      cases q_and_r with
+      | intro q r =>
+        exact ⟨ ⟨p,q⟩,r⟩
+
+theorem contrapositive
+  : (P → Q) → (¬Q → ¬P) := by
+    intro p_implies_q
+    intro not_q
+    intro p
+    exact not_q (p_implies_q p)
+end basicLogic