Merge branch 'main' of github.com:hhu-adam/lean4game

client/src/components/LeftPanel.tsx

@@ -77,7 +77,7 @@ function LeftPanel({ spells, inventory, showSidePanel, setShowSidePanel }) {
           <ListItemIcon sx={{minWidth: 0, mr: open ? 3 : 'auto', justifyContent: 'center' }}>
             <FontAwesomeIcon icon={faHammer}></FontAwesomeIcon>
           </ListItemIcon>
-          <ListItemText primary="Tactics" sx={{ display: showSidePanel ? null : "none" }} />
+          <ListItemText primary="Known Tactics" sx={{ display: showSidePanel ? null : "none" }} />
         </ListItemButton>
         {spells && spells.length > 0 &&
           <Paper sx={{ px: 2, py: 1, display: showSidePanel ? null : "none" }} elevation={0} >
@@ -89,7 +89,7 @@ function LeftPanel({ spells, inventory, showSidePanel, setShowSidePanel }) {
           <ListItemIcon sx={{minWidth: 0, mr: open ? 3 : 'auto', justifyContent: 'center' }}>
             <FontAwesomeIcon icon={faBook}></FontAwesomeIcon>
           </ListItemIcon>
-          <ListItemText primary="Lemmas" sx={{ display: showSidePanel ? null : "none" }} />
+          <ListItemText primary="Known Lemmas" sx={{ display: showSidePanel ? null : "none" }} />
         </ListItemButton>
         {inventory && inventory.length > 0 &&
           <Paper sx={{ px: 2, py: 1, mt: 2, display: showSidePanel ? null : "none" }} elevation={0} >

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 &&
         <FormControlLabel
           control={<Switch checked={showHints} onChange={handleHintsChange} />}
-          label="Help"
+          label="More Help?"
         />}
-        {hints.map((hint) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint.message}</ReactMarkdown></MathJax></Alert></Collapse>)}
+        {hints.map((hint) => <Collapse in={showHints}><Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint.message}</ReactMarkdown></MathJax></Alert></Collapse>)}
     </Box>)
 }
 
+/* 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 (
+    <Accordion>
+      <AccordionSummary expandIcon={<ExpandMoreIcon />}>
+        <Typography color="primary" sx={{ ml: 0 }}>⊢ {goal.goal}</Typography>
+      </AccordionSummary>
+      <AccordionDetails sx={{ backgroundColor: "aliceblue" }}>
+        {hasObject &&
+          <Box>
+            <Typography>Objects</Typography>
+            <List>
+              {goal.objects.map((item) =>
+                <ListItem key={item.userName}>
+                  <Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
+                  <Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
+                </ListItem>)}
+            </List>
+          </Box>}
+        {hasAssumption &&
+          <Box>
+            <Typography>Assumptions</Typography>
+            <List>
+              {goal.assumptions.map((item) =>
+                <ListItem key={item}>
+                  <Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
+                  <Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
+                </ListItem>)}
+            </List>
+          </Box>}
+        <Typography>Prove:</Typography>
+        <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
+      </AccordionDetails>
+    </Accordion>)
+}
+
 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 (
     <Box sx={{ height: "100%" }}>
-      {goals === null && <Typography variant="h6">No goals at cursor position</Typography>}
-      {hasGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5">Main goal at cursor</Typography> <Goal goal={goals[0]} /></Paper>}
+      {hasGoal &&
+        <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
+          <Typography variant="h5">Main Goal
+            (at <FontAwesomeIcon icon={faArrowPointer}></FontAwesomeIcon>)
+          </Typography>
+          <Goal goal={goals[0]} />
+        </Paper>}
+      {!(hasGoal || completed) &&
+        <Typography variant="h6">
+          No goals
+          (at <FontAwesomeIcon icon={faArrowPointer}></FontAwesomeIcon>)
+        </Typography>}
       {completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
-      {hasError && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
-        {diagnostics.map(({severity, message}) => <Typography color={{1: "red", 2:"orange", 3:"blue", 4:"gray"}[severity]}>{message}</Typography>)}
+      {hasError &&
+        <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
+          <Typography variant="h5" sx={{ mb: 2 }}>Lean says</Typography>
+          {diagnostics.map(({severity, message}) =>
+            <Alert severity={{1: "error", 2:"warning", 3:"info", 4:"success"}[severity]} sx={{ mt: 1 }}>{message}</Alert>
+            // TODO: When does Lean give severity=4? Had colour `gray` before. Make custom theme for that
+          )}
         </Paper>}
       {hasManyGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, mt: 1 }}>
-        <Typography variant="h6" sx={{ mb: 2 }}>Other goals</Typography>
-        {goals.slice(1).map((goal, index) => <Paper><Goal key={index} goal={goal} /></Paper>)}
+        <Typography variant="h5" sx={{ mb: 2 }}>Further Goals</Typography>
+        {goals.slice(1).map((goal, index) => <Paper><OtherGoal key={index} goal={goal} /></Paper>)}
       </Paper>}
     </Box>
   )

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

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

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

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

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."
-
-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
+"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man tippt diese mit
 `\\1`, `\\2`, `\\3`, …"
 
-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."
+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₁]`."
 
--- 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."
+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."
+
+
+-- -- 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."

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