From f48f639190ef9f0e696a460334be2f0d8d7acb67 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 17 Apr 2023 14:59:44 +0200 Subject: [PATCH] nng levels --- client/src/components/Level.tsx | 4 +- server/leanserver/GameServer/Commands.lean | 4 +- server/nng/NNG/Doc/Definitions.lean | 17 +++++++- server/nng/NNG/Doc/Lemmas.lean | 8 +++- server/nng/NNG/Doc/Tactics.lean | 38 ++++++++++-------- server/nng/NNG/Levels/Addition.lean | 43 ++++++++++++--------- server/nng/NNG/Levels/AdvAddition.lean | 1 + server/nng/NNG/Levels/Tutorial/Level_2.lean | 14 +++---- server/nng/NNG/Levels/Tutorial/Level_3.lean | 6 +-- server/nng/NNG/Levels/Tutorial/Level_4.lean | 17 ++++---- 10 files changed, 88 insertions(+), 64 deletions(-) diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 9637762..b3aef2d 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -249,13 +249,11 @@ function Introduction({worldId}) {
- { gameInfo.data?.worlds.nodes[worldId].introduction && -
+
{gameInfo.data?.worlds.nodes[worldId].introduction}
- }
{0 == gameInfo.data?.worldSize[worldId] ? diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 8a3b211..692139b 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -97,8 +97,8 @@ elab "TacticDoc" name:ident content:str : command => modifyEnv (inventoryDocExt.addEntry · { category := default type := .Tactic - name := name.getId, - displayName := name.getId.toString, + name := name.getId + displayName := name.getId.toString content := content.getString }) /-- Documentation entry of a lemma. Example: diff --git a/server/nng/NNG/Doc/Definitions.lean b/server/nng/NNG/Doc/Definitions.lean index 8a1d6c4..860c789 100644 --- a/server/nng/NNG/Doc/Definitions.lean +++ b/server/nng/NNG/Doc/Definitions.lean @@ -2,7 +2,11 @@ import GameServer.Commands DefinitionDoc MyNat as "ℕ" " -The Natural Numbers. +The Natural Numbers. These are constructed through: + +* `(0 : ℕ)`, an element called zero. +* `(succ : ℕ → ℕ)`, the successor function , i.e. one is `succ 0` and two is `succ (succ 0)`. +* `induction` (or `rcases`), tactics to treat the cases $n = 0$ and `n = m + 1` seperately. ## Game Modifications @@ -11,4 +15,13 @@ The natural numbers implemented in Lean's core are called `Nat`. If you end up getting someting of type `Nat` in this game, you probably need to write `(4 : ℕ)` to force it to be of type `MyNat`. -" \ No newline at end of file +" + +DefinitionDoc Add as "+" " +Addition on `ℕ` is defined through two axioms: + +* `add_zero (a : ℕ) : a + 0 = a` +* `add_succ (a d : ℕ) : a + succ d = succ (a + d)` +" + +DefinitionDoc Mul as "*" "" \ No newline at end of file diff --git a/server/nng/NNG/Doc/Lemmas.lean b/server/nng/NNG/Doc/Lemmas.lean index 832d773..821b846 100644 --- a/server/nng/NNG/Doc/Lemmas.lean +++ b/server/nng/NNG/Doc/Lemmas.lean @@ -1,10 +1,14 @@ import GameServer.Commands LemmaDoc MyNat.add_zero as "add_zero" in "Nat" -"(missing)" +"`add_zero (a : ℕ) : a + 0 = a` + +This is one of the two axioms defining addition on `ℕ`." LemmaDoc MyNat.add_succ as "add_succ" in "Nat" -"(missing)" +"`add_succ (a d : ℕ) : a + (succ d) = succ (a + d)` + +This is the second axiom definiting addition on `ℕ`" LemmaDoc MyNat.zero_add as "zero_add" in "Nat" "(missing)" diff --git a/server/nng/NNG/Doc/Tactics.lean b/server/nng/NNG/Doc/Tactics.lean index 5712775..1dda959 100644 --- a/server/nng/NNG/Doc/Tactics.lean +++ b/server/nng/NNG/Doc/Tactics.lean @@ -32,19 +32,19 @@ could prove things like `a + 0 = a`. " -TacticDoc rewrite -" -" TacticDoc rw " ## Summary -If `h` is a proof of `X = Y`, then `rw h,` will change -all `X`s in the goal to `Y`s. Variants: `rw ← h` (changes -`Y` to `X`) and -`rw h at h2` (changes `X` to `Y` in hypothesis `h2` instead -of the goal). +If `h` is a proof of `X = Y`, then `rw [h]` will change +all `X`s in the goal to `Y`s. + +### Variants + +* `rw [← h#` (changes `Y` to `X`) +* `rw [h] at h2` (changes `X` to `Y` in hypothesis `h2` instead of the goal) +* `rw [h] at *` (changes `X` to `Y` in the goal and all hypotheses) ## Details @@ -53,14 +53,14 @@ are two distinct situations where use this tactics. 1) If `h : A = B` is a hypothesis (i.e., a proof of `A = B`) in your local context (the box in the top right) -and if your goal contains one or more `A`s, then `rw h` +and if your goal contains one or more `A`s, then `rw [h]` will change them all to `B`'s. 2) The `rw` tactic will also work with proofs of theorems which are equalities (look for them in the drop down menu on the left, within Theorem Statements). For example, in world 1 level 4 -we learn about `add_zero x : x + 0 = x`, and `rw add_zero` +we learn about `add_zero x : x + 0 = x`, and `rw [add_zero]` will change `x + 0` into `x` in your goal (or fail with an error if Lean cannot find `x + 0` in the goal). @@ -70,7 +70,7 @@ or perhaps even a proposition itself rather than its proof), then `rw` is not the tactic you want to use. For example, `rw (P = Q)` is never correct: `P = Q` is the true-false statement itself, not the proof. -If `h : P = Q` is its proof, then `rw h` will work. +If `h : P = Q` is its proof, then `rw [h]` will work. Pro tip 1: If `h : A = B` and you want to change `B`s to `A`s instead, try `rw ←h` (get the arrow with `\\l` and @@ -80,7 +80,9 @@ note that this is a small letter L, not a number 1). If it looks like this in the top right hand box: ``` +Objects: x y : ℕ +Assumptions: h : x = y + y Goal: succ (x + 0) = succ (y + y) @@ -88,14 +90,14 @@ Goal: then -`rw add_zero,` +`rw [add_zero]` -will change the goal into `⊢ succ x = succ (y + y)`, and then +will change the goal into `succ x = succ (y + y)`, and then -`rw h,` +`rw [h]` -will change the goal into `⊢ succ (y + y) = succ (y + y)`, which -can be solved with `refl,`. +will change the goal into `succ (y + y) = succ (y + y)`, which +can be solved with `rfl`. ### Example: @@ -103,13 +105,15 @@ You can use `rw` to change a hypothesis as well. For example, if your local context looks like this: ``` +Objects: x y : ℕ +Assumptions: h1 : x = y + 3 h2 : 2 * y = x Goal: y = 3 ``` -then `rw h1 at h2` will turn `h2` into `h2 : 2 * y = y + 3`. +then `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`. ## Game modifications diff --git a/server/nng/NNG/Levels/Addition.lean b/server/nng/NNG/Levels/Addition.lean index 84d3722..27e5416 100644 --- a/server/nng/NNG/Levels/Addition.lean +++ b/server/nng/NNG/Levels/Addition.lean @@ -12,31 +12,36 @@ Title "Addition World" Introduction " -Welcome to Addition World. If you've done all four levels in tutorial world -and know about `rewrite` and `rfl`, then you're in the right place. Here's -a reminder of the things you're now equipped with which we'll need in this world. +Hi! +" + +-- Introduction +-- " +-- Welcome to Addition World. If you've done all four levels in tutorial world +-- and know about `rewrite` and `rfl`, then you're in the right place. Here's +-- a reminder of the things you're now equipped with which we'll need in this world. -## Data: +-- ## Data: - * a type called `ℕ` or `MyNat`. - * a term `0 : ℕ`, interpreted as the number zero. - * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\". - * Usual numerical notation `0,1,2` etc. (although `2` onwards will be of no use to us until much later ;-) ). - * Addition (with notation `a + b`). +-- * a type called `ℕ` or `MyNat`. +-- * a term `0 : ℕ`, interpreted as the number zero. +-- * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\". +-- * Usual numerical notation `0,1,2` etc. (although `2` onwards will be of no use to us until much later ;-) ). +-- * Addition (with notation `a + b`). -## Theorems: +-- ## Theorems: - * `add_zero (a : ℕ) : a + 0 = a`. Use with `rewrite [add_zero]`. - * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rewrite [add_succ]`. - * The principle of mathematical induction. Use with `induction` (which we learn about in this chapter). +-- * `add_zero (a : ℕ) : a + 0 = a`. Use with `rewrite [add_zero]`. +-- * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rewrite [add_succ]`. +-- * The principle of mathematical induction. Use with `induction` (which we learn about in this chapter). -## Tactics: +-- ## Tactics: - * `rfl` : proves goals of the form `X = X`. - * `rewrite [h]` : if `h` is a proof of `A = B`, changes all `A`'s in the goal to `B`'s. - * `induction n with d hd` : we're going to learn this right now. +-- * `rfl` : proves goals of the form `X = X`. +-- * `rewrite [h]` : if `h` is a proof of `A = B`, changes all `A`'s in the goal to `B`'s. +-- * `induction n with d hd` : we're going to learn this right now. -You will also find all this information in your Inventory to read the documentation. -" \ No newline at end of file +-- You will also find all this information in your Inventory to read the documentation. +-- " \ No newline at end of file diff --git a/server/nng/NNG/Levels/AdvAddition.lean b/server/nng/NNG/Levels/AdvAddition.lean index cc2e95d..129b734 100644 --- a/server/nng/NNG/Levels/AdvAddition.lean +++ b/server/nng/NNG/Levels/AdvAddition.lean @@ -19,4 +19,5 @@ Title "Advanced Addition World" Introduction " + Hi " \ No newline at end of file diff --git a/server/nng/NNG/Levels/Tutorial/Level_2.lean b/server/nng/NNG/Levels/Tutorial/Level_2.lean index 4178943..b4992c1 100644 --- a/server/nng/NNG/Levels/Tutorial/Level_2.lean +++ b/server/nng/NNG/Levels/Tutorial/Level_2.lean @@ -4,31 +4,29 @@ import NNG.MyNat.Multiplication Game "NNG" World "Tutorial" Level 2 -Title "the rewrite (rw) tactic" +Title "the rw tactic" Introduction " In this level, you also get \"Assumptions\" about your objects. These are hypotheses of which you assume (or know) that they are true. -The `rewrite` tactic is the way to \"substitute in\" the value of a variable. +The \"rewrite\" tactic `rw` is the way to \"substitute in\" the value of a variable. If you have a hypothesis of the form `A = B`, and your goal mentions the left hand side `A` somewhere, then the rewrite tactic will replace the `A` in your goal with a `B`. - -*(Note: For this game, `rw` is a shorthand for `rewrite`. Out in the real world, `rw` tries to call -`rfl` automatically afterwards.)* +Here is a theorem which cannot be proved using rfl -- you need a rewrite first. " Statement "If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$." (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by - Hint "You can use `rewrite [h]` to replace the `{y}` with `x + 7`. + Hint "You can use `rw [h]` to replace the `{y}` with `x + 7`. Note that the assumption `h` is written inside square brackets: `[h]`." rw [h] - Hint "In this game not all hints are directly shown. If you need help finishing the proof, click - on \"More Help\" below!" + Hint "Not all hints are directly shown. If you are stuck and need more help + finishing the proof, click on \"More Help\" below!" Hint (hidden := true) "Now both sides are identical, so you can use `rfl` to close the goal." rfl diff --git a/server/nng/NNG/Levels/Tutorial/Level_3.lean b/server/nng/NNG/Levels/Tutorial/Level_3.lean index a65e434..77abf68 100644 --- a/server/nng/NNG/Levels/Tutorial/Level_3.lean +++ b/server/nng/NNG/Levels/Tutorial/Level_3.lean @@ -40,13 +40,13 @@ on the natural numbers, for example addition, multiplication and so on. This game is all about seeing how far these axioms of Peano can take us. -Now let us practise the use of `rewrite` with this new function `succ`: +Now let us practise the use of `rw` with this new function `succ`: " Statement "If $\\operatorname{succ}(a) = b$, then $\\operatorname{succ}(\\operatorname{succ}(a)) = \\operatorname{succ}(a)$." (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by - Hint "You can use `rewrite` and your assumption `{h}` to substitute `succ a` with `b`. + Hint "You can use `rw` and your assumption `{h}` to substitute `succ a` with `b`. Notes: @@ -54,7 +54,7 @@ Statement them in mathematics: `succ b` means $\\operatorname\{succ}(b)$. 2) If you would want to substitute instead `b` with `succ a`, you can do that writing a small `←` (`\\l`, i.e. backslash + small letter L + space) - before `h` like this: `rewrite [← h]`." + before `h` like this: `rw [← h]`." Branch rewrite [← h] Hint (hidden := true) "Now both sides are identical…" diff --git a/server/nng/NNG/Levels/Tutorial/Level_4.lean b/server/nng/NNG/Levels/Tutorial/Level_4.lean index 742c5ac..b0e55bf 100644 --- a/server/nng/NNG/Levels/Tutorial/Level_4.lean +++ b/server/nng/NNG/Levels/Tutorial/Level_4.lean @@ -21,9 +21,9 @@ theorem. Note the name of this proof. Mathematicians sometimes call it \"Lemma 2.1\" or \"Hypothesis P6\" or something. But computer scientists call it `add_zero` because it tells you what the answer to \"x add zero\" is. It's a much better name than \"Lemma 2.1\". -Even better, you can use the `rewrite` tactic +Even better, you can use the `rw` tactic with `add_zero`. If you ever see `x + 0` in your goal, -`rewrite [add_zero]` should simplify it to `x`. This is +`rw [add_zero]` should simplify it to `x`. This is because `add_zero` is a proof that `x + 0 = x` (more precisely, `add_zero x` is a proof that `x + 0 = x` but Lean can figure out the `x` from the context). @@ -38,23 +38,24 @@ What's going on here is that we assume `a + d` is already defined, and we define Note the name of this proof too: `add_succ` tells you how to add a successor to something. If you ever see `… + succ …` in your goal, you should be able to use -`rewrite [add_succ]`, to make progress. +`rw [add_succ]` to make progress. " Statement "For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = a$." (a : ℕ) : a + succ 0 = succ a := by - Hint "You find `{a} + succ …` in the goal, so you can use `rewrite` and `add_succ` + Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ` to make progress." - Hint (hidden := true) "Explicitely, type `rewrite [add_succ]`!" - rewrite [add_succ] + Hint (hidden := true) "Explicitely, type `rw [add_succ]`!" + rw [add_succ] Hint "Now you see a term of the form `… + 0`, so you can use `add_zero`." - Hint (hidden := true) "Explicitely, type `rewrite [add_zero]`!" - rewrite [add_zero] + Hint (hidden := true) "Explicitely, type `rw [add_zero]`!" + rw [add_zero] Hint (hidden := true) "Finally both sides are identical." rfl NewLemma MyNat.add_succ MyNat.add_zero +NewDefinition Add Conclusion "