From abcc3087d3562dd520f4c6886b481c6d1e9a1d99 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 8 Feb 2023 16:05:51 +0100
Subject: [PATCH] new levels

---
 server/testgame/TestGame.lean                 |  9 ++--
 server/testgame/TestGame/LemmaDocs.lean       |  2 +
 .../testgame/TestGame/Levels/Induction.lean   |  2 +
 .../Induction/{T00_Sum.lean => L05_Sum.lean}  |  2 +-
 .../Levels/Induction/L06_SumComm.lean         | 25 +++++++++++
 .../Levels/Induction/T01_Induction.lean       | 16 +++++--
 .../Levels/Induction/T02_Induction.lean       |  9 ++++
 .../Levels/Induction/T03_SumComm.lean         | 34 --------------
 ...L10_Bernoulli.lean => T03__Bernoulli.lean} |  0
 server/testgame/TestGame/Levels/Prime.lean    | 11 ++++-
 .../TestGame/Levels/Prime/L01_Linarith.lean   | 29 ++++++++++++
 .../TestGame/Levels/Prime/L01_Prime.lean      | 41 -----------------
 .../TestGame/Levels/Prime/L02_Linarith.lean   | 31 +++++++++++++
 .../TestGame/Levels/Prime/L03_Dvd.lean        | 29 ++++++++++++
 .../TestGame/Levels/Prime/L04_Prime.lean      | 45 +++++++++++++++++++
 .../TestGame/Levels/Prime/L05_Prime.lean      | 42 +++++++++++++++++
 .../Levels/Prime/L06_ExistsUnique.lean        | 34 ++++++++++++++
 server/testgame/TestGame/TacticDocs.lean      |  6 +++
 18 files changed, 280 insertions(+), 87 deletions(-)
 rename server/testgame/TestGame/Levels/Induction/{T00_Sum.lean => L05_Sum.lean} (99%)
 create mode 100644 server/testgame/TestGame/Levels/Induction/L06_SumComm.lean
 delete mode 100644 server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
 rename server/testgame/TestGame/Levels/Induction/{L10_Bernoulli.lean => T03__Bernoulli.lean} (100%)
 create mode 100644 server/testgame/TestGame/Levels/Prime/L01_Linarith.lean
 delete mode 100644 server/testgame/TestGame/Levels/Prime/L01_Prime.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L02_Linarith.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L03_Dvd.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L04_Prime.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L05_Prime.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean

diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index eacf2ca..c4742bf 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -4,7 +4,7 @@ import TestGame.Levels.Proposition
 import TestGame.Levels.Implication
 import TestGame.Levels.Predicate
 import TestGame.Levels.Contradiction
---import TestGame.Levels.Prime
+import TestGame.Levels.Prime
 import TestGame.Levels.Induction
 
 import TestGame.Levels.LeanStuff
@@ -38,12 +38,9 @@ Conclusion
 "Fertig!"
 
 
-Path Proposition → Implication → Predicate → Contradiction → LeanStuff
--- Path Predicate → Prime
+Path Proposition → Implication → Predicate → Prime
+Path Predicate → Contradiction → LeanStuff → SetTheory → SetFunction
 Path Predicate → Induction → LeanStuff → Function → SetFunction
-
-Path LeanStuff → SetTheory → SetFunction
-
 Path SetTheory → SetTheory2
 
 
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index c8abd69..14622ce 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -93,6 +93,8 @@ LemmaDoc Subset.antisymm_iff as Subset.antisymm_iff in "Set"
 
 
 
+LemmaDoc Nat.prime_def_lt'' as Nat.prime_def_lt'' in "Nat"
+""
 
 
 
diff --git a/server/testgame/TestGame/Levels/Induction.lean b/server/testgame/TestGame/Levels/Induction.lean
index 4931437..7484e8d 100644
--- a/server/testgame/TestGame/Levels/Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction.lean
@@ -2,6 +2,8 @@ import TestGame.Levels.Induction.L01_Simp
 import TestGame.Levels.Induction.L02_Sum
 import TestGame.Levels.Induction.L03_Induction
 import TestGame.Levels.Induction.L04_SumOdd
+import TestGame.Levels.Induction.L05_Sum
+import TestGame.Levels.Induction.L06_SumComm
 
 Game "TestGame"
 World "Induction"
