nng levels

2023-04-17 14:59:44 +02:00
parent 8d395d56e7
commit f48f639190
10 changed files with 88 additions and 64 deletions
@@ -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:
@@ -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`.
-"
+"
+
+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 "*" ""
@@ -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)"
@@ -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

@@ -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!
+"

-## Data:
+-- 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.

-  * 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`).
+-- ## Data:

-## Theorems:
+--   * 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`).

-  * `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).
+-- ## 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).


-## 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.
-"
+-- You will also find all this information in your Inventory to read the documentation.
+-- "
@@ -19,4 +19,5 @@ Title "Advanced Addition World"

 Introduction
 "
+  Hi
 "
@@ -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
@@ -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…"
@@ -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
 "