From 9d1a591670eec25be672530e07537180fdbdeec4 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 19 Jan 2023 15:43:29 +0100
Subject: [PATCH] changes to levels

---
 .../TestGame/Levels/LeftOvers/L14_NotNot.lean | 33 ---------
 .../testgame/TestGame/Levels/Predicate.lean   |  8 +++
 .../TestGame/Levels/Predicate/L01_Ring.lean   |  9 ++-
 .../Levels/Predicate/L02_Rewrite.lean         | 70 +++++++++++++++++++
 .../{L04b_Rewrite.lean => L03_Rewrite.lean}   |  5 +-
 .../Levels/Predicate/L04_Rewrite.lean         | 50 -------------
 .../{L02_Ring.lean => L04_Ring.lean}          |  7 +-
 .../Predicate/{L02_Rfl.lean => L05_Rfl.lean}  |  2 +-
 .../{L03_Exists.lean => L06_Exists.lean}      |  2 +-
 .../{L04_Forall.lean => L07_Forall.lean}      | 14 +++-
 .../{L09_PushNeg.lean => L08_PushNeg.lean}    |  2 +-
 .../Levels/Predicate/L09_Summary.lean         | 60 ++++++++++++++++
 server/testgame/TestGame/Levels/Prime.lean    |  1 +
 .../TestGame/Levels/Prime/L01_Prime.lean      |  0
 .../TestGame/Levels/Proving/L01_Contra.lean   | 20 +++++-
 15 files changed, 187 insertions(+), 96 deletions(-)
 delete mode 100644 server/testgame/TestGame/Levels/LeftOvers/L14_NotNot.lean
 create mode 100644 server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
 rename server/testgame/TestGame/Levels/Predicate/{L04b_Rewrite.lean => L03_Rewrite.lean} (89%)
 delete mode 100644 server/testgame/TestGame/Levels/Predicate/L04_Rewrite.lean
 rename server/testgame/TestGame/Levels/Predicate/{L02_Ring.lean => L04_Ring.lean} (71%)
 rename server/testgame/TestGame/Levels/Predicate/{L02_Rfl.lean => L05_Rfl.lean} (98%)
 rename server/testgame/TestGame/Levels/Predicate/{L03_Exists.lean => L06_Exists.lean} (99%)
 rename server/testgame/TestGame/Levels/Predicate/{L04_Forall.lean => L07_Forall.lean} (68%)
 rename server/testgame/TestGame/Levels/Predicate/{L09_PushNeg.lean => L08_PushNeg.lean} (99%)
 create mode 100644 server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime.lean
 create mode 100644 server/testgame/TestGame/Levels/Prime/L01_Prime.lean

diff --git a/server/testgame/TestGame/Levels/LeftOvers/L14_NotNot.lean b/server/testgame/TestGame/Levels/LeftOvers/L14_NotNot.lean
deleted file mode 100644
index 40b9ba0..0000000
--- a/server/testgame/TestGame/Levels/LeftOvers/L14_NotNot.lean
+++ /dev/null
@@ -1,33 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Implication"
-Level 20
-
-Title "Nicht-nicht"
-
-Introduction
-"
-Wenn man ein Nicht (`¬`) im Goal hat, will man meistens einen Widerspruch starten,
-wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form
-`¬ (¬ A)`, in welchem Fall das Lemma `not_not` nützlich ist, welches du mit
-`rw` oder `apply` benützen kannst.
-"
-
-Statement
-    "Zeige, dass $\\neg(\\neg A)$ äquivalent zu $A$ ist."
-    (A : Prop) : ¬ (¬ A) ↔ A := by
-  rw [not_not]
-
-Message (A : Prop) : ¬ (¬ A) ↔ A => "Da `not_not` ein Lemma der Form `X ↔ Y` ist,
-kannst du wahlweise `rw [not_not]` oder `apply not_not` benützen.
-
-- `rw` ersetzt `¬ (¬ A)` mit `A` und schliesst dann `A ↔ A` mit `rfl`.
-- `apply` hingegen funktioniert hier nur, weil das gesamte Goal
-genau mit der Aussage des Lemmas übereinstimmt.
-"
-
-Tactics rw apply
-
-Lemmas not_not
diff --git a/server/testgame/TestGame/Levels/Predicate.lean b/server/testgame/TestGame/Levels/Predicate.lean
index 80f8942..85d84b1 100644
--- a/server/testgame/TestGame/Levels/Predicate.lean
+++ b/server/testgame/TestGame/Levels/Predicate.lean
@@ -1 +1,9 @@
 import TestGame.Levels.Predicate.L01_Ring