diff --git a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean b/server/testgame/TestGame/Levels/Induction/L05_Sum.lean
similarity index 99%
rename from server/testgame/TestGame/Levels/Induction/T00_Sum.lean
rename to server/testgame/TestGame/Levels/Induction/L05_Sum.lean
index 73a7454..283dbb5 100644
--- a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
+++ b/server/testgame/TestGame/Levels/Induction/L05_Sum.lean
@@ -6,7 +6,7 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Induction"
-Level 3
+Level 5
 
 Title "Induktion"
 
diff --git a/server/testgame/TestGame/Levels/Induction/L06_SumComm.lean b/server/testgame/TestGame/Levels/Induction/L06_SumComm.lean
new file mode 100644
index 0000000..f3e6366
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction/L06_SumComm.lean
@@ -0,0 +1,25 @@
+
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib
+
+import TestGame.Metadata
+
+set_option tactic.hygienic false
+
+open BigOperators
+
+Game "TestGame"
+World "Induction"
+Level 6
+
+Title "Summe vertauschen"
+
+Introduction
+"
+"
+
+Statement
+""
+    (n m : ℕ) : ∑ i : Fin n, ∑ j : Fin m, (i : ℕ) * j =
+    ∑ j : Fin m, ∑ i : Fin n, (i : ℕ) * j := by
+  rw [Finset.sum_comm]
diff --git a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
index 296806c..dbd37a2 100644
--- a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
@@ -5,12 +5,16 @@ import TestGame.Metadata
 
 set_option tactic.hygienic false
 
+open Nat
+
 Game "TestGame"
 World "Induction"
 Level 2
 
 Title "endliche Summe"
 
+-- TODO: Tactics `mono` and `omega` are not ported yet.
+
 Introduction
 "
 2^n > n^2   für   n ≥ 5
@@ -18,10 +22,14 @@ Introduction
 
 Statement
 "2^n > n^2   für   n ≥ 5"
