From 8a9b1a25e822b7e6b25aa0c693025cef40092c48 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 27 Feb 2023 12:20:01 +0100
Subject: [PATCH] levels

---
 .../testgame/TestGame/Levels/Inequality.lean  |  9 ++++
 .../Levels/Inequality/L01_Induction.lean      | 42 +++++++++++++++
 .../TestGame/Levels/Inequality/L02_LE.lean    | 24 +++++++++
 .../TestGame/Levels/Inequality/L03_Pos.lean   | 54 +++++++++++++++++++
 .../Levels/Inequality/L04_Linarith.lean       | 23 ++++++++
 .../Levels/Inequality/L05_Linarith.lean       | 28 ++++++++++
 .../TestGame/Levels/Prime/L01_Dvd.lean        | 52 ++++++++++++++++++
 7 files changed, 232 insertions(+)
 create mode 100644 server/testgame/TestGame/Levels/Inequality.lean
 create mode 100644 server/testgame/TestGame/Levels/Inequality/L01_Induction.lean
 create mode 100644 server/testgame/TestGame/Levels/Inequality/L02_LE.lean
 create mode 100644 server/testgame/TestGame/Levels/Inequality/L03_Pos.lean
 create mode 100644 server/testgame/TestGame/Levels/Inequality/L04_Linarith.lean
 create mode 100644 server/testgame/TestGame/Levels/Inequality/L05_Linarith.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L01_Dvd.lean

