From 9a5863343d2cf4a3b1f582ffcf209cc8bfa0e9f2 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Wed, 8 Jan 2025 01:27:21 +0900
Subject: [PATCH] till more exercises

---
 basics/main.lean | 115 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 mode change 100644 => 100755 basics/main.lean

diff --git a/basics/main.lean b/basics/main.lean
old mode 100644
new mode 100755
index 1ebfa67..b0db83a
--- a/basics/main.lean
+++ b/basics/main.lean
@@ -235,3 +235,118 @@ end Exercise1
 
 --- Proof by Simplification
 
+theorem plus_0_n : ∀ n : Nat, 0 + n = n := by
+  intros n
+  simp
+
+#check ∀ n : Nat, 0 + n = n
+
+example : ∀ n : Nat, 1 + n = .succ n := by
+  intros m
+  simp
+  apply Nat.add_comm 1 m
+
+example : ∀ n : Nat, 0 * n = 0 := by
+  intros n
+  exact Nat.zero_mul n
+
+--- Proof by Rewriting
+example : ∀ n m : Nat, n = m → n + n = m + m := by
+  intros n m h
+  rw [h]
+
+namespace Exercise1
+
+theorem plus_id_exercise : ∀ n m o : Nat, n = m → m = o → n + m = m + o := by
+  intros n m o h₁ h₂
+  rw [h₁]
+  rw [h₂]
+
+#check plus_0_n
+
+theorem mult_n_1 : ∀ p : Nat, p * 1 = p := by
+  intros p
+  cases p
+  . rw [Nat.mul_one]
+  . rw [Nat.mul_one]
+
+example : ∀ p : Nat, p * 1 = p := by
+  intros p
+  rw [Nat.mul_one]
+
+#check Nat.mul_zero
+#check Nat.mul_succ
+example : ∀ p : Nat, p * 1 = p := by
+  intros
+  rw [Nat.mul_succ]
+  rw [Nat.mul_zero]
+  simp
+
+end Exercise1
+
+#eval (1).succ.succ.succ
+#eval [1, 2, 3, 4].foldl (· + ·) 0
+#print Array.foldl
+#print optParam
+
+--- Proof by Case Analysis
+example : ∀ n : Nat, ((n + 1) = 0) = False := by
+  intros n
+  cases n
+  case zero => simp only [Nat.zero_add, Nat.add_one_ne_zero]
+  case succ => simp only [Nat.add_one_ne_zero]
+
+example : ∀ b : Bool, ¬ (¬ b) = b := by
+  intros b
+  cases b
+  . simp
+  . rw [Lean.Grind.not_eq_prop]
+
+example : ∀ b c : Bool, (b ∧ c) = (c ∧ b) := by
+  intros b c
+  cases b
+  . cases c
+    . simp only [Bool.false_eq_true, and_self]
+    . rw [@and_comm]
+  . rw [@and_comm]
+
+#eval true ∧ true
+#eval (true ∧ true) = (true ∧ true)
+#eval true ∧ false = false ∧ true
+#eval false ∧ false = false ∧ false
+#eval (false ∧ false) = (false ∧ false)
+#eval Bool.and true true
+#eval Bool.true ∧ Bool.true
+#eval true && false = false && true
+#print and_comm
+
+namespace Exercise
+
+example : ∀ b c : Bool, (Bool.and b c = true) → (c = true) := by
+  intros b c
+  cases c
+  case true => exact fun _a => rfl
+  case false =>
+    cases b
+    case true =>
+      intros h
+      exact h
+    case false =>
+      intros h
+      exact h
+
+#print id
+#check Function.const
+
+example : ∀ n : Nat, (0 == (n + 1)) = false := by
+  intros n
+  cases n
+  . simp only [Nat.zero_add, Nat.reduceBEq]
+  . simp only [Nat.reduceBeqDiff]
+
+end Exercise
+
+--- More on Notation
+-- skipping
+
+--- More Exercises