-    (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n := by
-  induction n with
-  | 0 | 1 | 2 | 3 | 4 => by contradiction
-  | n.succ  => by sorry
+    (n : ℕ) : (n + 5)^2 < 2 ^ (n + 5) := by
+induction' n with n ih
+simp
+rw [succ_eq_add_one]
+simp_rw [add_pow_two] at *
+ring_nf at ih ⊢
+sorry
+
 
 
 example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n
diff --git a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
index 7385153..4d97f96 100644
--- a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
@@ -20,7 +20,16 @@ Statement
 "n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n"
     (n : ℤ) : 3 ∣ n^3 + 2*n := by
   induction n
+  induction a
+  norm_cast
+  change 3 ∣ (Nat.succ n : ℤ) ^ 3 + 2 * (Nat.succ n : ℤ)
+  rw [Int.ofNat_succ]
   sorry
   sorry
 
+-- example (n : ℕ) : (n - 1) * (n + 1) = (n ^ 2 - 1) := by
+--   induction' n with n hn
+--   ring
+--   rw [Nat.succ_eq_one_add]
+--   rw []
 NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
deleted file mode 100644
index 96e789f..0000000
--- a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
+++ /dev/null
@@ -1,34 +0,0 @@
-
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
-import TestGame.Metadata
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Induction"
-Level 1
-
-Title "Simp"
-
-Introduction
-"
-"
-
-Statement
-""
-    (n : ℕ) : True := by
-  trivial
-
-NewTactics simp
-
-
--- Σ_i Σ_j ... = Σ_j Σ_i ...
--- rw [sum_comm]
-example : ¬ ∀ (x : ℕ), x ≥ 10 := by
-  push_neg
-  use 5
-  simp
-
-¬ ∀ (...) ↔ ∃ (¬ ...)
diff --git a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean b/server/testgame/TestGame/Levels/Induction/T03__Bernoulli.lean
similarity index 100%
rename from server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
rename to server/testgame/TestGame/Levels/Induction/T03__Bernoulli.lean
diff --git a/server/testgame/TestGame/Levels/Prime.lean b/server/testgame/TestGame/Levels/Prime.lean
index 7152735..f2de7ce 100644
--- a/server/testgame/TestGame/Levels/Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime.lean
@@ -1 +1,10 @@
-import TestGame.Levels.Prime.L01_Prime
+import TestGame.Levels.Prime.L01_Linarith
+import TestGame.Levels.Prime.L02_Linarith
+import TestGame.Levels.Prime.L03_Dvd
+import TestGame.Levels.Prime.L04_Prime
+import TestGame.Levels.Prime.L05_Prime
+import TestGame.Levels.Prime.L06_ExistsUnique
+
+Game "TestGame"
+World "Prime"
+Title "mehr Nat"
diff --git a/server/testgame/TestGame/Levels/Prime/L01_Linarith.lean b/server/testgame/TestGame/Levels/Prime/L01_Linarith.lean
new file mode 100644
index 0000000..3bf672a
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L01_Linarith.lean
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Linarith
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Prime"
+Level 1
+
+Title "Kleinergleich"
+
+Introduction
+"
+Ungleichheiten werden in Lean generell immer als Kleinergleich `≤` (`\\le`) oder `<`
+geschrieben.
+
+Die Symbole `≥` und `>` gibt es zwar auch, sind aber nur Notation für die gleiche
+Aussage mit `≤` und `<`.
+
+Die Taktik `linarith` kann alle Systeme von linearen (Un-)gleichungen über `ℤ`, `ℚ`, etc. lösen.
+Über `ℕ` ist sie etwas schwächer, aber einfache Aussagen kann sie trotzdem beweisen.
+"
+
+Statement
+"Wenn $n \\ge 2$, zeige, dass $n$ nich Null sein kann."
+    (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
+  linarith
+
+NewTactics linarith
diff --git a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
deleted file mode 100644
index 2361ca8..0000000
--- a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
+++ /dev/null
@@ -1,41 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Data.Nat.Prime
-
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-import Mathlib.Tactic.Contrapose
-import Mathlib.Tactic.Use
-import Mathlib.Tactic.Ring
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Prime"
-Level 1
-
-Title "Primzahlen"
-
-Introduction
-"
-"
-
-Statement
-  "TODO"
-    (n : ℕ) : ∃! (n : ℕ), Nat.Prime n ∧ Even n := by
-  use (2 : ℕ)
-  constructor
-  simp only []
-  intro y
-  rintro ⟨h₁, h₂⟩
-  rw [← Nat.Prime.even_iff]
-  assumption
-  assumption
-
-example : True := by
-  by_cases h : 1 = 0
-
-Conclusion ""
-
-NewTactics
-
-NewLemmas
diff --git a/server/testgame/TestGame/Levels/Prime/L02_Linarith.lean b/server/testgame/TestGame/Levels/Prime/L02_Linarith.lean
new file mode 100644
index 0000000..44c4af5
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L02_Linarith.lean
@@ -0,0 +1,31 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Linarith
+
+Game "TestGame"
+World "Prime"
+Level 2
+
+Title "Linarith"
+
+Introduction
+"
+Sobald man mit einem Ring arbeitet, der eine lineare Order hat (also z.B. `ℤ` oder `ℚ`),
+ist `linarith` stärker und kann Systeme von Gleichungen und Ungleichungen angehen.
+
+`linarith` kann aber nur mit linearen Ungleichungen umgehen, mit Termen der Form `x ^ 2`
+kann es nicht umgehen.
+"
+
+Statement
+"Angenommen man hat für zwei Ganzzahlen $x, y$ folgende Ungleichungen.
+$$
+\\begin{aligned} 5 * y &\\le 35 - 2 * x \\\\ 2 * y &\\le x + 3 \\end{aligned}
+$$
+Zeige, dass $y \\le 5$.
+
+"
+    (x y : ℤ)
+    (h₂ : 5 * y ≤ 35 - 2 * x)
+    (h₃ : 2 * y ≤ x + 3)
+    : y ≤ 5 := by
+  linarith
diff --git a/server/testgame/TestGame/Levels/Prime/L03_Dvd.lean b/server/testgame/TestGame/Levels/Prime/L03_Dvd.lean
new file mode 100644
index 0000000..47d2f76
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L03_Dvd.lean
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "Prime"
+Level 3
+
+Title "Teilbarkeit"
+
+Introduction
+"
+Die Aussage \"$m$ teilt $n$.\" wird in Lean als `m | n` (`\\|`) geschrieben.
+
+**Wichtig:** `∣` (Teilbarkeit) ist ein spezielles Unicode Symbol, das nicht dem
+senkrechten Strich auf der Tastatur (`|`) entspricht. Man erhält es mit `\\|`.
+
+`m ∣ n` bedeutet `∃ c, n = m * c`, das heisst, man kann damit genau gleich umgehen
+wie mit einem `∃`-Quantifier.
+"
+
+Statement dvd_add
+  "Wenn $m$ ein Teiler von $n$ und $k$ ist, dann teilt es die Summe."
+  (n m k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k := by
+  rcases h with ⟨x, h⟩
+  rcases g with ⟨y, g⟩
+  use x + y
+  rw [h, g]
+  ring
diff --git a/server/testgame/TestGame/Levels/Prime/L04_Prime.lean b/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
new file mode 100644
index 0000000..56a9937
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
@@ -0,0 +1,45 @@
+import TestGame.Metadata
+import Mathlib.Data.Nat.Prime
+
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Prime"
+Level 4
+
+Title "Primzahlen"
+
+Introduction
+"
+Um zu sagen, dass eine natürliche Zahl $n$ eine Primzahl ist, braucht man
+eine Aussage `Nat.Prime n`, ähnlich wie `Even n`.
+
+Primzahlen sind ein Objekt in Lean, das genug abstrakt definiert ist, dass es sich
+aus mathematischer Sicht nicht lohnt mit der Definition zu arbeiten.
+
+Alle wichtigen Lemmas um mit Primzahlen zu arbeiten sind in
+[`import Data.Nat.Prime`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html)
+
+Insbesondere `Nat.prime_def_lt''` welches die aus der Schule bekannte Definition einer
+Primzahl `Prime p ↔ 2 ≤ p ∧ (∀ m, m ∣ p → m = 1 ∨ m = p)` gibt.
+
+Beachte: In Lean gibt es auch noch den Ausdruck `Prime n`, der beschreibt generelle
+Primelemente in einem generellen Ring. Wenn man mit natürlichen
+Zahlen arbeitet, ist es besser `Nat.Prime` zu verwenden, obwohl man natürlich zeigen kann
+dass die beiden äquivalent sind.
+"
+
+Statement
+"Zeige dass die einzigen Teiler einer Primzahl $1$ und $p$ sind."
+    (p : ℕ) (h : Nat.Prime p) : ∀ (x : ℕ), (x ∣ p) → x = 1 ∨ x = p := by
+  rw [Nat.prime_def_lt''] at h
+  rcases h with ⟨_, h₂⟩
+  assumption
+
+NewLemmas Nat.prime_def_lt''
diff --git a/server/testgame/TestGame/Levels/Prime/L05_Prime.lean b/server/testgame/TestGame/Levels/Prime/L05_Prime.lean
new file mode 100644
index 0000000..09d5ac6
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L05_Prime.lean
@@ -0,0 +1,42 @@
+import TestGame.Metadata
+import Mathlib.Data.Nat.Prime
+
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Prime"
+Level 5
+
+Title "Primzahlen"
+
+Introduction
+"
+Mathematisch gesehen, bedeutet die Definition von vorhin dass $p$ ein
+irreduzibles Element ist, und Primzahlen sind oft durch
+`∀ (a b : ℕ), p ∣ a * b → p ∣ a ∨ p ∣ b`
+definiert. Auf den natürlichen Zahlen, sind die beiden äquivalent.
+"
+
+Statement
+"Zeige dass $p \\ge 2$ eine Primzahl ist, genau dann wenn
+$p \\mid a\\cdot b \\Rightarrow (p \\mid a) \\lor (p \\mid b)$."
+    (p : ℕ) (h₂ : 2 ≤ p):
+    Nat.Prime p ↔ ∀ (a b : ℕ), p ∣ a * b → p ∣ a ∨ p ∣ b := by
+  constructor
+  intro h a b
+  apply (Nat.Prime.dvd_mul h).mp
+  intro h
+  rw [Nat.prime_iff]
+  change p ≠ 0 ∧ ¬IsUnit p ∧ ∀ a b, p ∣ a * b → p ∣ a ∨ p ∣ b
+  rw [Nat.isUnit_iff, ←and_assoc]
+  constructor
+  constructor
+  linarith
+  linarith
+  assumption
diff --git a/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean b/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean
new file mode 100644
index 0000000..b5b15e2
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean
@@ -0,0 +1,34 @@
+import TestGame.Metadata
+import Mathlib.Data.Nat.Prime
+
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Prime"
+Level 6
+
+Title "Existiert eindeutig"
+
+Introduction
+"
+Hier lässt sich noch eine neue Notation einführen: `∃!` bedeutet
+\"es existiert ein eindeutiges\" und ist definiert als
+
+
+"
+
+Statement
+"Zeige dass die einzige gerade Primzahl $2$ ist."
+    : ∃! p, Nat.Prime p ∧ Even p := by
+  use 2
+  constructor
+  simp
+  rintro y ⟨hy, hy'⟩
+  rw [←Nat.Prime.even_iff hy]
+  assumption
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index 488aa67..4dc6b45 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -61,6 +61,12 @@ TacticDoc rewrite
 Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
 "
 
+TacticDoc linarith
+"
+## Beschreibung
+
+"
+
 TacticDoc rw
 "
 ## Beschreibung