From 96ec872f49b0ecb0d1ba56090cebc0d43a3b7c5f Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 24 Jan 2023 14:54:36 +0100
Subject: [PATCH] levels.

---
 .../testgame/TestGame/Levels/Induction.lean   |  6 ++-
 .../TestGame/Levels/Induction/L01_Simp.lean   | 44 +++++++++++++++++++
 .../TestGame/Levels/Induction/L02_Sum.lean    | 31 +++++++++++++
 .../Levels/Induction/L03_Induction.lean       | 44 +++++++++++++++++++
 .../TestGame/Levels/Induction/L04_SumOdd.lean | 31 +++++++++++++
 ...{L32_Induction.lean => L10_Bernoulli.lean} | 21 ++++++---
 .../TestGame/Levels/Induction/L31_Sum.lean    | 25 -----------
 server/testgame/TestGame/ToBePorted.lean      |  2 +
 8 files changed, 171 insertions(+), 33 deletions(-)
 create mode 100644 server/testgame/TestGame/Levels/Induction/L01_Simp.lean
 create mode 100644 server/testgame/TestGame/Levels/Induction/L02_Sum.lean
 create mode 100644 server/testgame/TestGame/Levels/Induction/L03_Induction.lean
 create mode 100644 server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
 rename server/testgame/TestGame/Levels/Induction/{L32_Induction.lean => L10_Bernoulli.lean} (59%)
 delete mode 100644 server/testgame/TestGame/Levels/Induction/L31_Sum.lean

