updates

2022-12-18 02:28:50 +01:00
parent ac29c83e79
commit 44b8edbec3
32 changed files with 332 additions and 121 deletions
@@ -4,6 +4,7 @@ import TestGame.Levels.Logic.L02_Rfl
 import TestGame.Levels.Logic.L03_Assumption
 import TestGame.Levels.Logic.L03b_Assumption
 import TestGame.Levels.Logic.L04_Rewrite
+import TestGame.Levels.Logic.L04b_Rewrite
 import TestGame.Levels.Logic.L05_Apply
 import TestGame.Levels.Logic.L05b_Apply
 import TestGame.Levels.Logic.L05c_Apply
@@ -32,3 +33,62 @@ import TestGame.Levels.Negation.L06_ByContra
 import TestGame.Levels.Negation.L07_Contrapose
 import TestGame.Levels.Negation.L08_Contrapose
 import TestGame.Levels.Negation.L09_PushNeg
+
+Game "TestGame"
+
+Title "Lean 4 game"
+
+Introduction
+"Work in progress. Hier sind die Kommentare, aufgeteilt in drei Kategorien
+
+### Levels / Spielinhalt
+Levels, die spielbar sind:
+
+- Logic
+- Contradiction
+
+Die anderen Levels gehen noch grössere Veränderungen durch.
+Kommentare zu den spielbaren Levels:
+
+- Taktik-Beschreibungen sind nicht gemacht, aber es sollten die richtigen
+Taktiken & Lemmas angezeigt werden
+- Noch mehr kurze Aufgaben?
+- Mehr zur Implikation `→`?
+- Ringschluss (noch nicht in Lean4)
+- `tauto` (noch nicht in Lean4). Am Anfang?
+- `trivial`: wann einführen? Ist ja ein Mix von verschiedenen Taktiken.
+- Wann führen wir `have h : f ha` ein? (ist jetzt mal in `by_contra` reingequetscht, sollte
+aber eigenständig sein)
+- Nicht erklärt, wann `rw` nur eines umschreibt und wann mehrere Male. Sollten wir das tun?
+
+### Spieler-Führung
+
+- Keine Möglichkeit zurück zu gehen und nach dem letzten Level kann man trotzdem
+\"Next Level\" klicken
+- Fehlermeldungen sind nicht besonders Benutzerfreundlich: Ganz unverständliche sammeln,
+damit wir diese später modifizieren können.
+- Kann man Taktiken blockieren?
+- Ich (J) bin kein Fan von der Autoergänzung, da diese im Moment viel unrelevantes anbietet.
+- BUG: Kann `suffices` & `have` nicht als Taktik anzeigen.
+- BUG: `¬ odd n` wird als Objekt gelistet, nicht als Assumption.
+- FEAT: Brauche ein `Message'` das nur aktiv ist, wenn keine zusätzlichen Annahmen vorhanden
+sind.
+
+
+
+
+### Benutzerinterface
+Das graphische wurde noch nicht wirklich angegangen, hier sind vorallem gröbere
+Ideen wie Seitenaufteilung hilfreich. Details werden dann aber später angegangen.
+
+- Spielstand wir noch nicht gespeichert.
+- Die Lean-Version der Aufgaben sieht rudimentär aus: Syntax highlighting?
+
+"
+
+Conclusion
+"There is nothing else so far. Thanks for rescuing natural numbers!"
+
+
+Path Logic → Nat → Contradiction
+Path Nat → Nat2
@@ -16,9 +16,11 @@ zero_add add_zero
 LemmaDoc not_not as not_not in "Logic"
 "`∀ (A : Prop), ¬¬A ↔ A`."

+LemmaDoc not_forall as not_forall in "Logic"
+"`∀ (A : Prop), ¬(∀ x, A) ↔ ∃x, (¬A)`."

-
-
+LemmaDoc not_exists as not_exists in "Logic"
+"`∀ (A : Prop), ¬(∃ x, A) ↔ ∀x, (¬A)`."

 LemmaDoc even as even in "Nat"
 "