+import TestGame.Levels.Predicate.L02_Rewrite
+import TestGame.Levels.Predicate.L03_Rewrite
+import TestGame.Levels.Predicate.L04_Ring
+import TestGame.Levels.Predicate.L05_Rfl
+import TestGame.Levels.Predicate.L06_Exists
+import TestGame.Levels.Predicate.L07_Forall
+import TestGame.Levels.Predicate.L08_PushNeg
+import TestGame.Levels.Predicate.L09_Summary
diff --git a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
index 21696e0..6304881 100644
--- a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
@@ -13,12 +13,15 @@ Introduction
 "
 Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon kurz begegnet.
 
-Gleichungen, die nur die Operationen `+, -, *, ^` und Variablen enthalten, kann Lean mit der
-Taktik `ring` beweisen.
+Gleichungen, die nur die Operationen `+, -, *, ^` (Addition, Subtraktion, Multiplikation, Potenz)
+und Variablen enthalten, kann Lean mit der Taktik `ring` beweisen.
 
 Diese Taktik funktioniert nicht nur über den natürlichen Zahlen,
 sondern auch in (kommutativen) Gruppen, Ringen, und Körpern. Sie heisst `ring`, weil sie für Ringe
 entwickelt wurde.
+
+(Note: Division `/` ignorieren wir hier erst einmal, weil diese auf `ℕ`
+nicht kanonisch definiert ist.)
 "
 
 Statement
@@ -37,3 +40,5 @@ Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
 "
 
 Tactics ring
