From 6576aa023169782b13156409fc9d5ef616ca9a22 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 24 Jan 2023 15:11:24 +0100 Subject: [PATCH] levels. --- server/testgame/TestGame.lean | 49 ++----------------- .../TestGame/Levels/Induction/L01_Simp.lean | 10 ++-- .../TestGame/Levels/Induction/L02_Sum.lean | 6 ++- .../Levels/Induction/L03_Induction.lean | 2 +- 4 files changed, 14 insertions(+), 53 deletions(-) diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index e64f995..54fdcdd 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 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 diff --git a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean index 4409f39..0abb0fa 100644 --- a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean +++ b/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 diff --git a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean index dee95ef..3c08230 100644 --- a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean +++ b/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 diff --git a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean index 7c6a034..ba5b7cf 100644 --- a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean +++ b/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