diff --git a/server/testgame/TestGame/Levels/Inequality.lean b/server/testgame/TestGame/Levels/Inequality.lean
new file mode 100644
index 0000000..c7d265c
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Inequality.lean
@@ -0,0 +1,9 @@
+import TestGame.Levels.Inequality.L01_Induction
+import TestGame.Levels.Inequality.L02_LE
+import TestGame.Levels.Inequality.L03_Pos
+import TestGame.Levels.Inequality.L04_Linarith
+import TestGame.Levels.Inequality.L05_Linarith
+
+Game "TestGame"
+World "Inequality"
+Title "Ungleichung"
diff --git a/server/testgame/TestGame/Levels/Inequality/L01_Induction.lean b/server/testgame/TestGame/Levels/Inequality/L01_Induction.lean
new file mode 100644
index 0000000..5c692c7
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Inequality/L01_Induction.lean
@@ -0,0 +1,42 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "Inequality"
+Level 1
+
+Title "Induktion"
+
+set_option tactic.hygienic false
+
+Introduction
+"
+Hier lernst du Induktion und Ungleichungen kennen. Beides essenziele Grundlagen, die du
+für spätere Aufgaben brauchst.
+
+Die Leantaktik `induction n` führt einen Induktionsbeweis über `(n : ℕ)`. Hier zuerst
+ein abstraktes Beispiel.
+"
+
+Statement
+"Sei $P(n)$ eine logische Aussage über die natürliche Zahl.
+Agenommen $P(0)$ ist wahr und $P(m) \\Rightarrow P(m+1)$ für alle $m$,
+dann gilt $P(n)$ für alle $n \\in \\mathbb{N}.$"
+    (n : ℕ) (P : ℕ → Prop) (h_base : P 0) (h_step : ∀ m, P m → P m.succ) : P n := by
+  induction n
+  assumption
+  apply h_step
+  assumption
+
+-- TODO: Why are these not shown.
+HiddenHint (n : ℕ) (P : ℕ → Prop) : P n =>
+"Benutze `induction n`."
+
+Hint (P : ℕ → Prop) : P 0 =>
+"Das ist die Induktionsverankerung, hier musst du $P(0)$ zeigen."
+
+Hint (P : ℕ → Prop) (m : ℕ) (hi : P m) : P (Nat.succ m) =>
+"An der Stelle kommt der Beweis $P(m) \\Rightarrow P(m+1)$.
+
+In diesem Beispiel kannst du `apply` benützen."
+
+NewTactics induction
diff --git a/server/testgame/TestGame/Levels/Inequality/L02_LE.lean b/server/testgame/TestGame/Levels/Inequality/L02_LE.lean
new file mode 100644
index 0000000..10168c5
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Inequality/L02_LE.lean
@@ -0,0 +1,24 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "Inequality"
+Level 2
+
+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 `<`.
+
+Zudem sind `<` und `≤` auf `ℕ` so definiert, dass `0 < n` und `1 ≤ n` per Definition
+äquivalent sind. Die folgende Aussage ist also mit `rfl` beweisbar.
+"
+
+Statement
+"$0 < n$ und $1 ≤ n$ sind äquivalente Aussagen."
+    (n m : ℕ) : m < n ↔ m.succ ≤ n := by
+  rfl
diff --git a/server/testgame/TestGame/Levels/Inequality/L03_Pos.lean b/server/testgame/TestGame/Levels/Inequality/L03_Pos.lean
new file mode 100644
index 0000000..840cc30
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Inequality/L03_Pos.lean
@@ -0,0 +1,54 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "Inequality"
+Level 3
+
+Title "Kleinergleich"
+
+Introduction
+"
+Es gibt zwei intrinsische Möglichkeiten, zu sagen dass `(n : ℕ)` nicht Null ist:
+`n ≠ 0` oder `0 < n`.
+
+Das folgende Lemma kannst du immer brauchen um zwischen den beiden zu wechseln.
+
+Note: `0 < n` wird in Lemmanamen oft mit `_pos` beschrieben anstatt `zero_lt`, siehe z.B.
+`Nat.succ_pos`.
+"
+
+Statement zero_lt_iff
+"$0 < n$ und $n \\ne 0$ sind äquivalente Aussagen."
+    (n : ℕ) : 0 < n ↔ n ≠ 0 := by
+  constructor
+  intro h
+  by_contra g
+  rw [g] at h
+  contradiction
+  intro h
+  induction n
+  contradiction
+  apply Nat.succ_pos
+
+NewLemmas Nat.succ_pos
+
+Hint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
+"An dieser Stelle fürst du am besten einen Beweis durch Widerspruch."
+
+HiddenHint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
+"Das macht man mit `by_contra`."
+
+Hint (n : ℕ) (h : 0 < n) (g : n = 0) : False =>
+"Brauche `rw [_] at _` um eine Annahme `0 < 0` zu erzeugen."
+
+HiddenHint (h : 0 < 0) : False =>
+"Mit `contradiction` schliesst du den Widerspruchsbeweis."
+
+Hint (n : ℕ) (h : n ≠ 0) : 0 < n =>
+"Diese Richtung beweist du am besten per Induktion."
+
+HiddenHint (n : ℕ) (h : n ≠ 0) : 0 < n =>
+"Starte mit `induction n`."
+
+Hint (m : ℕ) : 0 < Nat.succ m =>
+"Hier kannst du das Lemma `Nat.succ_pos` anwenden."
diff --git a/server/testgame/TestGame/Levels/Inequality/L04_Linarith.lean b/server/testgame/TestGame/Levels/Inequality/L04_Linarith.lean
new file mode 100644
index 0000000..8c0beb0
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Inequality/L04_Linarith.lean
@@ -0,0 +1,23 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Linarith
+
+Game "TestGame"
+World "Inequality"
+Level 4
+
+Title "Linarith"
+
+Introduction
+"
+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
+
+NewLemmas zero_lt_iff
diff --git a/server/testgame/TestGame/Levels/Inequality/L05_Linarith.lean b/server/testgame/TestGame/Levels/Inequality/L05_Linarith.lean
new file mode 100644
index 0000000..c846bc0
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Inequality/L05_Linarith.lean
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Linarith
+
+Game "TestGame"
+World "Inequality"
+Level 5
+
+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/L01_Dvd.lean b/server/testgame/TestGame/Levels/Prime/L01_Dvd.lean
new file mode 100644
index 0000000..5edc0da
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime/L01_Dvd.lean
@@ -0,0 +1,52 @@
+import TestGame.Metadata
+
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "Prime"
+Level 1
+
+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
+
+HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k =>
+"
+Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
+sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
+"
+
+HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (x : ℕ) (h : n = m * x) (g : m ∣ k) : m ∣ n + k =>
+"
+Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
+sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
+"
+
+HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (y : ℕ)  (h : m ∣ n) (g : k = m * y) : m ∣ n + k =>
+"
+Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
+sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
+"
+
+HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (x : ℕ) (y : ℕ) (h : n = m * x) (g : k = m * y) : m ∣ n + k =>
+"
+Jetzt kannst du mit `use` eine Zahl angeben, so dass $m * X = n + k$.
+"