+
+#eval 4 / 6
diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
new file mode 100644
index 0000000..de26cf0
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
@@ -0,0 +1,70 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Predicate"
+Level 2
+
+Title "Rewrite"
+
+Introduction
+"
+Wir haben gesehen, dass man mit `rw` Äquivalenzen wie `A ↔ B` brauchen kann, um im Goal
+$A$ durch $B$ zu ersetzen.
+
+Genau gleich kann man auch Gleichungen `a = b` mit `rw` verwenden.
+"
+
+Statement umschreiben
+"Angenommen man hat die Gleichheiten
+
+$$
+\\begin{aligned} a &= b \\\\ a &= d \\\\ c &= d \\end{aligned}
+$$
+
+Zeige dass $b = c$."
+(a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rw [h₁]
+  rw [←h₂]
+  assumption
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
+"Im Goal kommt `c` vor und `h₁` sagt `c = d`.
+Probiers doch mit `rw [h₁]`."
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = c =>
+"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
+Probiers doch mit `rw [h₁]`."
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
+" Man kann auch rückwärts umschreiben: `h₂` sagt `a = b` mit
+`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)"
+
+Hint (a : ℕ) (b : ℕ) (h : a = b) : a = b =>
+"Schau mal durch die Annahmen durch."
+
+
+
+-- These should not be necessary if they don't use `rw [] at`.
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = c) : b = c =>
+"Auch eine Möglichkeit... Kannst du das Goal so umschreiben,
+dass es mit einer Annahme übereinstimmt?"
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : b = d) : b = c =>
+"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?"
+
+Message (a : ℕ) (b : ℕ) (h : b = a) : a = b =>
+"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `a = A` umschreibst, kann man es mit
+`rfl` beweisen (rsp. das passiert automatisch.)"
+
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : d = a) : b = c =>
+"das ist nicht der optimale Weg..."
+
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : a = d) : b = c =>
+"das ist nicht der optimale Weg..."
+
+
+
+Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
+
+Tactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L04b_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
similarity index 89%
rename from server/testgame/TestGame/Levels/Predicate/L04b_Rewrite.lean
rename to server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
index 5cf54e4..e540543 100644
--- a/server/testgame/TestGame/Levels/Predicate/L04b_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
@@ -3,13 +3,14 @@ import Mathlib
 
 Game "TestGame"
 World "Predicate"
-Level 4
+Level 3
 
 Title "Rewrite"
 
 Introduction
 "
-Mit `rw` kann man nicht nur das Goal sondern auch andere Annahmen umschreiben:
+Als Übung erinnern wir daran, dass man mit `rw [h] at g` auch in anderen Annahmen umschreiben
+kann:
 
 Wenn `(h : X = Y)` ist, dann ersetzt `rw [h] at g` in der Annahme
 `g` das `X` durch `Y`.
diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L04_Rewrite.lean
deleted file mode 100644
index 361de35..0000000
--- a/server/testgame/TestGame/Levels/Predicate/L04_Rewrite.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Predicate"
-Level 3
-
-Title "Rewrite"
-
-Introduction
-"
-Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern man braucht
-mehrere Schritte im Beweis.
-
-Wenn man eine Annahme `(h : X = Y)` hat,
-kann die Taktik `rw [h]` im Goal $X$ durch $Y$ ersetzen.
-(`rw` steht für *rewrite*)
-"
-
-Statement umschreiben
-"Angenommen man hat die Gleichheiten
-
-$$
-\\begin{aligned} a &= b \\\\ a &= d \\\\ c &= d \\end{aligned}
-$$
-
-Zeige dass $b = c$."
-(a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
-  rw [h₁]
-  rw [←h₂]
-  assumption
-
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man tippt diese mit
-`\\1`, `\\2`, `\\3`, …"
-
-Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Im Goal kommt `c` vor und `h₁` sagt `c = d`.
-Probiers doch mit `rw [h₁]`."
-
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
-" Man kann auch rückwärts umschreiben: `h₂` sagt `a = b` mit
-`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)"
-
-Hint (a : ℕ) (b : ℕ) (h : a = b) : a = b =>
-"Schau mal durch die Annahmen durch."
-
-Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
-
-Tactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
similarity index 71%
rename from server/testgame/TestGame/Levels/Predicate/L02_Ring.lean
rename to server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
index 8c693f0..85ae5f3 100644
--- a/server/testgame/TestGame/Levels/Predicate/L02_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
@@ -3,13 +3,16 @@ import Mathlib.Tactic.Ring
 
 Game "TestGame"
 World "Predicate"
-Level 5
+Level 4
 
 Title "Natürliche Zahlen"
 
 Introduction
 "
-Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden.
+Oft braucht man eine Kombination von `rw` und `ring` um Gleichungen zu lösen.
+
+Zuerst setzt man mit `rw` die vorhandenen Annahmen ein, und sobald die beiden Seiten
+einer Gleichung im Goal rechnerisch gleich sind, kan `ring` dies beweisen.
 "
 
 Statement
diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
similarity index 98%
rename from server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean
rename to server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
index 3cedce1..73a940f 100644
--- a/server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
@@ -2,7 +2,7 @@ import TestGame.Metadata
 
 Game "TestGame"
 World "Predicate"
-Level 6
+Level 5
 
 Title "Definitionally equal"
 
diff --git a/server/testgame/TestGame/Levels/Predicate/L03_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
similarity index 99%
rename from server/testgame/TestGame/Levels/Predicate/L03_Exists.lean
rename to server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
index 02900e7..4db1672 100644
--- a/server/testgame/TestGame/Levels/Predicate/L03_Exists.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
@@ -8,7 +8,7 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Predicate"
-Level 7
+Level 6
 
 Title "Gerade/Ungerade"
 
diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
similarity index 68%
rename from server/testgame/TestGame/Levels/Predicate/L04_Forall.lean
rename to server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
index 400c156..30b10cc 100644
--- a/server/testgame/TestGame/Levels/Predicate/L04_Forall.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
@@ -8,7 +8,7 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Predicate"
-Level 8
+Level 7
 
 Title "Für alle"
 
@@ -16,7 +16,19 @@ Introduction
 "
 Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
 
+Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
+
+Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
+auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
+
+Also folgende Annahme und Lemma sind genau :
+- `(le_square : ∀ (n : ℕ), n ≤ n^2)`
+- `lemma le_square (n : ℕ) : n ≤ n^2`
+
 Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
