diff --git a/CREATE_GAME.md b/CREATE_GAME.md deleted file mode 100644 index 87b7f2d..0000000 --- a/CREATE_GAME.md +++ /dev/null @@ -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! diff --git a/DOCUMENTATION.md b/DOCUMENTATION.md new file mode 100644 index 0000000..9530ade --- /dev/null +++ b/DOCUMENTATION.md @@ -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!