merge addition of Lemma statements

2022-12-12 20:54:31 +01:00
parent b2727eef89
commit 46848d8a93
43 changed files with 113 additions and 64 deletions
@@ -58,8 +58,11 @@ function Level() {
        <div ref={messagePanelRef} className="message-panel">
          <MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
        </div>
-        <div ref={codeviewRef} className="codeview">
-        </div>
+        <p><b>Aufgabe:</b></p>
+        <div><MathJax><ReactMarkdown>{level?.data?.descrText}</ReactMarkdown></MathJax></div>
+        <div className="statement"><code>{level?.data?.descrFormat}</code></div>
+          {/*NOTE(TODO): currently this looks bad, so I disabled it. Maybe have a drop-down for it of Syntax highlighting... */}
+        <div ref={codeviewRef} className="codeview"></div>
      </Grid>
      <Grid xs={4} className="info-panel">

@@ -42,11 +42,12 @@ function Goal({ goal }) {
      <Typography>Prove:</Typography>
      <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
      {goal.messages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
-      <FormControlLabel
-        control={<Switch checked={showHints} onChange={handleHintsChange} />}
-        label="Help"
-      />
-      {goal.hints.map((message) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert></Collapse>)}
+      {hasHints &&
+        <FormControlLabel
+          control={<Switch checked={showHints} onChange={handleHintsChange} />}
+          label="Help"
+        />}
+        {goal.hints.map((hint) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint}</ReactMarkdown></MathJax></Alert></Collapse>)}
    </Box>)
 }