+
+
+TODO: 1-2 Aufgaben mehr.
 "
 
 Statement
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
similarity index 99%
rename from server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
rename to server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
index 7e3f625..0909843 100644
--- a/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
@@ -6,7 +6,7 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Predicate"
-Level 9
+Level 8
 
 Title "PushNeg"
 
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
new file mode 100644
index 0000000..d6d8e6b
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
@@ -0,0 +1,60 @@
+import TestGame.Metadata
+import Mathlib.Tactic.PushNeg
+import Mathlib
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Predicate"
+Level 9
+
+Title "Zusammenfassung"
+
+Introduction
+"
+Damit bist du am Ende der dritten Lektion angekommen.
+Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
+Abschlussaufgabe.
+
+## Notationen / Begriffe
+
+|               | Beschreibung                |
+|:--------------|:----------------------------|
+| `ℕ`           | Die natürlichen Zahlen.     |
+| `∃`           | Existential-Quantifier      |
+| `∀`           | Forall-Quantifier           |
+| `even n`      | `n` ist gerade              |
+| `odd n`       | `n` ist ungerade            |
+|               |                             |
+|               |                             |
+|               |                             |
+|               |                             |
+|               |                             |
+
+
+## Taktiken
+
+|       | Taktik                    | Beispiel                                               |
+|:------|:--------------------------|:-------------------------------------------------------|
+| *11ᶜ* | `rw`                      | Umschreiben mit Gleichungen.                           |
+| 12    | `ring`                    | Löst Gleichungen mit `+, -, *, ^`.                     |
+| 13    | `unfold`                  | Setzt visuell die Bedeutung einer Definition ein.      |
+| 14    | `use`                     | Um ein `∃` im Goal anzugehen.                          |
+| *7ᶜ*  | `rcases h with ⟨x, hx⟩`   | Um ein `∃` in den Annahmen zu zerlegen.                |
+| *8ᵇ*  | `intro`                   | Um ein `∀` im Goal anzugehen.                          |
+| 15    | `push_neg`                | Für `¬∃` und `¬∀` im Goal.                             |
+
+Als Abschlussübung kannst du folgende Äquivalenz zeigen:
+
+"
+
+Statement
+    "TODO":
+    True := by
+  trivial
+
+Conclusion ""
+
+Tactics push_neg intro use rw unfold ring
+
+Lemmas even odd not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Prime.lean b/server/testgame/TestGame/Levels/Prime.lean
new file mode 100644
index 0000000..7152735
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Prime.lean
@@ -0,0 +1 @@
+import TestGame.Levels.Prime.L01_Prime
diff --git a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
new file mode 100644
index 0000000..e69de29
diff --git a/server/testgame/TestGame/Levels/Proving/L01_Contra.lean b/server/testgame/TestGame/Levels/Proving/L01_Contra.lean
index c70e3b3..e4807e3 100644
--- a/server/testgame/TestGame/Levels/Proving/L01_Contra.lean
+++ b/server/testgame/TestGame/Levels/Proving/L01_Contra.lean
@@ -14,10 +14,24 @@ Level 1
 Title "Ad absurdum"
 
 Introduction
-"Aber, die Aussagen müssen wirklich exakte Gegenteile sein.
+"
+In diesem Kapitel lernen wir die wichtigsten Beweistechniken kennen.
 
-Hier musst du zuerst eines der Lemmas `(not_odd : ¬ odd n ↔ even n)` oder
-`(not_even : ¬ even n ↔ odd n)` benützen, um einer der Terme umzuschreiben."
+Zuerst repetieren wir, dass man vorhandene Lemmas mit `rw` und `apply` benützen kann.
+
+
+  Aber, die Aussagen müssen wirklich exakte Gegenteile sein.
+
+Hier musst du zuerst eines der folgenden Lemmas benützen, um einer der Terme umzuschreiben.
+
+```
+lemma not_odd (n : ℕ): ¬ odd n ↔ even n := by
+  ...
+
+lemma not_even (n : ℕ): ¬ even n ↔ odd n := by
+  ...
+```
+"
 
 Statement
     "Sei $n$ eine natürliche Zahl die sowohl gerade wie auch ungerade ist.