levels.

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
 
 Game "TestGame"
@@ -12,50 +12,7 @@ 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
-- 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?
-
+"Work in progress.
 "
 
 Conclusion
@@ -63,5 +20,5 @@ Conclusion
 
 
 Path Proposition → Implication → Predicate → Contradiction
-Path Predicate → Prime
+--Path Predicate → Prime
 Path Predicate → Induction

server/testgame/TestGame/Levels/Induction/L01_Simp.lean

@@ -19,9 +19,9 @@ 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 …$
+Der Syntax für  $\\sum_{i=0}^n a_i$ (\\sum) ist `∑ i : Fin n, …`
 
-Als kann die Taktik `simp` (für \"simplification\") ganz viel Triviales vereinfachen.
+Als erstes 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.
 
@@ -30,15 +30,15 @@ Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
 ```
 @[simp]
 lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
-  [...]
+  sorry
 ```
 
 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
+"Zeige dass $\\sum_{i = 0} ^ {n-1} (0 + 0) = 0$."
+    (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
   simp
 
 Tactics simp

server/testgame/TestGame/Levels/Induction/L02_Sum.lean

@@ -17,8 +17,12 @@ Jetzt wollen wir ein paar Lemmas zu Summen kennenlernen, die `simp` nicht automa
 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$
+`rw [Finset.sum_add_distrib]` als zwei Summen $\\sum_{i = 0}^n a_i + \\sum_{j = 0}^n b_j$
 auseinandernehmen.
+
+Insbesondere ist auch zu beachten, dass der Index `i` keine natürliche Zahl ist, sondern
+vom Typ `Fin n`, das heisst, man muss diesen eigentlich immer mit `(i : ℕ)`
+als natürliche Zahl verwenden.
 "
 
 Statement

server/testgame/TestGame/Levels/Induction/L03_Induction.lean

@@ -30,7 +30,7 @@ Für den Induktionsschritt braucht man fast immer zwei technische Lemmas:
 -- 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}$."
+"Zeige $\\sum_{i = 0}^n i = \\frac{n \\cdot (n + 1)}{2}$."
   (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
   induction n
   simp