@@ -46,4 +48,4 @@ LemmaSet natural : "Natürliche Zahlen" :=
 even odd not_odd not_even

 LemmaSet logic : "Logik" :=
-not_not
+not_not not_forall not_exists
@@ -14,8 +14,8 @@ Zum Beispiel
 \"und angenommen, dass $n$ strikt grösser als $1$ ist\".

 In Lean schreibt man beides mit dem gleichen Syntax: `(n : ℕ) (h : 1 < n)` definiert
-zuerst eine natürliche Zahl $n$ und eine Annahme dass $1 < n$ (die Annahme kriegt
-den Namen `h`).
+zuerst eine natürliche Zahl $n$ und eine Annahme dass $1 < n$ gilt
+(welche den Namen `h` kriegt).

 Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
 "
@@ -18,14 +18,14 @@ kann die Taktik `rw [h]` im Goal $X$ durch $Y$ ersetzen.
 "

 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
+"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
@@ -0,0 +1,39 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Logic"
+Level 6
+
+Title "Rewrite"
+
+Introduction
+"
+Mit `rw` kann man nicht nur das Goal sondern auch andere Annahmen umschreiben:
+
+Wenn `(h : X = Y)` ist, dann ersetzt `rw [h] at g` in der Annahme
+`g` das `X` durch `Y`.
+"
+
+Statement umschreiben
+"Angenommen man hat die Gleichheiten
+
+$$
+\\begin{aligned} a &= b \\\\ a + a ^ 2 &= b + 1 \\end{aligned}
+$$
+
+Zeige dass $b + b ^ 2 = b + 1$."
+(a b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 := by
+  rw [h] at g
+  assumption
+
+Message (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 =>
+"`rw [ ... ] at g` schreibt die Annahme `g` um."
+
+Message (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1 =>
+"Sackgasse. probiers doch mit `rw [h] at g` stattdessen."
+
+Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
+dem Goal umschreiben."
+
+Tactics assumption rw
@@ -3,32 +3,32 @@ import Mathlib

 Game "TestGame"
 World "Logic"
-Level 6
+Level 7

 Title "Implikation"

 Introduction
 "Als nächstes widmen wir uns der Implikation $A \\Rightarrow B$.
-
-Mit zwei logischen Aussagen `(A : Prop)`, `(B : Prop)` schreibt man eine Implikation
+Mit zwei logischen Aussagen `(A : Prop) (B : Prop)` schreibt man eine Implikation
 als `A → B` (`\\to`).

-Wenn man als Goal $B$ hat und eine Impikation `(g : A → B)` kann man mit `apply g` diese
-anwenden, worauf das Goal $A$ ist. Auf Papier würde man an der Stelle
-folgendes zu schreiben: \"Es genügt $A$ zu zeigen, denn $A$ impliziert $B$\".
+Wenn man als Goal $B$ beweisen möchte und eine Impikation `(g : A → B)`
+hat, kann man mit `apply g` diese
+anwenden, worauf das zu beweisende Goal $A$ wird. Auf Papier würde man an der Stelle
+folgendes zu schreiben: \"Es genügt $A$ zu zeigen, denn $A \\Rightarrow B$\".

 *Bemerke:* Das ist der selbe Pfeil, der später auch für Funktionen wie `ℕ → ℕ` gebraucht
 wird, deshalb heisst er `\\to`."


 Statement
-    "Seien $A$, $B$ logische Aussagen, wobei $A$ wahr ist und $A$ impliziert $B$.
+    "Seien $A, B$ logische Aussagen, wobei $A$ wahr ist und $A \\Rightarrow B$.
    Zeige, dass $B$ wahr ist."
    (A B : Prop) (hA : A) (g : A → B) : B := by
  apply g
  assumption

-Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
+Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : B =>
 "Mit `apply g` kannst du die Implikation `g` anwenden."

 Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
@@ -37,8 +37,8 @@ dafür hast du bereits einen Beweis in den Annahmen."

 Tactics apply assumption

-- Mathjax notes
-- `\\\\(    \\\\)` or `$   $` for inline
+-- Katex notes
+-- `\\(    \\)` or `$   $` for inline
 -- and `$$  $$` block.
 -- align block:
-- $$\\begin{aligned} 2x - 4 &= 6 \\\\\\\\ 2x &= 10 \\\\\\\\ x &= 5 \\end{aligned}$$
+-- $$\\begin{aligned} 2x - 4 &= 6 \\\\ 2x &= 10 \\\\ x &= 5 \\end{aligned}$$
@@ -2,7 +2,7 @@ import TestGame.Metadata

 Game "TestGame"
 World "Logic"
-Level 7
+Level 8

 Title "Implikation"

@@ -28,12 +28,17 @@ Statement
  apply f
  assumption

-Message  (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
+Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
+    (hA : A) (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F) : F =>
+"Versuch mit `apply` den richtigen Weg zu finden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
    (hA : A) (f : A → B) (g : C → B) (h : B → E)
    (i : D → E) (k : E → F) (m : C → F) : C =>
 "Sackgasse. Probier doch einen anderen Weg."

-Message  (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
+Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
    (hA : A) (f : A → B) (g : C → B) (h : B → E)
    (i : D → E) (k : E → F) (m : C → F) : D =>
 "Sackgasse. Probier doch einen anderen Weg."
@@ -4,7 +4,7 @@ set_option tactic.hygienic false

 Game "TestGame"
 World "Logic"
-Level 8
+Level 9

 Title "Implikation"

@@ -15,7 +15,7 @@ Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit
 "

 Statement
-    ""
+    "Angenommen man weiss $A \\Rightarrow B \\Rightarrow C$, zeige dass $A \\Rightarrow C$."
    (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
  intro hA
  apply g
@@ -23,7 +23,7 @@ Statement
  assumption

 Message (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C =>
-"mit `intro hA` kann man eine Implikation angehen."
+"Mit `intro hA` kann man eine Implikation angehen."

 Message (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
 "Jetzt ist es ein altbekanntes Spiel von `apply`-Anwendungen."
@@ -5,7 +5,7 @@ import Init.Data.ToString

 Game "TestGame"
 World "Logic"
-Level 9
+Level 10

 Title "Genau dann wenn"

@@ -2,7 +2,7 @@ import TestGame.Metadata

 Game "TestGame"
 World "Logic"
-Level 10
+Level 11

 Title "Genau dann wenn"

@@ -4,7 +4,7 @@ set_option tactic.hygienic false

 Game "TestGame"
 World "Logic"
-Level 11
+Level 12

 Title "Genau dann wenn"

@@ -4,7 +4,7 @@ import Mathlib.Tactic.Cases

 Game "TestGame"
 World "Logic"
-Level 12
+Level 13

 Title "Genau dann wenn"

@@ -5,7 +5,7 @@ set_option tactic.hygienic false

 Game "TestGame"
 World "Logic"
-Level 13
+Level 14

 Title "Und"

@@ -6,7 +6,7 @@ import Mathlib.Tactic.LeftRight

 Game "TestGame"
 World "Logic"
-Level 14
+Level 15

 Title "Oder"

@@ -9,7 +9,7 @@ import Mathlib.Tactic.LeftRight

 Game "TestGame"
 World "Logic"
-Level 15
+Level 16

 Title "Oder - Bonus"

@@ -6,7 +6,7 @@ set_option tactic.hygienic false

 Game "TestGame"
 World "Logic"
-Level 16
+Level 17

 Title "Oder"

@@ -18,9 +18,14 @@ bereits mit `rfl` bewiesen werden können.
 Algemeinere Gleichungen mit Variablen kann man mit der Taktik `ring` lösen.
 "

-Statement "" (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
+Statement
+    "Zeige $(x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2$."
+    (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  ring

+Message (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 =>
+"`ring` übernimmt den ganzen Spaß."
+
 Conclusion
 "
 Die Taktik heisst übrigens `ring` weil sie dafür entwickelt wurde, Gleichungen in einem abstrakten
@@ -12,10 +12,19 @@ Introduction
 Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden.
 "

-Statement "" (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
+Statement
+    "Angenommen, man hat die Gleichung $x = 2 * y + 1$, zeige
+    $x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y$.  "
+    (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
  rw [h]
  ring

+Message (x : ℕ) (y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
+  "Die Annahme `h` kannst du mit `rw [h]` benützen."
+
+Message (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
+  "Jetzt kann `ring` übernehmen."
+
 Conclusion ""

-Tactics ring
+Tactics ring rw
@@ -33,15 +33,15 @@ Hierzu gibt es 3 wichtige Taktiken:
   soll. Das macht man mit `use y`
 "

-Statement even_square "" (n : ℕ) (h : even n) : even (n ^ 2) := by
+Statement even_square
+      "Wenn $n$ gerade ist, dann ist $n^2$ gerade."
+      (n : ℕ) (h : even n) : even (n ^ 2) := by
  unfold even at *
  rcases h with ⟨x, hx⟩
  use 2 * x ^ 2
  rw [hx]
  ring

-- TODO: Server PANIC because of the `even`.
--
 Message (n : ℕ) (h : even n) : even (n ^ 2) =>
 "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
 `unfold even at *` ersetzen.
@@ -68,3 +68,4 @@ Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^
 "Die Taktik `ring` löst solche Gleichungen."

 Tactics unfold rcases use rw ring
+Lemmas even odd
@@ -19,7 +19,9 @@ Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
 Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
 "

-Statement "" : ∀ (x : ℕ), (even x) → odd (1 + x) := by
+Statement
+    " Für alle natürlichen Zahlen $x$ gilt, falls $x$ gerade ist, dann ist $x + 1$
+    ungerade." : ∀ (x : ℕ), (even x) → odd (1 + x) := by
  intro x h
  unfold even at h
  unfold odd
@@ -22,8 +22,13 @@ Der einfachste Widerspruch ist wenn man einen Beweis von `False` hat:
 "

 Statement
-    "Ein Widerspruch impliziert alles."
+    "Sei $A$ eine Aussage und angenommen man hat einen Beweis für `False`.
+    Zeige, dass daraus $A$ folgt."
    (A : Prop) (h : False) : A := by
  contradiction

+Message (A : Prop) (h : False) : A =>
+"Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen,
+unabhängig davon, was das Goal ist."
+
 Tactics contradiction
@@ -16,9 +16,10 @@ Introduction
 also `(h : A)` und `(g : ¬ A)`. (`\\not`)
 "

-Statement
-    "Ein Widerspruch impliziert alles."
-    (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 128 := by
+Statement absurd
+    "Sei $n$ eine natürliche Zahl die sowohl gerade wie auch nicht gerade ist.
+    Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)"
+    (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 42 := by
  contradiction

 Conclusion
@@ -14,28 +14,24 @@ Level 3
 Title "Ad absurdum"

 Introduction
-"
-Aber, die Aussagen müssen wirklich exakte Gegenteile sein.
+"Aber, die Aussagen müssen wirklich exakte Gegenteile sein.

-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.
-"
+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."

 Statement
-    "Ein Widerspruch impliziert alles."
-    (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
-  rw [← not_even] at h₂
+    "Sei $n$ eine natürliche Zahl die sowohl gerade wie auch ungerade ist.
+    Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)."
+    (n : ℕ) (h_even : even n) (h_odd : odd n) : n = 42 := by
+  rw [← not_even] at h_odd
  contradiction

-Message (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 =>
-"Schreibe zuerst eine der Aussagen mit `rw [←not_even] at h₂` um, damit diese genaue
-Gegenteile sind."
+Message (n : ℕ) (h_even : even n) (h_odd : odd n) : n = 42 =>
+"Schreibe zuerst eine der Aussagen mit `rw [←not_even] at h_odd` um, damit diese genaue
+Gegenteile werden."

-Conclusion
-"
-Detail: `¬ A` ist übrigens als `A → false` implementiert, was aussagt, dass
-\"falls `A` wahr ist, impliziert das `false` und damit einen Widerspruch\".
-"
-- TODO: Oder doch ganz entfernen?
+Conclusion ""

-Tactics contradiction
+Tactics contradiction rw
+
+Lemmas even odd not_even not_odd
@@ -11,21 +11,25 @@ Title "Ad absurdum"
 Introduction
 "
 Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form
-`A = B` hat, wo Lean weiss, dass `A und `B` unterschiedlich sind, z.B. `0 = 1` in `ℕ`
-oder auch Annahmen der Form `A ≠ A` (`\\ne`).
+`A ≠ A` (`\\ne`) hat, oder Aussagen der Form
+`A = B` hat, wo Lean weiss, dass `A` und `B` unterschiedlich sind, wie zum Beispiel `0 = 1` in `ℕ`.
+
+*Bemerkung:* `X ≠ Y` muss man als `¬ (X = Y)` lesen, und auch so behandeln.
 "

 Statement
-    "Ein Widerspruch impliziert alles."
+    "Angenommen man hat $a = b = c$ und $a \\ne c$ natürliche Zahlen $a, b, c$.
+    Zeige, dass man daraus jede beliebige Aussage beweisen kann."
    (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by
  rw [g₁] at h
  contradiction

 Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A =>
-  "Recap: `rw [...] at h` hilft dir hier."
+  "Benütze `rw [...] at ...` um zwei Aussagen zu bekommen die genau das Gegenteil
+  aussagen."

-Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : b ≠ c) : A =>
-  "`b ≠ c` muss man als `¬ (b = c)` lesen. Deshalb findet `contradiction` hier direkt
+Hint (A : Prop) (a : ℕ) (b : ℕ) (g₁ : a = b) (h : a ≠ b) : A =>
+  "`X ≠ Y` muss man als `¬ (X = Y)` lesen. Deshalb findet `contradiction` hier direkt
  einen Widerspruch."

 Tactics contradiction
@@ -11,14 +11,23 @@ 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.
+`¬ (¬ 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]

-Tactics rw
+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
@@ -14,35 +14,68 @@ Title "Widerspruch"

 Introduction
 "
+Zwei wichtige Beweisformen sind per Widerspruch und per Kontraposition. Hier
+schauen wir beide an und auch den Unterschied.
+
 Um einen Beweis per Widerspruch zu führen, kann man mit `by_contra h` annehmen,
 dass das Gegenteil des Goals wahr sei, und dann einen Widerspruch erzeugen.
+
+**Bemerkung:** Besonders beim Beweis durch Widerspruch ist es hilfreich, wenn man
+Zwischenresultate erstellen kann.
+`suffices h₁ : ¬(odd (n ^ 2))` erstellt zwei neue Goals:
+
+1) Ein Beweis, wieso es genügt `¬(odd (n ^ 2))` zu zeigen (\"weil das einen Widerspruch zu
+`h` bewirkt\").
+2) Einen Beweis des Zwischenresultats `suffices h₁ : ¬(odd (n ^ 2))`
+
+Alternativ macht `have h₁ : ¬(odd (n ^ 2))` genau das gleiche, vertauscht aber die
+Beweise (1) und (2), so dass man zuerst `h₁` beweist, und dann den eigentlichen Beweis
+fortsetzt.
 "

 Statement
    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
    (n : ℕ) (h : odd (n ^ 2)) : odd n := by
  by_contra g
+  suffices d : ¬ odd (n ^ 2) -- TODO: I don't like this
+  contradiction
+
  rw [not_odd] at g
-
-  suffices ¬ odd (n ^ 2) by contradiction -- TODO: I don't like this
-
  rw [not_odd]
  apply even_square
  assumption

-Message : false =>
-"Es gibt mehrere Möglichkeiten, wie man nach einem `by_contra` weitergeht.
+Message (n : ℕ) (h : odd (n^2)) : odd n =>
+"Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten."

-Hier wollen wir einen Widerspruch zu `h` machen. Wir machen das mit
-`suffices ¬ odd (n ^ 2) by contradiction`, worauf man dann nur noch `¬ odd (n ^ 2)`
-zeigen muss."
+Message (n : ℕ) (g : ¬ odd n) (h : odd (n^2)) : False =>
+"Nun *genügt es zu zeigen, dass* `¬odd (n ^ 2)` wahr ist,
+denn dann erhalten wir einen Widerspruch zu `h`.

-Hint (n : ℕ) : ¬ (odd (n ^ 2)) =>
-"Das Lemma `not_odd` ist hilfreich."
+Benütze dafür `suffices h₂ : ¬odd (n ^ 2)`.
+"
+
+Message (n : ℕ) (g : ¬ odd (n^2)) (h : odd (n^2)) : False =>
+"Hier musst du rechtfertigen, wieso das genügt. In unserem Fall, weil
+dadurch einen Widerspruch entsteht."
+
+Hint (n : ℕ) (g : ¬ odd (n^2)) (h : odd (n^2)) : False =>
+"Also `contradiction`..."
+
+Message (n : ℕ) (g : ¬ odd n) (h : odd (n^2)) : ¬ odd (n^2) =>
+"Das Zwischenresultat `¬odd (n^2)` muss auch bewiesen werden.
+Hier ist wieder das Lemma `not_odd` hilfreich."
+
+Hint (n : ℕ) (g : ¬ odd n) (h : odd (n^2)) : even (n^2) =>
+"Mit `rw [not_odd] at *` kannst du im Goal und allen Annahmen gleichzeitig umschreiben."

 Message (n: ℕ) (h : odd (n ^ 2)) (g : even n) : even (n ^ 2) =>
-"Das haben wir schon gezeigt. Mit `apply even_square` kannst du das Lemma anwenden."
+"Diese Aussage hast du bereits als Lemma bewiesen."

-Tactics contradiction by_contra rw apply assumption -- TODO: suffices
+Hint (n: ℕ) (h : odd (n ^ 2)) (g : even n) : even (n ^ 2) =>
+"Probiers mit `apply ...`"
+
+
+Tactics contradiction by_contra rw apply assumption -- TODO: suffices, have

 Lemmas odd even not_odd not_even even_square
@@ -29,5 +29,22 @@ Statement
  rw [not_odd]
  apply even_square

+Message (n : ℕ) (h : odd (n ^ 2)) : odd n =>
+"`intro` wär generell ein guter Ansatz! Aber hier wollen wir `contrapose` benützen, was eine
+Implikation benötigt, deshalb ist `intro` hier der falsche Weg!"
+
+
+Message (n : ℕ) : odd (n ^ 2) → odd n =>
+"Mit `contrapose` kann man die Implikation zu
+`¬ (even n) → ¬ (even n^2)` umkehren."
+
+Hint (n : ℕ) : ¬odd n → ¬odd (n ^ 2) => "Du kennst bereits ein Lemma um `¬ odd ...` mit `rw`
+umzuschreiben"
+
+Message (n : ℕ) : even n → ¬odd (n ^ 2) => "rw [not_odd] muss hier zweimal angewendet werden,
+da rw das erste Mal `not_odd n` gebraucht hat und das zweite Mal `not_odd (n^2)` benützt."
+
+Message (n : ℕ) : even n → even (n ^ 2) => "Diese Aussage hast du bereits als Lemma bewiesen."
+
 Tactics contrapose rw apply
 Lemmas even odd not_even not_odd even_square
@@ -13,20 +13,25 @@ Level 8
 Title "Kontraposition"

 Introduction
-"
-Lean Trick: Wenn das Goal nicht bereits eine Implikation ist, sondern man eine Annahme `h` hat, die
+"**Lean Trick:** Wenn das Goal nicht bereits eine Implikation ist, sondern man eine Annahme `h` hat, die
 Man gerne für die Kontraposition benützen würde, kann man mit `revert h` diese als
 Implikationsannahme ins Goal schreiben.
 "

 Statement
    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
-    (n : ℕ) (h : odd (n ^ 2)): odd n := by
+    (n : ℕ) (h : odd (n ^ 2)) : odd n := by
  revert h
  contrapose
  rw [not_odd]
  rw [not_odd]
  apply even_square

+Hint (n : ℕ) (h : odd (n ^ 2)) : odd n =>
+"Benutze `revert h` um das Goal in eine Implikation umzuschreiben."
+
+Message (n : ℕ) : odd (n ^ 2) → odd n =>
+"Jetzt ist es genau das gleiche wie bei der letzten Aufgabe."
+
 Tactics contrapose rw apply revert
 Lemmas even odd not_even not_odd even_square
@@ -14,23 +14,53 @@ Introduction
 "
 Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
 mit `push_neg` das `¬` durch den Quantor hindurchschieben.
+
+Das braucht intern die Lemmas
+
+- `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
+- `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
+
+(welche man auch mit `rw` explizit benutzen könnte.)
 "

 Statement
-    "Es existiert keine natürliche Zahl, die grösser als alle anderen.":
+    "Es existiert keine natürliche Zahl $n$, sodass $n + k$ immer ungerade ist.":
    ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
  push_neg
  intro n
-  use 3*n + 6
+  use n
  rw [not_odd]
  unfold even
-  use 2*n + 3
+  use n
  ring

-Message (n : ℕ) : (Exists fun k ↦ ¬odd (n + k)) =>
-"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutz `use ...`
+Message : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) =>
+"`push_neg` schiebt die Negierung an den Quantoren vorbei."
+
+
+Message (n : ℕ) : (∃ k, ¬odd (n + k)) =>
+"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutze `use`
 mit der richtigen Zahl."

+
+Hint (n : ℕ) : ¬odd (n + n) =>
+"Du kennst ein Lemma um mit `¬odd` umzugehen."
+
+-- Hint (n : ℕ) (k : ℕ) : ¬odd (n + k) =>
+-- "Du kennst ein Lemma um mit `¬odd` umzugehen."
+
+Hint (n : ℕ) : even (n + n) =>
+"`unfold even` hilft, anzuschauen, was hinter `even` steckt.
+
+Danach musst du wieder mit `use r` ein `(r : ℕ)` angeben, dass du benützen möchtest."
+
+-- Hint (n : ℕ) (k : ℕ) : even (n + k) =>
+-- "`unfold even` hilft hier weiter."
+
+Message (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
+
 Conclusion ""

 Tactics push_neg intro use rw unfold ring
+
+Lemmas even odd not_even not_odd not_exists not_forall
@@ -2,24 +2,3 @@ import GameServer.Commands
 import TestGame.TacticDocs
 import TestGame.LemmaDocs
 import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ.
-
-Game "TestGame"
-
-Title "The Natural Number Game"
-
-Introduction
-"This is a sad day for mathematics. While trying to find glorious new foundations for mathematics,
-someone removed the law of excluded middle and the axiom of choice. Unsurprisingly,
-everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage
-but now we need to rebuild all of mathematics from scratch.
-
-As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from
-the axioms that Giuseppe Peano found under the collapsed tower of number theory. You've been equipped
-with a level 1 spell book. Good luck."
-
-Conclusion
-"There is nothing else so far. Thanks for rescuing natural numbers!"
-
-
-Path Logic → Nat → Contradiction
-Path Nat → Nat2