@@ -92,7 +92,7 @@ function Welcome() {
        </Typography>
      </Box>
      <Box textAlign='center' sx={{ m: 5 }}>
-        <Button component={RouterLink} to="/world/TestWorld/level/1" variant="contained">Start rescue mission</Button>
+        <Button component={RouterLink} to="/world/Logic/level/1" variant="contained">Start rescue mission</Button>
      </Box>
      <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
    </div>
@@ -14,7 +14,9 @@ interface LevelInfo {
  introduction: null|string,
  index: number,
  tactics: any[],
-  lemmas: any[]
+  lemmas: any[],
+  descrText: null|string,
+  descrFormat: null|string,
 }

 const customBaseQuery = async (
@@ -46,13 +46,47 @@ elab "Introduction" t:str : command => do
  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}

-/-- Define the statement of the current level. -/
-elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
+-- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
+-- us highlighting on the client side.
+partial def reprintCore : Syntax → Option Format
+  | Syntax.missing => none
+  | Syntax.atom _ val => val.trim
+  | Syntax.ident _ rawVal _ _ => rawVal.toString
+  | Syntax.node _ kind args =>
+    match args.toList.filterMap reprintCore with
+    | [] => none
+    | [arg] => arg
+    | args => Format.group <| Format.nest 2 <| Format.joinSep args " "
+
+def reprint (stx : Syntax) : Format :=
+  reprintCore stx |>.getD ""
+
+-- macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
+
+/-- Define the statement of the current level.
+
+Arguments:
+- ident: (Optional) The name of the statemtent.
+- descr: The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
+-/
+elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : command => do
+
  let lvlIdx ← getCurLevelIdx
-  let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String)
-  elabCommand (← `(theorem $(mkIdent declName) $sig $val))
-  modifyCurLevel fun level => pure {level with goal := sig}
-- TODO: Do something with the lemma name.
+  let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
+    ("level" ++ toString lvlIdx : String)
+  let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
+  -- let thmStatement' ← match statementName with
+  -- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
+  -- | some name => `(lemma $name $sig $val)
+
+  elabCommand thmStatement
+  modifyCurLevel fun level => pure {level with
+    goal := sig,
+    descrText := descr.getString,
+    descrFormat := match statementName with
+    | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
+    | some name => (Format.join ["lemma ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10  -- "lemma "  ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
+  } -- Format.pretty <| format thmStatement.raw }

 /-- Define the conclusion of the current game or current level if some
 building a level. -/
@@ -182,6 +182,16 @@ deriving Inhabited
 def getCurLevelId [MonadError m] : m LevelId := do
  return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}

+/--
+
+
+Fields:
+- TODO
+- introduction: Theory block shown all the time.
+- description:  The mathematical statemtent in mathematician-readable form.
+- goal:         The statement in Lean.
+- conclusion:   Displayed when level is completed.
+-/
 structure GameLevel where
  index: Nat
  title: String := default
@@ -191,6 +201,8 @@ structure GameLevel where
  lemmas: Array LemmaDocEntry := default
  messages: Array GoalMessageEntry := default
  goal : TSyntax `Lean.Parser.Command.declSig := default
+  descrText: String := default
+  descrFormat : String := default
  deriving Inhabited, Repr

 /-! ## World -/
@@ -35,6 +35,8 @@ structure LevelInfo where
  tactics: Array TacticDocEntry
  lemmas: Array LemmaDocEntry
  introduction : String
+  descrText : String := ""
+  descrFormat : String := ""
 deriving ToJson

 structure LoadLevelParams where
@@ -62,6 +64,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
            title := lvl.title,
            tactics := lvl.tactics,
            lemmas := lvl.lemmas,
+            descrText := lvl.descrText,
+            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
            introduction := lvl.introduction }
      c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
      return true
@@ -24,8 +24,8 @@ structure GameGoal where
 deriving FromJson, ToJson


-def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String)
-    (hints : Array String) : MetaM GameGoal := do
+def Lean.MVarId.toGameGoal (goal : MVarId)
+    (messages : Array String) (hints : Array String) : MetaM GameGoal := do
 match (← getMCtx).findDecl? goal with
 | none          => throwError "unknown goal"
 | some mvarDecl => do
@@ -20,7 +20,7 @@ After closing this message, type rfl in the invocation zone and hit Enter or cli
 the \"Cast spell\" button.
 "

-Statement (x y z : ℕ) :  x * y + z = x * y + z := by
+Statement "" (x y z : ℕ) :  x * y + z = x * y + z := by
 rfl

 Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button."
@@ -26,7 +26,7 @@ this substitution using the `rewrite` spell. This spell takes a list of equaliti
 or equivalences so you can cast `rewrite [h]`.
 "

-Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
+Statement "" (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
  rewrite [h]
  rfl

@@ -56,7 +56,7 @@ the *right* hand side. Try and figure out how the goal will change, and
 then try it.
 "

-Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by
+Statement "" (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by
  rewrite [h]
  rfl

@@ -43,7 +43,7 @@ Observe that the goal mentions `... + succ ...`. So type
 and hit enter; see the goal change.
 "

-Statement (a : ℕ ) : a + succ 0 = succ a := by
+Statement "" (a : ℕ ) : a + succ 0 = succ a := by
  rewrite [add_succ]
  rewrite [add_zero]
  rfl
@@ -64,7 +64,7 @@ The names of the proofs tell you what the theorems are. Anyway, let's prove `0 +
 Start by casting `induction_on n`.
 "

-Statement (n : ℕ) : 0 + n = n := by
+Statement "" (n : ℕ) : 0 + n = n := by
  sorry
  -- induction_on n
  -- rewrite [add_zero]
@@ -21,7 +21,7 @@ ersten offenen Goal zu machen.
 Wenn der Beweis komplett ist, erscheint \"goals accomplished\".
 "

-Statement "Zeige `42 = 42`." : 42 = 42 := by
+Statement "Zeige $ 42 = 42 $." : 42 = 42 := by
  rfl

 Message : 42 = 42 =>
@@ -16,10 +16,8 @@ ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man

 -- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
 Statement mehr_triviales
-    "
-    Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`.
-    Zeige, dass `A` wahr ist.
-    "
+    "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

@@ -22,10 +22,8 @@ Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `
 "

 Statement
-    "
-    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
-    Zeige, dass `B` wahr ist.
-    "
+    "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist."
    (A B : Prop) (hA : A) (g : A → B) : B := by
  apply g
  assumption
@@ -18,10 +18,8 @@ Beweise Aussage `F`.
 "

 Statement
-    "
-    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
-    Zeige, dass `B` wahr ist.
-    "
+    "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist."
    (A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E)
     (i : D → E) (k : E → F) (m : C → F) : F := by
  apply k
@@ -16,6 +16,7 @@ und das Goal wird zu `B`.
 "

 Statement
+    ""
    (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
  intro hA
  apply g
@@ -21,9 +21,7 @@ Gleichungen von natürlichen Zahlen.
 "

 Statement
-    "
-    Zeige dass `B ↔ C`.
-    "
+    "Zeige dass `B ↔ C`."
    (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
  rw [h₁]
  rw [←h₂]
@@ -17,9 +17,7 @@ Wenn das Goal `A ↔ B` ist, kann man mit der `constructor` Taktik, dieses in di
 "

 Statement
-    "
-    Zeige dass `B ↔ C`.
-    "
+    "Zeige dass `B ↔ C`."
    (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
  constructor
  assumption
@@ -20,6 +20,7 @@ man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<`

 "
 Statement
+    ""
    (A B : Prop) : (A ↔ B) → (A → B) := by
  intro h
  rcases h
@@ -17,9 +17,7 @@ Implikation `A → B` auf ein Goal `B` anwenden.
 "

 Statement
-    "
-    Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen.
-    "
+    "Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen."
    (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
  intro hA
  apply g
@@ -20,6 +20,7 @@ Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man
 "

 Statement
+    ""
    (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
  constructor
  intro h
@@ -18,7 +18,7 @@ Wenn das Goal ein `∨` ist kann man mit `left` oder `right` entscheiden,
 welche Seite man beweisen möchte.
 "

-Statement (A B : Prop) (hA : A) : A ∨ (¬ B) := by
+Statement "" (A B : Prop) (hA : A) : A ∨ (¬ B) := by
  left
  assumption

@@ -25,6 +25,7 @@ Diese Annahme benennt man dann mit `rcases h with hA | hB`.
 "

 Statement
+    ""
    (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by
  rcases h with ⟨ha, hb⟩ | (h | h)
  left
@@ -16,7 +16,7 @@ Introduction
 "

 Statement and_or_imp
-  "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
+    "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
    (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
  rcases h with h₁ | h₂
  left
@@ -18,7 +18,7 @@ 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 "" (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  ring

 Conclusion
@@ -12,7 +12,7 @@ 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 "" (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
  rw [h]
  ring

@@ -33,7 +33,7 @@ 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 "" (n : ℕ) (h : even n) : even (n ^ 2) := by
  unfold even at *
  rcases h with ⟨x, hx⟩
  use 2 * x ^ 2
@@ -19,7 +19,7 @@ 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 "" : ∀ (x : ℕ), (even x) → odd (1 + x) := by
  intro x h
  unfold even at h
  unfold odd
@@ -13,7 +13,7 @@ TODO: Summe

 "

-Statement : True := by
+Statement "" : True := by
  trivial

 Conclusion
@@ -13,7 +13,7 @@ TODO: Induktion (& induktion vs rcases)

 "

-Statement : True := by
+Statement "" : True := by
  trivial

 Conclusion
@@ -13,7 +13,7 @@ TODO: Primzahl

 "

-Statement : True := by
+Statement "" : True := by
  trivial

 Conclusion
@@ -13,7 +13,7 @@ TODO: Es existiert genau eine gerade Primzahl.

 "

-Statement : True := by
+Statement "" : True := by
  trivial

 Conclusion
@@ -22,7 +22,7 @@ Der einfachste Widerspruch ist wenn man einen Beweis von `false` hat:
 "

 Statement
-  "Ein Widerspruch impliziert alles."
+    "Ein Widerspruch impliziert alles."
    (A : Prop) (h : false) : A := by
  contradiction

@@ -17,7 +17,7 @@ also `(h : A)` und `(g : ¬ A)`. (`\\not`)
 "

 Statement
-  "Ein Widerspruch impliziert alles."
+    "Ein Widerspruch impliziert alles."
    (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 128 := by
  contradiction

@@ -22,8 +22,8 @@ Hier musst du zuerst eines der Lemmas `not_odd : ¬ odd n ↔ even n` oder
 "

 Statement
-  "Ein Widerspruch impliziert alles."
-  (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
+    "Ein Widerspruch impliziert alles."
+    (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
  rw [← not_even] at h₂
  contradiction

@@ -16,7 +16,7 @@ oder auch Annahmen der Form `A ≠ A` (`\\ne`).
 "

 Statement
-  "Ein Widerspruch impliziert alles."
+    "Ein Widerspruch impliziert alles."
    (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by
  rw [g₁] at h
  contradiction
@@ -15,6 +15,7 @@ wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form
 "

 Statement
+    ""
    (A : Prop) : ¬ (¬ A) ↔ A := by
  rw [not_not]

@@ -19,7 +19,7 @@ dass das Gegenteil des Goals wahr sei, und dann einen Widerspruch erzeugen.
 "

 Statement
-  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
+    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
    (n : ℕ) (h : odd (n ^ 2)) : odd n := by
  by_contra g
  rw [not_odd] at g
@@ -22,7 +22,7 @@ Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
 "

 Statement
-  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
    (n : ℕ) : odd (n ^ 2) → odd n := by
  contrapose
  rw [not_odd]
@@ -20,7 +20,7 @@ Implikationsannahme ins Goal schreiben.
 "

 Statement
-  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
    (n : ℕ) (h : odd (n ^ 2)): odd n := by
  revert h
  contrapose
@@ -17,8 +17,8 @@ mit `push_neg` das `¬` durch den Quantor hindurchschieben.
 "

 Statement
-  "Es existiert keine natürliche Zahl, die grösser als alle anderen."
-  : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
+    "Es existiert keine natürliche Zahl, die grösser als alle anderen.":
+    ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
  push_neg
  intro n
  use 3*n + 6