diff --git a/server/testgame/TestGame/Levels/Induction.lean b/server/testgame/TestGame/Levels/Induction.lean
index 1c320f2..88d12a3 100644
--- a/server/testgame/TestGame/Levels/Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction.lean
@@ -1,2 +1,4 @@
-import TestGame.Levels.Induction.L31_Sum
-import TestGame.Levels.Induction.L32_Induction
+import TestGame.Levels.Induction.L01_Simp
+import TestGame.Levels.Induction.L02_Sum
+import TestGame.Levels.Induction.L03_Induction
+import TestGame.Levels.Induction.L04_SumOdd
diff --git a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
new file mode 100644
index 0000000..4409f39
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
@@ -0,0 +1,44 @@
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib
+
+import TestGame.Metadata
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Induction"
+Level 1
+
+Title "Simp"
+
+Introduction
+"
+In diesem Kapitel lernen wir endliche Summen und Induktion kennen.
+
+Eine endliche Summe läuft erstmal immer über einen endlichen Index
+`Fin n`, welcher $n$ Elemente
+$\\{0, 1, \\ldots, n-1\\}$ beinhaltet.
+
+Der Syntax für`∑ i : Fin n, (...)` (\\sum) ist der Syntax für $\\sum_{i=0}^n …$
+
+Als kann die Taktik `simp` (für \"simplification\") ganz viel Triviales vereinfachen.
+`simp` ist eine der stärksten Taktiken in Lean und verwendet
+ganz viele markierte Lemmas um das Goal zu vereinfachen.
+
+Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
+
+```
+@[simp]
+lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
+  [...]
+```
+
+Mit `simp?` anstatt `simp` kannst du zudem schauen, welche Lemmas von `simp` benutzt wurde.
+"
+
+Statement
+"Zeige dass `∑_{i = 0} ^ {n-1} 0 = 0 + 0`."
+    (n : ℕ) : (∑ i : Fin n, 0) = 0 + 0 := by
+  simp
+
+Tactics simp
diff --git a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
new file mode 100644
index 0000000..dee95ef
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
@@ -0,0 +1,31 @@
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib
+
+import TestGame.Metadata
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Induction"
+Level 2
+
+Title "endliche Summe"
+
+Introduction
+"
+Jetzt wollen wir ein paar Lemmas zu Summen kennenlernen, die `simp` nicht automatisch
+verwendet.
+
+Als erstes, kann man eine endliche Summe $\\sum_{i = 0}^n a_i + b_i$ mit
+`rw rw [Finset.sum_add_distrib]` als zwei Summen $\\sum_{i = 0}^n a_i + \\sum_{j = 0}^n b_j$
+auseinandernehmen.
+"
+
+Statement
+"Zeige dass $\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$."
+    (n : ℕ) : ∑ i : Fin n, ((i : ℕ) + 1) = n + (∑ i : Fin n, (i : ℕ)) := by
+  rw [Finset.sum_add_distrib]
+  simp
+  ring
+
+Tactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
new file mode 100644
index 0000000..7c6a034
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
@@ -0,0 +1,44 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Ring
+import Mathlib
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Induction"
+Level 3
+
+Title "Induktion"
+
+Introduction
+"
+Induktion ist eine wichtige Beweismethode, nicht zuletzt auch wenn es um endliche Summen geht.
+
+Die Taktik `induction' n with n n_ih` teilt das Goal in zwei Goals auf:
+
+1. Induktionsanfang, wo `n` durch `0` ersetzt wird.
+2. Induktionsschritt, wo `n` durch `n.succ` (also `(n + 1)`) ersetzt wird und man die
+   Induktionshypothese als Annahme `n_ih` kriegt.
+
+Für den Induktionsschritt braucht man fast immer zwei technische Lemmas:
+
+- `Fin.sum_univ_castSucc` um $\\sum_{i=0}^{n} a_i$ als
+  $\\sum_{i=0}^{n-1} a_i + a_n$ umzuschreiben.
+- `nat_succ` um `n.succ` zu `n + 1` umzuschreiben.
+"
+
+-- Note: I don't want to deal with Nat-division, so I stated it as `2 * ... = ...` instead.
+
+Statement
+"Zeige $\\sum_{i = 0}^n i = \\frac{n ⬝ (n + 1)}{2}$."
+  (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
+  induction n
+  simp
+
+  sorry
+  -- rw [Fin.sum_univ_castSucc]
+  -- simp [nat_succ]
+  -- rw [mul_add, hn]
+  -- ring
+
+Tactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
new file mode 100644
index 0000000..e35e16b
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
@@ -0,0 +1,31 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Ring
+import Mathlib
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Induction"
+Level 4
+
+Title "Bernoulli Ungleichung"
+
+Introduction
+"
+Hier nochmals eine Übung zur Induktion.
+"
+
+Statement
+"Zeige folgende Gleichung zur Summe aller ungeraden Zahlen:
+
+$\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
+    (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 := by
+  induction' n with n hn
+  simp
+  rw [nat_succ]
+  sorry -- waiting on Algebra.BigOperators.Fin
+  --simp [Fin.sum_univ_cast_succ]
+  --rw [hn]
+  --ring
+
+Tactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/L32_Induction.lean b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
similarity index 59%
rename from server/testgame/TestGame/Levels/Induction/L32_Induction.lean
rename to server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
index 4f6aa2e..20d6ed8 100644
--- a/server/testgame/TestGame/Levels/Induction/L32_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
@@ -2,11 +2,13 @@ import TestGame.Metadata
 import Mathlib.Tactic.Ring
 import Mathlib
 
+import TestGame.ToBePorted
+
 Game "TestGame"
 World "Induction"
-Level 2
+Level 5
 
-Title "Induktion"
+Title "Bernoulli Ungleichung"
 
 Introduction
 "
@@ -15,13 +17,20 @@ TODO: Induktion (& induktion vs rcases)
 "
 
 
-theorem nat_succ (n : ℕ) : Nat.succ n = n + 1 := rfl
+example (x : ℕ) (n : ℕ) : 1 + n * x ≤ (x + 1) ^ n := by
+  induction' n with n hn
+  simp
+  rw [Nat.succ_mul]
+  rw [Nat.pow_succ]
+  sorry
 
-lemma hh1 (n m : ℕ) (h : 2 * m = n) : m = n / 2 := by
-  rw [←h]
-  rw [Nat.mul_div_right]
+example (n : ℕ) : (∑ i : Fin (n + 1), ↑(2 * i - 1)) = n ^ 2 := by
+  induction' n with n hn
   simp
 
+
+
+
 Statement
 "Zeige $\\sum_{i = 0}^n i = \\frac{n ⬝ (n + 1)}{2}$."
   (n : ℕ) : (∑ i : Fin (n + 1), ↑i) = n * (n + 1) / 2 := by
diff --git a/server/testgame/TestGame/Levels/Induction/L31_Sum.lean b/server/testgame/TestGame/Levels/Induction/L31_Sum.lean
deleted file mode 100644
index eca12b2..0000000
--- a/server/testgame/TestGame/Levels/Induction/L31_Sum.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
-import TestGame.Metadata
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Induction"
-Level 1
-
-Title "Summe"
-
-Introduction
-"
-"
-
-Statement
-""
-    (n : ℕ) : 2 * (∑ i : Fin (n+1), ↑i) = n * (n + 1) := by
-  induction' n with n hn
-  simp
-  sorry -- done in Lean3.
-
-Tactics intro constructor assumption
diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean
index b8c2cef..226d5c7 100644
--- a/server/testgame/TestGame/ToBePorted.lean
+++ b/server/testgame/TestGame/ToBePorted.lean
@@ -10,3 +10,5 @@ lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by
   use 2 * x ^ 2
   rw [hx]
   ring
+
+theorem nat_succ (n : ℕ) : Nat.succ n = n + 1 := rfl