add docs
This commit is contained in:
Jon Eugster
@@ -1,97 +0,0 @@
|
||||
# Level
|
||||
|
||||
A level is a single exercise that should be solved by the user. Here is an example:
|
||||
|
||||
```lean
|
||||
import GameServer.Commands -- also import everything else you need.
|
||||
|
||||
Game "NNG"
|
||||
World "Addition"
|
||||
Level 2 -- must start at `1` and be consequtive.
|
||||
Title "add_zero"
|
||||
|
||||
Introduction "" -- optional. Is displayed throughout the level.
|
||||
|
||||
Statement MyNat.zero_add -- optional. if name is specified, the lemma will be added to the inventory in future levels.
|
||||
"description in mathematical term" -- optional. mathematical description
|
||||
(n : ℕ) : n + 0 = n := by -- statement: exactly how it would be in a `theorem`. (bug: forgets about implicit arguments)
|
||||
intro k
|
||||
rw [add_zero]
|
||||
Hint "look at {k}." -- hint at this place. `{k}` gets the user's name for the variable (bug currently)
|
||||
Hint (hidden := true) "more" -- hidden hint
|
||||
use n
|
||||
Branch -- A branch in the proof. Does not modify the goal but useful
|
||||
simp -- to place hints at dead ends etc.
|
||||
tauto
|
||||
rw [add_comm]
|
||||
rfl
|
||||
|
||||
LemmaTab "Nat" -- optional. specify the tab that's open in the lemma inventory
|
||||
|
||||
NewLemma add_zero -- optional. add lemma to inventory
|
||||
NewTactic rw -- optional. add tactic to inventory
|
||||
NewDefinition Nat -- optional. add definition to inventory
|
||||
DisabledLemma add_zero -- optional. disable specific lemmas
|
||||
DisabledTactic tauto simp -- optional. disable tactics
|
||||
OnlyLemma add_zero -- optional. disable all lemmas but these
|
||||
OnlyTactic assumption rw -- optional. disable all tactics but these
|
||||
|
||||
Conclusion "" -- optional. Show when level completed
|
||||
```
|
||||
|
||||
And in the following there are some tips that might be important.
|
||||
|
||||
## Imports
|
||||
|
||||
You're level can import levels from the same world
|
||||
|
||||
```
|
||||
import NNG.Levels.Addition.Level_1
|
||||
```
|
||||
|
||||
as well as entire other worlds
|
||||
|
||||
```
|
||||
import NNG.Levels.Multiplication
|
||||
```
|
||||
|
||||
However, you must not import a single level in a different world's level or
|
||||
it will mess up the World introduction texts (bug?)
|
||||
|
||||
## Documentation (Lemmas, Tactics, Definitions)
|
||||
|
||||
It will complain when the specified lemma/tactic names do not have documentation.
|
||||
In that case you need to add `LemmaDoc`/`TacticDoc`/`DefinitionDoc` entries in the
|
||||
doc part (and `ctrl+shift+X`-reload your file in VSCode). See info under `Game > Documentation`
|
||||
|
||||
# World
|
||||
|
||||
combines multiple levels, like a chapter. Description pending.
|
||||
|
||||
# Game
|
||||
|
||||
Combines different games in form of a directed graph. Description pending.
|
||||
|
||||
## Documentation
|
||||
It is recommended to have all documentation for the inventory centrally and import it in
|
||||
the levels
|
||||
|
||||
```lean
|
||||
LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
|
||||
"(missing)"
|
||||
|
||||
TacticDoc constructor
|
||||
"(missing)"
|
||||
|
||||
DefinitionDoc One as "1"
|
||||
"(missing)"
|
||||
```
|
||||
|
||||
Notes:
|
||||
|
||||
* The lemma name must be **fully qualified**. The string display name can be arbitrary.
|
||||
* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
|
||||
without french quotes.
|
||||
* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
|
||||
|
||||
There will be features added to get automatic information from mathlib!
|
||||
@@ -0,0 +1,156 @@
|
||||
# Creating a game.
|
||||
|
||||
Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
|
||||
|
||||
## Game Structure
|
||||
|
||||
A game consist of worlds which have multiple levels each. In the following we describe how to create a level file and how to combine these into a game.
|
||||
|
||||
### Level
|
||||
|
||||
#### Preample
|
||||
|
||||
A level file is a lean file that imports at least `GameServer.Commands` and starts with the four lean commands
|
||||
|
||||
```lean
|
||||
Game "NNG"
|
||||
World "Addition"
|
||||
Level 1
|
||||
Title "The rfl tactic"
|
||||
```
|
||||
|
||||
Note that the levels inside a world must have consequtive numbering starting with `1`. The `Game`
|
||||
and `World` strings can be anything.
|
||||
|
||||
#### Statement
|
||||
|
||||
The core of a level is the `Statement`, which is the exercise that should be proven:
|
||||
|
||||
```lean
|
||||
Statement MyNat.zero_add
|
||||
"For all natural numbers $n$, we have $0 + n = n$."
|
||||
(n : ℕ) : 0 + n = n := by
|
||||
Hint "You can start a proof by `induction n`."
|
||||
induction n with n hn
|
||||
· Hint "This is the base case."
|
||||
rw [add_zero]
|
||||
rfl
|
||||
· Hint "This is the induction hypothesis"
|
||||
rw [add_succ]
|
||||
Branch
|
||||
simp
|
||||
Hint "A branch is an alternative tactic sequence. Does not need to finish the proof."
|
||||
rw [hn]
|
||||
rfl
|
||||
```
|
||||
|
||||
The first two arguments (name, attributes, and description) are optional. Thereafter you have a statement and a proof.
|
||||
|
||||
- The proof should always be a tactic proof, i.e. the `:= by` is mandatory.
|
||||
- In the proof you can use `Hint "text"` to display text if the goal state in-game matches the one where `Hint` is placed. For more options about hints, see below.
|
||||
- In the proof you can add a `Branch` that runs an alternativ tactic sequence, which helps setting `Hints` in different places. The `Branch` does not affect the main proof and does not need to finish any goals.
|
||||
- If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels. (Note that a future level must also import this level, so that Lean knows about the added statement). The name must be *fully qualified*.
|
||||
- If you add a description (i.e. non-Lean exercise statement), it will be shown above the exercise. It supports Markdown (including katex).
|
||||
|
||||
#### Introduction/Conclusion
|
||||
|
||||
Optionally, you can add a `Introduction "some text"` and `Conclusion "some text"` to your level. the introduction will always be visible on top, the conclusion is displayed once the level is solved.
|
||||
|
||||
#### Lemmas/Tactics/Definitions
|
||||
|
||||
Only enabled lemmas/tactics/definitions (called "items" here) are available in a level.
|
||||
|
||||
To add a new item in a level, you can add
|
||||
|
||||
```lean
|
||||
NewTactic rfl simp
|
||||
NewLemma MyNat.add_zero
|
||||
NewDefinition Nat
|
||||
```
|
||||
|
||||
Once added, items will be available in all future levels/worlds, unless you disable them for a particular level with
|
||||
|
||||
```lean
|
||||
DisabledTactic tauto
|
||||
DisabledLemma MyNat.add_zero
|
||||
```
|
||||
|
||||
or specify explicitely which items should be available with
|
||||
|
||||
```lean
|
||||
OnlyTactic rw rfl apply
|
||||
OnlyLemma MyNat.add_zero
|
||||
```
|
||||
|
||||
Lastly, all items need documentation entries (which are imported in the level), see more about that below. There is also explains the `LemmaTab`
|
||||
|
||||
### World
|
||||
|
||||
Multiple levels are combined into a world and the worlds are then added to the game. It is recommended that all levels of a world are inside one folder (e.g. `NNG/Levels/Addition/`) and
|
||||
then there is one world file (`NNG/Levels/Addition.lean`) which contains the following
|
||||
|
||||
```lean
|
||||
import NNG.Levels.Addition.Level_1
|
||||
import NNG.Levels.Addition.Level_2
|
||||
|
||||
Game "NNG"
|
||||
World "Addition"
|
||||
Title "Addition World"
|
||||
|
||||
Introduction "some text"
|
||||
```
|
||||
|
||||
The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
|
||||
Note that all levels of a world should be imported by the world file and they **must not** be
|
||||
imported in another world's levels. (bug?)
|
||||
|
||||
However, you can import an entire world in a different world's level: `import NNG.Levels.Addition`
|
||||
|
||||
### Game
|
||||
|
||||
The Game itself (i.e. the main file of you lake project, `NNG.lean`) should import all worlds and have the following layout, concluding with `MakeGame`:
|
||||
|
||||
```lean
|
||||
import NNG.Levels.Addition
|
||||
import NNG.Levels.Multiplication
|
||||
import NNG.Levels.Power
|
||||
|
||||
Game "NNG"
|
||||
Title "Natural Number Game"
|
||||
Introduction "some text"
|
||||
|
||||
Path Addition → Multiplication → Power
|
||||
|
||||
MakeGame
|
||||
```
|
||||
|
||||
There can be several `Path` statements to define the relation between the worlds. The worlds
|
||||
must form a directed acyclic graph, i.e. have no loops. The order of worlds influences which tactics and lemmas will be unlocked in a given level.
|
||||
|
||||
### Documentation
|
||||
|
||||
Each tactic, lemma, or definition (all called items here) that is introduced in the game
|
||||
needs a documentation entry. These are statements of the following form:
|
||||
|
||||
```lean
|
||||
LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
|
||||
"(missing)"
|
||||
|
||||
TacticDoc constructor
|
||||
"(missing)"
|
||||
|
||||
DefinitionDoc One as "1"
|
||||
"(missing)"
|
||||
```
|
||||
|
||||
Notes:
|
||||
|
||||
* The lemma name must be **fully qualified**. The string display name can be arbitrary.
|
||||
* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
|
||||
without french quotes.
|
||||
* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
|
||||
|
||||
Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level file, you
|
||||
can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.
|
||||
|
||||
There will be features added to get automatic information from mathlib!
|
||||
Reference in New Issue
Block a user