- { 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
"