diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx index 85662f5..b43b011 100644 --- a/client/src/components/LeftPanel.tsx +++ b/client/src/components/LeftPanel.tsx @@ -77,7 +77,7 @@ function LeftPanel({ spells, inventory, showSidePanel, setShowSidePanel }) { - + {spells && spells.length > 0 && @@ -89,7 +89,7 @@ function LeftPanel({ spells, inventory, showSidePanel, setShowSidePanel }) { - + {inventory && inventory.length > 0 && diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx index 3807fd3..086e530 100644 --- a/client/src/components/TacticState.tsx +++ b/client/src/components/TacticState.tsx @@ -9,6 +9,11 @@ import { MathJax } from "better-react-mathjax"; import List from '@mui/material/List'; import ListItem from '@mui/material/ListItem'; import { Paper, Box, Typography, Alert, FormControlLabel, FormGroup, Switch, Collapse } from '@mui/material'; +import { Accordion, AccordionSummary, AccordionDetails, Divider } from '@mui/material'; +import ExpandMoreIcon from '@mui/icons-material/ExpandMore'; + +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faArrowPointer } from '@fortawesome/free-solid-svg-icons' // TODO: Dead variables (x✝) are not displayed correctly. @@ -46,27 +51,82 @@ function Goal({ goal }) { {hasHints && } - label="Help" + label="More Help?" />} - {hints.map((hint) => {hint.message})} + {hints.map((hint) => {hint.message})} ) } +/* Function to display a goal that is not the main goal. */ +function OtherGoal({ goal }) { + + const hasObject = typeof goal.objects === "object" && goal.objects.length > 0 + const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0 + + return ( + + }> + ⊢ {goal.goal} + + + {hasObject && + + Objects + + {goal.objects.map((item) => + + {item.userName} : + {item.type} + )} + + } + {hasAssumption && + + Assumptions + + {goal.assumptions.map((item) => + + {item.userName} : + {item.type} + )} + + } + Prove: + {goal.goal} + + ) +} + function TacticState({ goals, diagnostics, completed }) { const hasError = typeof diagnostics === "object" && diagnostics.length > 0 const hasGoal = goals !== null && goals.length > 0 const hasManyGoal = hasGoal && goals.length > 1 return ( - {goals === null && No goals at cursor position} - {hasGoal && Main goal at cursor } + {hasGoal && + + Main Goal + (at ) + + + } + {!(hasGoal || completed) && + + No goals + (at ) + } {completed && Level completed ! 🎉} - {hasError && - {diagnostics.map(({severity, message}) => {message})} + {hasError && + + Lean says + {diagnostics.map(({severity, message}) => + {message} + // TODO: When does Lean give severity=4? Had colour `gray` before. Make custom theme for that + )} } {hasManyGoal && - Other goals - {goals.slice(1).map((goal, index) => )} + Further Goals + {goals.slice(1).map((goal, index) => )} } ) diff --git a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean index 91655db..ed9f7c5 100644 --- a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean @@ -11,23 +11,30 @@ Introduction Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer unterstützt und verifiziert schreiben kann. -Ein Beweis besteht in Lean aus verschiedenen **Taktiken**, welche ungefähr einem -logischen Schritt entsprechen, den man auf Papier aufschreiben würde. - -Rechts im **Infoview** siehst den Status des aktuellen Beweis. -Du siehst ein oder mehrere offene **Goals** (mit einem `⊢` davor), die du noch zeigen musst. -Wenn du eine Taktik hinschreibst, dann versucht Lean diesen Schritt beim -ersten offenen Goal zu machen. -Wenn der Beweis komplett ist, erscheint \"goals accomplished\". +*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am Beweisen +bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals** +aufgelistet, diese musst du dann später auch noch zeigen. + +Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie +man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen, +andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der +Seite. + +Wenn der Beweis komplett ist, erscheint \"Level Completed! 🎉\". + +Deine erste Taktik ist `rfl`, welche dazu da ist, ein Goal der Form `X = X` zu schliessen. +Gib die Taktik ein gefolgt von Enter ⏎. " Statement "Zeige $ 42 = 42 $." : 42 = 42 := by rfl Message : 42 = 42 => -"Die erste Taktik ist `rfl`, die ein Goal von der Form `A = A` beweist." +"Die Taktik `rfl` beweist ein Goal der Form `X = X`." Hint : 42 = 42 => -"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein gefolgt von ENTER." +"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein und geh mit Enter ⏎ auf eine neue Zeile." Conclusion "Bravo!" + +Tactics rfl diff --git a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean index aa67cb4..d0240f0 100644 --- a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean @@ -8,22 +8,20 @@ Title "Definitionally equal" Introduction " -Achtung: `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich -definiert sind, auch wenn diese unterschiedlich dargestellt werden. -So sind `1 + 1` und `2` per Definition das Gleiche, da sie beide von Lean als `0.succ.succ` -gelesen werden. +**Vorsicht:** `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich +definiert sind, auch wenn diese unterschiedlich dargestellt werden. Das kann anfänglich +zu Verwirrung führen. -Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab. +So sind `2` definiert als `1 + 1`, deshalb funktioniert `rfl` auch hier. " -Statement "Zeige dass eins plus eins zwei ist." : 1 + 1 = 2 := by +Statement "Zeige dass $1 + 1$ zwei ist." : 1 + 1 = 2 := by rfl Conclusion " -Im weiteren führen die meisten anderen Taktiken `refl` automatisch am Ende aus, -deshalb musst du dieses häufig gar nicht mehr schreiben. +**Notiz:** Die meisten anderen Taktiken versuchen am Schluss automatisch `rfl` +aufzurufen, deshalb brauchst du das nur noch selten. " Tactics rfl -Lemmas zero_add diff --git a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean index b6fa2f0..cef86d2 100644 --- a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean @@ -8,13 +8,14 @@ Title "Annahmen" Introduction " -Mathematische Aussagen haben Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine -natürliche Zahl\", oder auch wahre Aussagen über diese Objekte, wie zum Beispiel +Um Aussagen zu formulieren brauchen wir Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine +natürliche Zahl\", und Annahmen über diese Objekte, von denen wir wissen, dass sie wahr sind. +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 `n` als natürliche Zahl und kreeirt eien Annahme, dass `1 < n`. Dieser Annahme geben wir -den Namen `h`. +zuerst eine natürliche Zahl `n` und eine Annahme dass `1 < n` (die Annahme kriegt +den Namen `h`). Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen. " @@ -24,6 +25,9 @@ Statement triviale_angelegenheit (n : ℕ) (h : 1 < n) : 1 < n := by assumption +Message (n : ℕ) (h : 1 < n) : 1 < n => + "`assumption` sucht nach einer Annahme, die dem Goal entspricht." + Conclusion "" Tactics assumption diff --git a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean index d693c49..21ad625 100644 --- a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean +++ b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean @@ -9,18 +9,22 @@ Title "Logische Aussagen: `Prop`" Introduction " -Eine allgemeine logische Aussage definiert man mit `(A : Prop)`. Damit sagt man noch nicht, -ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man an, dass -`A` wahr ist: `hA` ist ein Beweis der Aussage `A`. +Eine allgemeine logische Aussage definiert man mit `(A : Prop)`. + +Damit sagt man noch nicht, ob die Aussage `A` wahr oder falsch ist. +Mit einer Annahme `(hA : A)` nimmt man an, dass `A` wahr ist: +`hA` ist sozusagen ein Beweis von `A`. " --- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben? Statement mehr_triviales "Sei $ A $ eine logische Aussage und sei `hA` ein Beweis für $A$. Zeige, dass $ A $ wahr ist." (A : Prop) (hA : A) : A := by assumption +Hint (A : Prop) (hA : A) : A => +"Auch hier kann `assumption` den Beweis von `A` finden." + Conclusion "" Tactics assumption diff --git a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean index e5cce32..62138d5 100644 --- a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean +++ b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean @@ -12,39 +12,41 @@ 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 die sagt, dass `X` und `Y` gleich sind, -kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal -das eine durch das andere zu ersetzen. +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 - `a = b`, `a = d`, `c = d`. - Zeige dass `b = c`. - " + "Angenommen man hat die Gleichheiten + $a = b$, $a = d$, $c = d$. + 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 --- Gleich am Anfang anzeigen. Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c => -"Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste -`c` im Goal mit `d` ersetzen." +"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 => -"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man schreibt diese mit -`\\1`, `\\2`, `\\3`, …" +"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 => -"Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses -`(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen." +" 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." + --- TODO: Muss ich das wirklich mehrmals auflisten? -Message (x : ℕ) : x = x => -"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht, -anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen." +-- -- TODO: Muss ich das wirklich mehrmals auflisten? +-- Message (x : ℕ) : x = x => +-- "Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht, +-- anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen." Conclusion "Übrigens, mit `rw [h₁] at h₂` kann man auch eine andere Annahme umschreiben anstatt dem Goal." diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean index 8291fae..bf37e6a 100644 --- a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean @@ -8,7 +8,9 @@ Level 6 Title "Implikation" Introduction -" +"Als nächstes widmen wir uns der Implikation &A \\Rightarrow B&. TODO + +Logische Aussagen `(A : Prop)`, `(B : Prop)` Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der Aussage `A`. @@ -18,8 +20,7 @@ Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Z Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man diese mit `apply h` anwenden. -Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\". -" +Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\"." Statement "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`. @@ -32,5 +33,4 @@ Message (A : Prop) (B : Prop) (hA : A) (g : A → B) : A => "Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch `A` zeigen, dafür hast du bereits einen Beweis in den Annahmen." -Tactics apply -Tactics assumption +Tactics apply assumption