From 6e8911e5dab07ebe1ab0c02aca8c6f08b5b14b07 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 26 Mar 2023 14:29:13 +0200 Subject: [PATCH] add NNG --- server/nng/NNG.lean | 32 ++++- server/nng/NNG/Doc/Definitions.lean | 6 + server/nng/NNG/Doc/Lemmas.lean | 31 +++++ server/nng/NNG/Doc/Tactics.lean | 57 ++++++++ server/nng/NNG/Levels/Addition.lean | 42 ++++++ server/nng/NNG/Levels/Addition/Level_1.lean | 93 +++++++++++++ server/nng/NNG/Levels/Addition/Level_2.lean | 70 ++++++++++ server/nng/NNG/Levels/Addition/Level_3.lean | 66 +++++++++ server/nng/NNG/Levels/Addition/Level_4.lean | 60 ++++++++ server/nng/NNG/Levels/Addition/Level_5.lean | 54 ++++++++ server/nng/NNG/Levels/Addition/Level_6.lean | 47 +++++++ server/nng/NNG/Levels/AdvAddition.lean | 22 +++ .../nng/NNG/Levels/AdvAddition/Level_1.lean | 30 ++++ .../nng/NNG/Levels/AdvAddition/Level_10.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_11.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_12.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_13.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_2.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_3.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_4.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_5.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_6.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_7.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_8.lean | 24 ++++ .../nng/NNG/Levels/AdvAddition/Level_9.lean | 24 ++++ server/nng/NNG/Levels/AdvMultiplication.lean | 13 ++ .../NNG/Levels/AdvMultiplication/Level_1.lean | 24 ++++ .../NNG/Levels/AdvMultiplication/Level_2.lean | 24 ++++ .../NNG/Levels/AdvMultiplication/Level_3.lean | 24 ++++ .../NNG/Levels/AdvMultiplication/Level_4.lean | 24 ++++ server/nng/NNG/Levels/AdvProposition.lean | 19 +++ .../NNG/Levels/AdvProposition/Level_1.lean | 28 ++++ .../NNG/Levels/AdvProposition/Level_10.lean | 36 +++++ .../NNG/Levels/AdvProposition/Level_2.lean | 33 +++++ .../NNG/Levels/AdvProposition/Level_3.lean | 31 +++++ .../NNG/Levels/AdvProposition/Level_4.lean | 31 +++++ .../NNG/Levels/AdvProposition/Level_5.lean | 34 +++++ .../NNG/Levels/AdvProposition/Level_6.lean | 31 +++++ .../NNG/Levels/AdvProposition/Level_7.lean | 31 +++++ .../NNG/Levels/AdvProposition/Level_8.lean | 49 +++++++ .../NNG/Levels/AdvProposition/Level_9.lean | 36 +++++ server/nng/NNG/Levels/Function.lean | 18 +++ server/nng/NNG/Levels/Function/Level_1.lean | 27 ++++ server/nng/NNG/Levels/Function/Level_2.lean | 28 ++++ server/nng/NNG/Levels/Function/Level_3.lean | 31 +++++ server/nng/NNG/Levels/Function/Level_4.lean | 37 +++++ server/nng/NNG/Levels/Function/Level_5.lean | 27 ++++ server/nng/NNG/Levels/Function/Level_6.lean | 30 ++++ server/nng/NNG/Levels/Function/Level_7.lean | 29 ++++ server/nng/NNG/Levels/Function/Level_8.lean | 27 ++++ server/nng/NNG/Levels/Function/Level_9.lean | 36 +++++ server/nng/NNG/Levels/Inequality.lean | 25 ++++ server/nng/NNG/Levels/Inequality/Level_1.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_10.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_11.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_12.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_13.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_14.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_15.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_16.lean | 24 ++++ .../nng/NNG/Levels/Inequality/Level_17.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_2.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_3.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_4.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_5.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_6.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_7.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_8.lean | 24 ++++ server/nng/NNG/Levels/Inequality/Level_9.lean | 24 ++++ server/nng/NNG/Levels/Multiplication.lean | 18 +++ .../NNG/Levels/Multiplication/Level_1.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_2.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_3.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_4.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_5.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_6.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_7.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_8.lean | 24 ++++ .../NNG/Levels/Multiplication/Level_9.lean | 24 ++++ server/nng/NNG/Levels/Power.lean | 16 +++ server/nng/NNG/Levels/Power/Level_1.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_2.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_3.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_4.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_5.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_6.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_7.lean | 24 ++++ server/nng/NNG/Levels/Power/Level_8.lean | 24 ++++ server/nng/NNG/Levels/Proposition.lean | 18 +++ .../nng/NNG/Levels/Proposition/Level_1.lean | 24 ++++ .../nng/NNG/Levels/Proposition/Level_2.lean | 25 ++++ .../nng/NNG/Levels/Proposition/Level_3.lean | 30 ++++ .../nng/NNG/Levels/Proposition/Level_4.lean | 30 ++++ .../nng/NNG/Levels/Proposition/Level_5.lean | 27 ++++ .../nng/NNG/Levels/Proposition/Level_6.lean | 30 ++++ .../nng/NNG/Levels/Proposition/Level_7.lean | 28 ++++ .../nng/NNG/Levels/Proposition/Level_8.lean | 35 +++++ .../nng/NNG/Levels/Proposition/Level_9.lean | 29 ++++ server/nng/NNG/Levels/Tutorial.lean | 12 ++ server/nng/NNG/Levels/Tutorial/Level_1.lean | 42 ++++++ server/nng/NNG/Levels/Tutorial/Level_2.lean | 46 ++++++ server/nng/NNG/Levels/Tutorial/Level_3.lean | 71 ++++++++++ server/nng/NNG/Levels/Tutorial/Level_4.lean | 68 +++++++++ server/nng/NNG/Metadata.lean | 5 + server/nng/NNG/Modifications/Tactics.lean | 131 ++++++++++++++++++ server/nng/NNG/MyNat/Addition.lean | 23 +++ server/nng/NNG/MyNat/Definition.lean | 37 +++++ server/nng/NNG/MyNat/Inequality.lean | 28 ++++ server/nng/NNG/MyNat/Multiplication.lean | 17 +++ server/nng/NNG/MyNat/Power.lean | 21 +++ server/nng/NNG/MyNat/Theorems/Addition.lean | 45 ++++++ .../nng/NNG/MyNat/Theorems/Proposition.lean | 1 + server/nng/lake-manifest.json | 27 +++- server/nng/lakefile.lean | 3 + 114 files changed, 3380 insertions(+), 4 deletions(-) create mode 100644 server/nng/NNG/Doc/Definitions.lean create mode 100644 server/nng/NNG/Doc/Lemmas.lean create mode 100644 server/nng/NNG/Doc/Tactics.lean create mode 100644 server/nng/NNG/Levels/Addition.lean create mode 100644 server/nng/NNG/Levels/Addition/Level_1.lean create mode 100644 server/nng/NNG/Levels/Addition/Level_2.lean create mode 100644 server/nng/NNG/Levels/Addition/Level_3.lean create mode 100644 server/nng/NNG/Levels/Addition/Level_4.lean create mode 100644 server/nng/NNG/Levels/Addition/Level_5.lean create mode 100644 server/nng/NNG/Levels/Addition/Level_6.lean create mode 100644 server/nng/NNG/Levels/AdvAddition.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_1.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_10.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_11.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_12.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_13.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_2.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_3.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_4.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_5.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_6.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_7.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_8.lean create mode 100644 server/nng/NNG/Levels/AdvAddition/Level_9.lean create mode 100644 server/nng/NNG/Levels/AdvMultiplication.lean create mode 100644 server/nng/NNG/Levels/AdvMultiplication/Level_1.lean create mode 100644 server/nng/NNG/Levels/AdvMultiplication/Level_2.lean create mode 100644 server/nng/NNG/Levels/AdvMultiplication/Level_3.lean create mode 100644 server/nng/NNG/Levels/AdvMultiplication/Level_4.lean create mode 100644 server/nng/NNG/Levels/AdvProposition.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_1.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_10.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_2.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_3.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_4.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_5.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_6.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_7.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_8.lean create mode 100644 server/nng/NNG/Levels/AdvProposition/Level_9.lean create mode 100644 server/nng/NNG/Levels/Function.lean create mode 100644 server/nng/NNG/Levels/Function/Level_1.lean create mode 100644 server/nng/NNG/Levels/Function/Level_2.lean create mode 100644 server/nng/NNG/Levels/Function/Level_3.lean create mode 100644 server/nng/NNG/Levels/Function/Level_4.lean create mode 100644 server/nng/NNG/Levels/Function/Level_5.lean create mode 100644 server/nng/NNG/Levels/Function/Level_6.lean create mode 100644 server/nng/NNG/Levels/Function/Level_7.lean create mode 100644 server/nng/NNG/Levels/Function/Level_8.lean create mode 100644 server/nng/NNG/Levels/Function/Level_9.lean create mode 100644 server/nng/NNG/Levels/Inequality.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_1.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_10.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_11.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_12.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_13.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_14.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_15.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_16.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_17.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_2.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_3.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_4.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_5.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_6.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_7.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_8.lean create mode 100644 server/nng/NNG/Levels/Inequality/Level_9.lean create mode 100644 server/nng/NNG/Levels/Multiplication.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_1.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_2.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_3.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_4.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_5.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_6.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_7.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_8.lean create mode 100644 server/nng/NNG/Levels/Multiplication/Level_9.lean create mode 100644 server/nng/NNG/Levels/Power.lean create mode 100644 server/nng/NNG/Levels/Power/Level_1.lean create mode 100644 server/nng/NNG/Levels/Power/Level_2.lean create mode 100644 server/nng/NNG/Levels/Power/Level_3.lean create mode 100644 server/nng/NNG/Levels/Power/Level_4.lean create mode 100644 server/nng/NNG/Levels/Power/Level_5.lean create mode 100644 server/nng/NNG/Levels/Power/Level_6.lean create mode 100644 server/nng/NNG/Levels/Power/Level_7.lean create mode 100644 server/nng/NNG/Levels/Power/Level_8.lean create mode 100644 server/nng/NNG/Levels/Proposition.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_1.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_2.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_3.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_4.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_5.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_6.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_7.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_8.lean create mode 100644 server/nng/NNG/Levels/Proposition/Level_9.lean create mode 100644 server/nng/NNG/Levels/Tutorial.lean create mode 100644 server/nng/NNG/Levels/Tutorial/Level_1.lean create mode 100644 server/nng/NNG/Levels/Tutorial/Level_2.lean create mode 100644 server/nng/NNG/Levels/Tutorial/Level_3.lean create mode 100644 server/nng/NNG/Levels/Tutorial/Level_4.lean create mode 100644 server/nng/NNG/Metadata.lean create mode 100644 server/nng/NNG/Modifications/Tactics.lean create mode 100644 server/nng/NNG/MyNat/Addition.lean create mode 100644 server/nng/NNG/MyNat/Definition.lean create mode 100644 server/nng/NNG/MyNat/Inequality.lean create mode 100644 server/nng/NNG/MyNat/Multiplication.lean create mode 100644 server/nng/NNG/MyNat/Power.lean create mode 100644 server/nng/NNG/MyNat/Theorems/Addition.lean create mode 100644 server/nng/NNG/MyNat/Theorems/Proposition.lean diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean index 88032ba..b315174 100644 --- a/server/nng/NNG.lean +++ b/server/nng/NNG.lean @@ -1,9 +1,35 @@ import GameServer.Commands +import NNG.Levels.Tutorial +import NNG.Levels.Addition +import NNG.Levels.Multiplication +import NNG.Levels.Power +import NNG.Levels.Function +import NNG.Levels.Proposition +import NNG.Levels.AdvProposition +import NNG.Levels.AdvAddition +import NNG.Levels.AdvMultiplication +import NNG.Levels.Inequality + Game "NNG" -World "HelloWorld" -Level 1 +Title "Natural Number Game" +Introduction +" +[intro text missing] + +## Credits +* Content and Lean3-version: Kevin Buzzard, Mohammad Pedramfar +* Game Engine: Alexander Bentkamp, Jon Eugster, Patrick Massot +* Port to Lean 4: Chris Lovett + +## Resources +* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) +* [Chris' translation to lean4](https://lovettsoftware.com/NaturalNumbers/TutorialWorld/Level1.lean.html) +" -Statement : 1 + 1 = 2 := rfl +Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition +Path AdvAddition → AdvMultiplication → Inequality +Path Addition → Multiplication → AdvMultiplication +Path Multiplication → Power MakeGame \ No newline at end of file diff --git a/server/nng/NNG/Doc/Definitions.lean b/server/nng/NNG/Doc/Definitions.lean new file mode 100644 index 0000000..ec56a79 --- /dev/null +++ b/server/nng/NNG/Doc/Definitions.lean @@ -0,0 +1,6 @@ +import GameServer.Commands + +DefinitionDoc MyNat as "ℕ" +" +The Natural Numbers. +" \ No newline at end of file diff --git a/server/nng/NNG/Doc/Lemmas.lean b/server/nng/NNG/Doc/Lemmas.lean new file mode 100644 index 0000000..f7c4b03 --- /dev/null +++ b/server/nng/NNG/Doc/Lemmas.lean @@ -0,0 +1,31 @@ +import GameServer.Commands + +LemmaDoc MyNat.add_zero as "add_zero" in "Nat" +"" + +LemmaDoc MyNat.add_succ as "add_succ" in "Nat" +"" + +LemmaDoc MyNat.zero_add as "zero_add" in "Nat" +"" + +LemmaDoc MyNat.add_assoc as "add_assoc" in "Nat" +"" + +LemmaDoc MyNat.succ_add as "succ_add" in "Nat" +"" + +LemmaDoc MyNat.add_comm as "add_comm" in "Nat" +"" + +LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "Nat" +"" + +LemmaDoc not_iff_imp_false as "not_iff_imp_false" in "Prop" +"" + +LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat" +"" + +LemmaDoc MyNat.zero_ne_succ as "zero_ne_succ" in "Nat" +"" diff --git a/server/nng/NNG/Doc/Tactics.lean b/server/nng/NNG/Doc/Tactics.lean new file mode 100644 index 0000000..e0b50a3 --- /dev/null +++ b/server/nng/NNG/Doc/Tactics.lean @@ -0,0 +1,57 @@ +import GameServer.Commands + +TacticDoc rfl +" +" + +TacticDoc rewrite +" +" + +TacticDoc rw +" +" + +TacticDoc induction +" +" + +TacticDoc exact +" +" + +TacticDoc apply +" +" + +TacticDoc intro +" +" + +TacticDoc «have» +" +" + +TacticDoc constructor +" +" + +TacticDoc rcases +" +" + +TacticDoc left +" +" + +TacticDoc right +" +" + +TacticDoc contradiction +" +" + +TacticDoc exfalso +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Addition.lean b/server/nng/NNG/Levels/Addition.lean new file mode 100644 index 0000000..84d3722 --- /dev/null +++ b/server/nng/NNG/Levels/Addition.lean @@ -0,0 +1,42 @@ +import NNG.Levels.Addition.Level_1 +import NNG.Levels.Addition.Level_2 +import NNG.Levels.Addition.Level_3 +import NNG.Levels.Addition.Level_4 +import NNG.Levels.Addition.Level_5 +import NNG.Levels.Addition.Level_6 + + +Game "NNG" +World "Addition" +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. + +## 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`). + +## 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: + + * `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 diff --git a/server/nng/NNG/Levels/Addition/Level_1.lean b/server/nng/NNG/Levels/Addition/Level_1.lean new file mode 100644 index 0000000..e6e849c --- /dev/null +++ b/server/nng/NNG/Levels/Addition/Level_1.lean @@ -0,0 +1,93 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Addition" +Level 1 +Title "the induction tactic." + +open MyNat + +set_option tactic.hygienic false + +Introduction +" +OK so let's see induction in action. We're going to prove + +``` +zero_add (n : ℕ) : 0 + n = n +``` + +Wait… what is going on here? Didn't we already prove that adding zero to $n$ gave us $n$? + +No we didn't! We proved $n + 0 = n$, and that proof was called `add_zero`. We're now +trying to establish `zero_add`, the proof that $0 + n = n$. + +But aren't these two theorems the same? + +No they're not! It is *true* that `x + y = y + x`, but we haven't *proved* it yet, +and in fact we will need both `add_zero` and `zero_add` in order +to prove this. In fact `x + y = y + x` is the boss level for addition world, +and `induction` is the only other tactic you'll need to beat it. + +Now `add_zero` is one of Peano's axioms, so we don't need to prove it, we already have it. +To prove `0 + n = n` we need to use induction on $n$. While we're here, +note that `zero_add` is about zero add something, and `add_zero` is about something add zero. +The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`. +" + +Statement 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 over `n` by typing: + `induction n with d hd`. + + If you use the `with` part, you can name your variable and induction hypothesis, otherwise + they get default names." + induction n with n hn + · Hint "Now you have two goals. Once you proved the first, you will jump to the second one. + This first goal is the base case $n = 0$. + + Recall that you can use all lemmas that are visible in your inventory." + Hint (hidden := true) "try using `add_zero`." + rw [add_zero] + rfl + · Hint "Now you jumped to the second goal. Here you have the induction hypothesis + `{hn} : 0 + {n} = {n}` and you need to prove the statement for `succ {n}`." + Hint (hidden := true) "look at `add_succ`." + rw [add_succ] + Hint (hidden := true) "At this point you see the term `0 + {n}`, so you can use the + induction hypothesis with `rw [{hn}]`." + rw [hn] + rfl + +NewTactic induction + +Conclusion +" +## Now venture off on your own. + +Those three tactics: + +* `induction n with d hd` +* `rw [h]` +* `rfl` + +will get you quite a long way through this game. Using only these tactics +you can beat Addition World level 4 (the boss level of Addition World), +all of Multiplication World including the boss level `a * b = b * a`, +and even all of Power World including the fiendish final boss. This route will +give you a good grounding in these three basic tactics; after that, if you +are still interested, there are other worlds to master, where you can learn +more tactics. + +But we're getting ahead of ourselves, you still have to beat the rest of Addition World. +We're going to stop explaining stuff carefully now. If you get stuck or want +to know more about Lean (e.g. how to do much harder maths in Lean), +ask in `#new members` at +[the Lean chat](https://leanprover.zulipchat.com) +(login required, real name preferred). Kevin or Mohammad or one of the other +people there might be able to help. + +Good luck! Click on \"Next\" to solve some levels on your own. +" diff --git a/server/nng/NNG/Levels/Addition/Level_2.lean b/server/nng/NNG/Levels/Addition/Level_2.lean new file mode 100644 index 0000000..b49723a --- /dev/null +++ b/server/nng/NNG/Levels/Addition/Level_2.lean @@ -0,0 +1,70 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Addition" +Level 2 +Title "add_assoc (associativity of addition)" + +open MyNat + +theorem MyNat.zero_add (n : ℕ) : 0 + n = n := by + induction n with n hn + · rw [add_zero] + rfl + · rw [add_succ] + rw [hn] + rfl + +Introduction +" +It's well-known that $(1 + 2) + 3 = 1 + (2 + 3)$; if we have three numbers +to add up, it doesn't matter which of the additions we do first. This fact +is called *associativity of addition* by mathematicians, and it is *not* +obvious. For example, subtraction really is not associative: $(6 - 2) - 1$ +is really not equal to $6 - (2 - 1)$. We are going to have to prove +that addition, as defined the way we've defined it, is associative. + +See if you can prove associativity of addition. +" + +Statement add_assoc +"On the set of natural numbers, addition is associative. +In other words, for all natural numbers $a, b$ and $c$, we have +$ (a + b) + c = a + (b + c). $" + (a b c : ℕ) : (a + b) + c = a + (b + c) := by + Hint "Because addition was defined by recursion on the right-most variable, + use induction on the right-most variable (try other variables at your peril!). + + Note that when Lean writes `a + b + c`, it means `(a + b) + c`. If it wants to talk + about `a + (b + c)` it will put the brackets in explictly." + Branch + induction a + Hint "Good luck with that…" + rw [zero_add, zero_add] + rfl + Branch + induction b + Hint "Good luck with that…" + induction c with c hc + Hint (hidden := true) "look at the lemma `add_zero`." + rw [add_zero] + Hint "`rw [add_zero]` only rewrites one term of the form `… + 0`, so you might to + use it multiple times." + rw [add_zero] + rfl + Hint (hidden := true) "`add_succ` might help here." + rw [add_succ] + rw [add_succ] + rw [add_succ] + Hint (hidden := true) "Now you can use the induction hypothesis." + rw [hc] + rfl + + +Conclusion +" + +" + +NewLemma MyNat.zero_add \ No newline at end of file diff --git a/server/nng/NNG/Levels/Addition/Level_3.lean b/server/nng/NNG/Levels/Addition/Level_3.lean new file mode 100644 index 0000000..95a846d --- /dev/null +++ b/server/nng/NNG/Levels/Addition/Level_3.lean @@ -0,0 +1,66 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import NNG.Levels.Addition.Level_2 + +Game "NNG" +World "Addition" +Level 3 +Title "succ_add" + +open MyNat + +theorem MyNat.add_assoc (a b c : ℕ) : (a + b) + c = a + (b + c) := by + induction c with c hc + · rw [add_zero] + rw [add_zero] + rfl + · rw [add_succ] + rw [add_succ] + rw [add_succ] + rw [hc] + rfl + + +Introduction +" +Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add` +is the proof that `succ(a) + b = succ(a + b)` for `a` and `b` in your +natural number type. We need to prove this now, because we will need +to use this result in our proof that `a + b = b + a` in the next level. + +NB: think about why computer scientists called this result `succ_add` . +There is a logic to all the names. + +Note that if you want to be more precise about exactly where you want +to rewrite something like `add_succ` (the proof you already have), +you can do things like `rw [add_succ (succ a)]` or +`rw [add_succ (succ a) d]`, telling Lean explicitly what to use for +the input variables for the function `add_succ`. Indeed, `add_succ` +is a function: it takes as input two variables `a` and `b` and outputs a proof +that `a + succ(b) = succ(a + b)`. The tactic `rw [add_succ]` just says to Lean \"guess +what the variables are\". +" + +Statement succ_add +"For all natural numbers $a, b$, we have +$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$." + (a b : ℕ) : succ a + b = succ (a + b) := by + Hint (hidden := true) "You might again want to start by induction + on the right-most variable." + Branch + induction a + Hint "Induction on `a` will not work." + induction b with d hd + · rw [add_zero] + rfl + · rw [add_succ] + rw [hd] + rw [add_succ] + rfl + +NewLemma MyNat.add_assoc + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Addition/Level_4.lean b/server/nng/NNG/Levels/Addition/Level_4.lean new file mode 100644 index 0000000..d32acd2 --- /dev/null +++ b/server/nng/NNG/Levels/Addition/Level_4.lean @@ -0,0 +1,60 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import NNG.Levels.Addition.Level_3 + +Game "NNG" +World "Addition" +Level 4 +Title "`add_comm` (boss level)" + +open MyNat + +theorem MyNat.succ_add (a b : ℕ) : succ a + b = succ (a + b) := by + induction b with d hd + · rw [add_zero] + rfl + · rw [add_succ] + rw [hd] + rw [add_succ] + rfl + +Introduction +" +[boss battle music] + +Look in your inventory to see the proofs you have available. +These should be enough. +" + +Statement add_comm +"On the set of natural numbers, addition is commutative. +In other words, for all natural numbers $a$ and $b$, we have +$a + b = b + a$." + (a b : ℕ) : a + b = b + a := by + Branch + induction a with d hd + · rw [zero_add] + rw [add_zero] + rfl + · rw [succ_add] + rw [hd] + rw [add_succ] + rfl + induction b with d hd + · rw [zero_add] + rw [add_zero] + rfl + · rw [add_succ] + rw [hd] + rw [succ_add] + rfl + +NewLemma MyNat.succ_add + +Conclusion +" +If you got this far -- nice! You're nearly ready to make a choice: +Multiplication World or Function World. But there are just a couple +more useful lemmas in Addition World which you should prove first. +Press on to level 5. +" diff --git a/server/nng/NNG/Levels/Addition/Level_5.lean b/server/nng/NNG/Levels/Addition/Level_5.lean new file mode 100644 index 0000000..62dd561 --- /dev/null +++ b/server/nng/NNG/Levels/Addition/Level_5.lean @@ -0,0 +1,54 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import NNG.Levels.Addition.Level_4 + +Game "NNG" +World "Addition" +Level 5 +Title "succ_eq_add_one" + +open MyNat + +theorem MyNat.add_comm (a b : ℕ) : a + b = b + a := by + induction b with d hd + · rw [zero_add] + rw [add_zero] + rfl + · rw [add_succ] + rw [hd] + rw [succ_add] + rfl + +theorem MyNat.one_eq_succ_zero : (1 : ℕ) = succ 0 := by + rfl + +NewLemma MyNat.add_comm MyNat.one_eq_succ_zero + +Introduction +" +I've just added `one_eq_succ_zero` (a proof of $1 = \\operatorname{succ}(0)$) +to your list of theorems; this is true +by definition of $1$, but we didn't need it until now. + +Levels 5 and 6 are the two last levels in Addition World. +Level 5 involves the number $1$. When you see a $1$ in your goal, +you can write `rw [one_eq_succ_zero]` to get back +to something which only mentions `0`. This is a good move because $0$ is easier for us to +manipulate than $1$ right now, because we have +some theorems about $0$ (`zero_add`, `add_zero`), but, other than `1 = succ 0`, +no theorems at all which mention $1$. Let's prove one now. +" + +Statement succ_eq_add_one +"For any natural number $n$, we have +$ \\operatorname{succ}(n) = n+1$ ." + (n : ℕ) : succ n = n + 1 := by + rw [one_eq_succ_zero] + rw [add_succ] + rw [add_zero] + rfl + +Conclusion +" +Well done! On to the last level! +" diff --git a/server/nng/NNG/Levels/Addition/Level_6.lean b/server/nng/NNG/Levels/Addition/Level_6.lean new file mode 100644 index 0000000..362d261 --- /dev/null +++ b/server/nng/NNG/Levels/Addition/Level_6.lean @@ -0,0 +1,47 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import NNG.Levels.Addition.Level_5 + +Game "NNG" +World "Addition" +Level 6 +Title "add_right_comm" + +open MyNat + +Introduction +" +Lean sometimes writes `a + b + c`. What does it mean? The convention is +that if there are no brackets displayed in an addition formula, the brackets +are around the left most `+` (Lean's addition is \"left associative\"). +So the goal in this level is `(a + b) + c = (a + c) + b`. This isn't +quite `add_assoc` or `add_comm`, it's something you'll have to prove +by putting these two theorems together. + +If you hadn't picked up on this already, `rw [add_assoc]` will +change `(x + y) + z` to `x + (y + z)`, but to change it back +you will need `rw [← add_assoc]`. Get the left arrow by typing `\\l` +then the space bar (note that this is L for left, not a number 1). +Similarly, if `h : a = b` then `rw [h]` will change `a`'s to `b`'s +and `rw [← h]` will change `b`'s to `a`'s. + +Also, you can be (and will need to be, in this level) more precise +about where to rewrite theorems. `rw add_comm,` will just find the +first `? + ?` it sees and swap it around. You can target more specific +additions like this: `rw add_comm a` will swap around +additions of the form `a + ?`, and `rw add_comm a b,` will only +swap additions of the form `a + b`. +" + +Statement add_right_comm +"For all natural numbers $a, b$ and $c$, we have +$a + b + c = a + c + b$." + (a b c : ℕ) : a + b + c = a + c + b := by + rw [add_assoc] + rw [add_comm b c] + rw [←add_assoc] + rfl + +Conclusion +" +" diff --git a/server/nng/NNG/Levels/AdvAddition.lean b/server/nng/NNG/Levels/AdvAddition.lean new file mode 100644 index 0000000..cc2e95d --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition.lean @@ -0,0 +1,22 @@ +import NNG.Levels.AdvAddition.Level_1 +import NNG.Levels.AdvAddition.Level_2 +import NNG.Levels.AdvAddition.Level_3 +import NNG.Levels.AdvAddition.Level_4 +import NNG.Levels.AdvAddition.Level_5 +import NNG.Levels.AdvAddition.Level_6 +import NNG.Levels.AdvAddition.Level_7 +import NNG.Levels.AdvAddition.Level_8 +import NNG.Levels.AdvAddition.Level_9 +import NNG.Levels.AdvAddition.Level_10 +import NNG.Levels.AdvAddition.Level_11 +import NNG.Levels.AdvAddition.Level_12 +import NNG.Levels.AdvAddition.Level_13 + + +Game "NNG" +World "AdvAddition" +Title "Advanced Addition World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/AdvAddition/Level_1.lean b/server/nng/NNG/Levels/AdvAddition/Level_1.lean new file mode 100644 index 0000000..ded4dae --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_1.lean @@ -0,0 +1,30 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +theorem MyNat.succ_inj {a b : ℕ} : succ a = succ b → a = b := by simp only [succ.injEq, imp_self] + +theorem MyNat.zero_ne_succ (a : ℕ) : zero ≠ succ a := by simp only [ne_eq, not_false_iff] + +Statement succ_inj' +"" + {a b : ℕ} (hs : succ a = succ b) : a = b := by + exact succ_inj hs + +NewLemma MyNat.succ_inj MyNat.zero_ne_succ + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_10.lean b/server/nng/NNG/Levels/AdvAddition/Level_10.lean new file mode 100644 index 0000000..f9f01c7 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_10.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 10 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_11.lean b/server/nng/NNG/Levels/AdvAddition/Level_11.lean new file mode 100644 index 0000000..b4d244e --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_11.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 11 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_12.lean b/server/nng/NNG/Levels/AdvAddition/Level_12.lean new file mode 100644 index 0000000..ddc0e06 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_12.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 12 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_13.lean b/server/nng/NNG/Levels/AdvAddition/Level_13.lean new file mode 100644 index 0000000..13250ec --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_13.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 13 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_2.lean b/server/nng/NNG/Levels/AdvAddition/Level_2.lean new file mode 100644 index 0000000..1d22594 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_2.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_3.lean b/server/nng/NNG/Levels/AdvAddition/Level_3.lean new file mode 100644 index 0000000..09185a8 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_3.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_4.lean b/server/nng/NNG/Levels/AdvAddition/Level_4.lean new file mode 100644 index 0000000..6973471 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_4.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_5.lean b/server/nng/NNG/Levels/AdvAddition/Level_5.lean new file mode 100644 index 0000000..c3b8b6f --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_5.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_6.lean b/server/nng/NNG/Levels/AdvAddition/Level_6.lean new file mode 100644 index 0000000..72623d1 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_6.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_7.lean b/server/nng/NNG/Levels/AdvAddition/Level_7.lean new file mode 100644 index 0000000..1ef04a2 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_7.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_8.lean b/server/nng/NNG/Levels/AdvAddition/Level_8.lean new file mode 100644 index 0000000..09a2200 --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_8.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvAddition/Level_9.lean b/server/nng/NNG/Levels/AdvAddition/Level_9.lean new file mode 100644 index 0000000..6acbb8b --- /dev/null +++ b/server/nng/NNG/Levels/AdvAddition/Level_9.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvAddition" +Level 9 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvMultiplication.lean b/server/nng/NNG/Levels/AdvMultiplication.lean new file mode 100644 index 0000000..903e3d9 --- /dev/null +++ b/server/nng/NNG/Levels/AdvMultiplication.lean @@ -0,0 +1,13 @@ +import NNG.Levels.AdvMultiplication.Level_1 +import NNG.Levels.AdvMultiplication.Level_2 +import NNG.Levels.AdvMultiplication.Level_3 +import NNG.Levels.AdvMultiplication.Level_4 + + +Game "NNG" +World "AdvMultiplication" +Title "Advanced Multiplication World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean new file mode 100644 index 0000000..bb1d6fc --- /dev/null +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvMultiplication" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean new file mode 100644 index 0000000..f1afe1b --- /dev/null +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvMultiplication" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean new file mode 100644 index 0000000..33413e4 --- /dev/null +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvMultiplication" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean new file mode 100644 index 0000000..fa3a204 --- /dev/null +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvMultiplication" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition.lean b/server/nng/NNG/Levels/AdvProposition.lean new file mode 100644 index 0000000..8d38a47 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition.lean @@ -0,0 +1,19 @@ +import NNG.Levels.AdvProposition.Level_1 +import NNG.Levels.AdvProposition.Level_2 +import NNG.Levels.AdvProposition.Level_3 +import NNG.Levels.AdvProposition.Level_4 +import NNG.Levels.AdvProposition.Level_5 +import NNG.Levels.AdvProposition.Level_6 +import NNG.Levels.AdvProposition.Level_7 +import NNG.Levels.AdvProposition.Level_8 +import NNG.Levels.AdvProposition.Level_9 +import NNG.Levels.AdvProposition.Level_10 + + +Game "NNG" +World "AdvProposition" +Title "Advanced Proposition World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/AdvProposition/Level_1.lean b/server/nng/NNG/Levels/AdvProposition/Level_1.lean new file mode 100644 index 0000000..10868a8 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_1.lean @@ -0,0 +1,28 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "AdvProposition" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by + constructor + exact p + exact q + +NewTactic constructor + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_10.lean b/server/nng/NNG/Levels/AdvProposition/Level_10.lean new file mode 100644 index 0000000..1622db4 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_10.lean @@ -0,0 +1,36 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases + +Game "NNG" +World "AdvProposition" +Level 10 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by + by_cases p : P + · by_cases q : Q + intro h p' -- cc + assumption + intro h p' + have g : ¬ P := h q + contradiction + · by_cases q : Q + intro h p + assumption + intro h p + contradiction + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_2.lean b/server/nng/NNG/Levels/AdvProposition/Level_2.lean new file mode 100644 index 0000000..526e47a --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_2.lean @@ -0,0 +1,33 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases + +Game "NNG" +World "AdvProposition" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +set_option tactic.hygienic false + +Statement and_symm +"" + (P Q : Prop) : P ∧ Q → Q ∧ P := by + intro h + rcases h with ⟨p, q⟩ + constructor + exact q + exact p + +NewTactic rcases + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_3.lean b/server/nng/NNG/Levels/AdvProposition/Level_3.lean new file mode 100644 index 0000000..76415ec --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_3.lean @@ -0,0 +1,31 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases + +Game "NNG" +World "AdvProposition" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement and_trans +"" + (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by + intro hpq + intro hqr + rcases hpq with ⟨p, q⟩ + rcases hqr with ⟨q', r⟩ + constructor + assumption + assumption + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_4.lean b/server/nng/NNG/Levels/AdvProposition/Level_4.lean new file mode 100644 index 0000000..023bd22 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_4.lean @@ -0,0 +1,31 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases + +Game "NNG" +World "AdvProposition" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement iff_trans +"" + (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by + intro hpq + intro hqr + rcases hpq with ⟨hpq, hqp⟩ + rcases hqr with ⟨hqr, hrq⟩ + constructor + exact fun x => hqr (hpq x) -- cc + exact fun x => hqp (hrq x) -- cc + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_5.lean b/server/nng/NNG/Levels/AdvProposition/Level_5.lean new file mode 100644 index 0000000..26224e6 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_5.lean @@ -0,0 +1,34 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases + +Game "NNG" +World "AdvProposition" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement iff_trans +"" + (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by + intro hpq hqr + constructor + intro p + apply hqr.1 + apply hpq.1 + assumption + intro r + apply hpq.2 + apply hqr.2 + assumption + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_6.lean b/server/nng/NNG/Levels/AdvProposition/Level_6.lean new file mode 100644 index 0000000..01ee698 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_6.lean @@ -0,0 +1,31 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight +--import Mathlib.Logic.Basic + +Game "NNG" +World "AdvProposition" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Prop) : Q → (P ∨ Q) := by + intro q + right + assumption + +NewTactic left right + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_7.lean b/server/nng/NNG/Levels/AdvProposition/Level_7.lean new file mode 100644 index 0000000..abff8e3 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_7.lean @@ -0,0 +1,31 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight + +Game "NNG" +World "AdvProposition" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement or_symm +"" + (P Q : Prop) : P ∨ Q → Q ∨ P := by + intro h + rcases h with p | q + right + exact p + left + exact q + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_8.lean b/server/nng/NNG/Levels/AdvProposition/Level_8.lean new file mode 100644 index 0000000..fd235cc --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_8.lean @@ -0,0 +1,49 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight + +Game "NNG" +World "AdvProposition" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement and_or_distrib_left +"" + (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by + constructor + intro h + rcases h with ⟨hp, hqr⟩ + rcases hqr with q | r + left + constructor + assumption + assumption + right + constructor + assumption + assumption + intro h + rcases h with hpq | hpr + rcases hpq with ⟨p, q⟩ + constructor + assumption + left + assumption + rcases hpr with ⟨hp, hr⟩ + constructor + assumption + right + assumption + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/AdvProposition/Level_9.lean b/server/nng/NNG/Levels/AdvProposition/Level_9.lean new file mode 100644 index 0000000..d04f314 --- /dev/null +++ b/server/nng/NNG/Levels/AdvProposition/Level_9.lean @@ -0,0 +1,36 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import Std.Tactic.RCases +import NNG.MyNat.Theorems.Proposition + + + +Game "NNG" +World "AdvProposition" +Level 9 +Title "" + +open MyNat + +Introduction +" + +" + +Statement contra +"" + (P Q : Prop) : (P ∧ ¬ P) → Q := by + intro h + rcases h with ⟨p, np ⟩ + contradiction + -- rw [not_iff_imp_false] at np + -- exfalso + -- apply np + -- exact p + +NewTactic exfalso contradiction + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function.lean b/server/nng/NNG/Levels/Function.lean new file mode 100644 index 0000000..5b7a403 --- /dev/null +++ b/server/nng/NNG/Levels/Function.lean @@ -0,0 +1,18 @@ +import NNG.Levels.Function.Level_1 +import NNG.Levels.Function.Level_2 +import NNG.Levels.Function.Level_3 +import NNG.Levels.Function.Level_4 +import NNG.Levels.Function.Level_5 +import NNG.Levels.Function.Level_6 +import NNG.Levels.Function.Level_7 +import NNG.Levels.Function.Level_8 +import NNG.Levels.Function.Level_9 + + +Game "NNG" +World "Function" +Title "Function World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Function/Level_1.lean b/server/nng/NNG/Levels/Function/Level_1.lean new file mode 100644 index 0000000..18aa81f --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_1.lean @@ -0,0 +1,27 @@ +import NNG.Metadata +import NNG.MyNat.Theorems.Addition +import NNG.MyNat.Multiplication + +Game "NNG" +World "Function" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true." + (P Q : Prop) (p : P) (h : P → Q) : Q := by + exact h p + +NewTactic exact + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_2.lean b/server/nng/NNG/Levels/Function/Level_2.lean new file mode 100644 index 0000000..1e27341 --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_2.lean @@ -0,0 +1,28 @@ +import NNG.Metadata +import NNG.MyNat.Theorems.Addition +import NNG.MyNat.Multiplication + +Game "NNG" +World "Function" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : ℕ → ℕ := by + intro n + exact 3 * n + 2 + +NewTactic intro + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_3.lean b/server/nng/NNG/Levels/Function/Level_3.lean new file mode 100644 index 0000000..1dc9c55 --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_3.lean @@ -0,0 +1,31 @@ +import NNG.Metadata +import NNG.MyNat.Theorems.Addition +import NNG.MyNat.Multiplication + +Game "NNG" +World "Function" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R S T U: Type) (p : P) (h : P → Q) (i : Q → R) (j : Q → T) (k : S → T) (l : T → U) : + U := by + have q := h p + have t : T := j q + have u : U := l t + exact u + +NewTactic «have» + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_4.lean b/server/nng/NNG/Levels/Function/Level_4.lean new file mode 100644 index 0000000..ab2a23d --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_4.lean @@ -0,0 +1,37 @@ +import NNG.Metadata +import NNG.MyNat.Theorems.Addition +import NNG.MyNat.Multiplication + +Game "NNG" +World "Function" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R S T U: Type) +(p : P) +(h : P → Q) +(i : Q → R) +(j : Q → T) +(k : S → T) +(l : T → U) : U := +by + apply l + apply j + apply h + exact p + +NewTactic apply + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_5.lean b/server/nng/NNG/Levels/Function/Level_5.lean new file mode 100644 index 0000000..8f00824 --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_5.lean @@ -0,0 +1,27 @@ +import NNG.Metadata +import NNG.MyNat.Theorems.Addition +import NNG.MyNat.Multiplication + +Game "NNG" +World "Function" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Type) : P → (Q → P) := by + intro p + intro q + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_6.lean b/server/nng/NNG/Levels/Function/Level_6.lean new file mode 100644 index 0000000..7754306 --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_6.lean @@ -0,0 +1,30 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Function" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) := by + intro f + intro h + intro p + have j : Q → R := f p + apply j + apply h + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_7.lean b/server/nng/NNG/Levels/Function/Level_7.lean new file mode 100644 index 0000000..6cf284b --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_7.lean @@ -0,0 +1,29 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Function" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := by + intro f + intro h + intro p + apply h + apply f + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_8.lean b/server/nng/NNG/Levels/Function/Level_8.lean new file mode 100644 index 0000000..7a76cb5 --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_8.lean @@ -0,0 +1,27 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Function" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Type) : (P → Q) → ((Q → empty) → (P → empty)) := by + intros f h p + apply h + apply f + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Function/Level_9.lean b/server/nng/NNG/Levels/Function/Level_9.lean new file mode 100644 index 0000000..f612d41 --- /dev/null +++ b/server/nng/NNG/Levels/Function/Level_9.lean @@ -0,0 +1,36 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Function" +Level 9 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (A B C D E F G H I J K L : Type) + (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) + (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) + (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by + intro a + apply f15 + apply f11 + apply f9 + apply f8 + apply f5 + apply f2 + apply f1 + exact a + + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality.lean b/server/nng/NNG/Levels/Inequality.lean new file mode 100644 index 0000000..87a1766 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality.lean @@ -0,0 +1,25 @@ +import NNG.Levels.Inequality.Level_1 +import NNG.Levels.Inequality.Level_2 +import NNG.Levels.Inequality.Level_3 +import NNG.Levels.Inequality.Level_4 +import NNG.Levels.Inequality.Level_5 +import NNG.Levels.Inequality.Level_6 +import NNG.Levels.Inequality.Level_7 +import NNG.Levels.Inequality.Level_8 +import NNG.Levels.Inequality.Level_9 +import NNG.Levels.Inequality.Level_10 +import NNG.Levels.Inequality.Level_11 +import NNG.Levels.Inequality.Level_12 +import NNG.Levels.Inequality.Level_13 +import NNG.Levels.Inequality.Level_14 +import NNG.Levels.Inequality.Level_15 +import NNG.Levels.Inequality.Level_16 +import NNG.Levels.Inequality.Level_17 + +Game "NNG" +World "Inequality" +Title "Inequality World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Inequality/Level_1.lean b/server/nng/NNG/Levels/Inequality/Level_1.lean new file mode 100644 index 0000000..0995685 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_1.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_10.lean b/server/nng/NNG/Levels/Inequality/Level_10.lean new file mode 100644 index 0000000..a08569a --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_10.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 10 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_11.lean b/server/nng/NNG/Levels/Inequality/Level_11.lean new file mode 100644 index 0000000..b141e0f --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_11.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 11 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_12.lean b/server/nng/NNG/Levels/Inequality/Level_12.lean new file mode 100644 index 0000000..9ef7d0e --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_12.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 12 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_13.lean b/server/nng/NNG/Levels/Inequality/Level_13.lean new file mode 100644 index 0000000..5308b97 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_13.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 13 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_14.lean b/server/nng/NNG/Levels/Inequality/Level_14.lean new file mode 100644 index 0000000..4fd5211 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_14.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 14 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_15.lean b/server/nng/NNG/Levels/Inequality/Level_15.lean new file mode 100644 index 0000000..74ff4aa --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_15.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 15 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_16.lean b/server/nng/NNG/Levels/Inequality/Level_16.lean new file mode 100644 index 0000000..25d25fc --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_16.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 16 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_17.lean b/server/nng/NNG/Levels/Inequality/Level_17.lean new file mode 100644 index 0000000..f42a282 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_17.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 17 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_2.lean b/server/nng/NNG/Levels/Inequality/Level_2.lean new file mode 100644 index 0000000..597f6bd --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_2.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_3.lean b/server/nng/NNG/Levels/Inequality/Level_3.lean new file mode 100644 index 0000000..21d9865 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_3.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_4.lean b/server/nng/NNG/Levels/Inequality/Level_4.lean new file mode 100644 index 0000000..788af62 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_4.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_5.lean b/server/nng/NNG/Levels/Inequality/Level_5.lean new file mode 100644 index 0000000..3cf1b1b --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_5.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_6.lean b/server/nng/NNG/Levels/Inequality/Level_6.lean new file mode 100644 index 0000000..5b28efe --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_6.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_7.lean b/server/nng/NNG/Levels/Inequality/Level_7.lean new file mode 100644 index 0000000..bc22434 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_7.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_8.lean b/server/nng/NNG/Levels/Inequality/Level_8.lean new file mode 100644 index 0000000..8cc9b70 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_8.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Inequality/Level_9.lean b/server/nng/NNG/Levels/Inequality/Level_9.lean new file mode 100644 index 0000000..4c2afa4 --- /dev/null +++ b/server/nng/NNG/Levels/Inequality/Level_9.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Inequality" +Level 9 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication.lean b/server/nng/NNG/Levels/Multiplication.lean new file mode 100644 index 0000000..4ff6d8c --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication.lean @@ -0,0 +1,18 @@ +import NNG.Levels.Multiplication.Level_1 +import NNG.Levels.Multiplication.Level_2 +import NNG.Levels.Multiplication.Level_3 +import NNG.Levels.Multiplication.Level_4 +import NNG.Levels.Multiplication.Level_5 +import NNG.Levels.Multiplication.Level_6 +import NNG.Levels.Multiplication.Level_7 +import NNG.Levels.Multiplication.Level_8 +import NNG.Levels.Multiplication.Level_9 + + +Game "NNG" +World "Multiplication" +Title "Multiplication World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Multiplication/Level_1.lean b/server/nng/NNG/Levels/Multiplication/Level_1.lean new file mode 100644 index 0000000..c2ad14a --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_1.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_2.lean b/server/nng/NNG/Levels/Multiplication/Level_2.lean new file mode 100644 index 0000000..502e4f6 --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_2.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_3.lean b/server/nng/NNG/Levels/Multiplication/Level_3.lean new file mode 100644 index 0000000..ca45877 --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_3.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_4.lean b/server/nng/NNG/Levels/Multiplication/Level_4.lean new file mode 100644 index 0000000..e692704 --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_4.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_5.lean b/server/nng/NNG/Levels/Multiplication/Level_5.lean new file mode 100644 index 0000000..01e06dc --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_5.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_6.lean b/server/nng/NNG/Levels/Multiplication/Level_6.lean new file mode 100644 index 0000000..4eeba03 --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_6.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_7.lean b/server/nng/NNG/Levels/Multiplication/Level_7.lean new file mode 100644 index 0000000..746f3c9 --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_7.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_8.lean b/server/nng/NNG/Levels/Multiplication/Level_8.lean new file mode 100644 index 0000000..369d554 --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_8.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Multiplication/Level_9.lean b/server/nng/NNG/Levels/Multiplication/Level_9.lean new file mode 100644 index 0000000..20fb8eb --- /dev/null +++ b/server/nng/NNG/Levels/Multiplication/Level_9.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Multiplication" +Level 9 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power.lean b/server/nng/NNG/Levels/Power.lean new file mode 100644 index 0000000..54910cb --- /dev/null +++ b/server/nng/NNG/Levels/Power.lean @@ -0,0 +1,16 @@ +import NNG.Levels.Power.Level_1 +import NNG.Levels.Power.Level_2 +import NNG.Levels.Power.Level_3 +import NNG.Levels.Power.Level_4 +import NNG.Levels.Power.Level_5 +import NNG.Levels.Power.Level_6 +import NNG.Levels.Power.Level_7 +import NNG.Levels.Power.Level_8 + +Game "NNG" +World "Power" +Title "Power World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Power/Level_1.lean b/server/nng/NNG/Levels/Power/Level_1.lean new file mode 100644 index 0000000..6a9192c --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_1.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_2.lean b/server/nng/NNG/Levels/Power/Level_2.lean new file mode 100644 index 0000000..fe6698a --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_2.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_3.lean b/server/nng/NNG/Levels/Power/Level_3.lean new file mode 100644 index 0000000..7cf3d38 --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_3.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_4.lean b/server/nng/NNG/Levels/Power/Level_4.lean new file mode 100644 index 0000000..635fd22 --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_4.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_5.lean b/server/nng/NNG/Levels/Power/Level_5.lean new file mode 100644 index 0000000..e9f6dc0 --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_5.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_6.lean b/server/nng/NNG/Levels/Power/Level_6.lean new file mode 100644 index 0000000..eaf97a0 --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_6.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_7.lean b/server/nng/NNG/Levels/Power/Level_7.lean new file mode 100644 index 0000000..f5b1949 --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_7.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Power/Level_8.lean b/server/nng/NNG/Levels/Power/Level_8.lean new file mode 100644 index 0000000..0240bfd --- /dev/null +++ b/server/nng/NNG/Levels/Power/Level_8.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Power" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : true := by + trivial + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition.lean b/server/nng/NNG/Levels/Proposition.lean new file mode 100644 index 0000000..9dc768a --- /dev/null +++ b/server/nng/NNG/Levels/Proposition.lean @@ -0,0 +1,18 @@ +import NNG.Levels.Proposition.Level_1 +import NNG.Levels.Proposition.Level_2 +import NNG.Levels.Proposition.Level_3 +import NNG.Levels.Proposition.Level_4 +import NNG.Levels.Proposition.Level_5 +import NNG.Levels.Proposition.Level_6 +import NNG.Levels.Proposition.Level_7 +import NNG.Levels.Proposition.Level_8 +-- import NNG.Levels.Proposition.Level_9 -- `cc` is not ported + + +Game "NNG" +World "Proposition" +Title "Proposition World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Proposition/Level_1.lean b/server/nng/NNG/Levels/Proposition/Level_1.lean new file mode 100644 index 0000000..179f73a --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_1.lean @@ -0,0 +1,24 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 1 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Prop) (p : P) (h : P → Q) : Q := by +exact h p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_2.lean b/server/nng/NNG/Levels/Proposition/Level_2.lean new file mode 100644 index 0000000..221bf0d --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_2.lean @@ -0,0 +1,25 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 2 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + : P → P := by + intro p + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_3.lean b/server/nng/NNG/Levels/Proposition/Level_3.lean new file mode 100644 index 0000000..707f571 --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_3.lean @@ -0,0 +1,30 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 3 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R) + (j : Q → T) (k : S → T) (l : T → U) : U := by + have q := h p + have t := j q + have u := l t + exact u + +DisabledTactic apply + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_4.lean b/server/nng/NNG/Levels/Proposition/Level_4.lean new file mode 100644 index 0000000..e81b416 --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_4.lean @@ -0,0 +1,30 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 4 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R) + (j : Q → T) (k : S → T) (l : T → U) : U := by + apply l + apply j + apply h + exact p + +DisabledTactic «have» + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_5.lean b/server/nng/NNG/Levels/Proposition/Level_5.lean new file mode 100644 index 0000000..6afe937 --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_5.lean @@ -0,0 +1,27 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 5 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Prop) : P → (Q → P) := by + intro p + intro q + exact p + rfl + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_6.lean b/server/nng/NNG/Levels/Proposition/Level_6.lean new file mode 100644 index 0000000..2d71058 --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_6.lean @@ -0,0 +1,30 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 6 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) := by + intro f + intro h + intro p + have j : Q → R := f p + apply j + apply h + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_7.lean b/server/nng/NNG/Levels/Proposition/Level_7.lean new file mode 100644 index 0000000..5caa3a3 --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_7.lean @@ -0,0 +1,28 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Proposition" +Level 7 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) := by + intro hpq hqr + intro p + apply hqr + apply hpq + exact p + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_8.lean b/server/nng/NNG/Levels/Proposition/Level_8.lean new file mode 100644 index 0000000..566034c --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_8.lean @@ -0,0 +1,35 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import NNG.MyNat.Theorems.Proposition + + +Game "NNG" +World "Proposition" +Level 8 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) := by + rw [not_iff_imp_false] + rw [not_iff_imp_false] + intro f + intro h + intro p + apply h + apply f + exact p + +NewLemma not_iff_imp_false + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Proposition/Level_9.lean b/server/nng/NNG/Levels/Proposition/Level_9.lean new file mode 100644 index 0000000..3f83050 --- /dev/null +++ b/server/nng/NNG/Levels/Proposition/Level_9.lean @@ -0,0 +1,29 @@ +import NNG.Metadata +import NNG.MyNat.Addition +import NNG.MyNat.Theorems.Proposition + +Game "NNG" +World "Proposition" +Level 9 +Title "" + +open MyNat + +Introduction +" + +" + +Statement +"" + (A B C D E F G H I J K L : Prop) + (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) + (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) + (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by + -- cc -- TODO: `cc` is not ported yet. + sorry + +Conclusion +" + +" diff --git a/server/nng/NNG/Levels/Tutorial.lean b/server/nng/NNG/Levels/Tutorial.lean new file mode 100644 index 0000000..5fcd9a3 --- /dev/null +++ b/server/nng/NNG/Levels/Tutorial.lean @@ -0,0 +1,12 @@ +import NNG.Levels.Tutorial.Level_1 +import NNG.Levels.Tutorial.Level_2 +import NNG.Levels.Tutorial.Level_3 +import NNG.Levels.Tutorial.Level_4 + +Game "NNG" +World "Tutorial" +Title "Tutorial World" + +Introduction +" +" \ No newline at end of file diff --git a/server/nng/NNG/Levels/Tutorial/Level_1.lean b/server/nng/NNG/Levels/Tutorial/Level_1.lean new file mode 100644 index 0000000..13a6d5b --- /dev/null +++ b/server/nng/NNG/Levels/Tutorial/Level_1.lean @@ -0,0 +1,42 @@ +import NNG.Metadata +import NNG.MyNat.Multiplication + +Game "NNG" +World "Tutorial" +Level 1 +Title "The rfl tactic" + +Introduction +" +Each level in this game involves proving a mathematical statement. In this first level +you have three natural numbers $x, y, z$ (listed under \"Objects\") and you want to prove +$x \\cdot y + z = x \\cdot y + z$ (displayed under \"Goal\"). + +You can modify the Goal using *Tactics* until you can close (i.e. prove) it. + +The first tactic is called `rfl`, which stands for \"reflexivity\", +a fancy way of saying that it will prove any goal of the form `A = A`. It doesn't matter how +complicated `A` is, all that matters is that the left hand side is exactly equal to the right hand +side (a computer scientist would say \"definitionally equal\"). I really mean \"press the same buttons +on your computer in the same order\" equal. For example, `x * y + z = x * y + z` can be proved by `rfl`, +but `x + y = y + x` cannot. +" + +Statement +"For all natural numbers $x, y$ and $z$, we have $xy + z = xy + z$." + (x y z : ℕ) : x * y + z = x * y + z := by + Hint "In order to use the tactic `rfl` you can enter it above and hit \"Execute\"." + rfl + +NewTactic rfl +NewDefinition MyNat + +Conclusion +" +Congratulations! You completed your first verified proof! + +If you want to be reminded about the `rfl` tactic, your inventory on the right contains useful +information about things you've learned. + +Now click on \"Next\" to continue the journey. +" diff --git a/server/nng/NNG/Levels/Tutorial/Level_2.lean b/server/nng/NNG/Levels/Tutorial/Level_2.lean new file mode 100644 index 0000000..a17243e --- /dev/null +++ b/server/nng/NNG/Levels/Tutorial/Level_2.lean @@ -0,0 +1,46 @@ +import NNG.Metadata +import NNG.MyNat.Multiplication + +Game "NNG" +World "Tutorial" +Level 2 +Title "the rewrite (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. +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.)* +" + +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`. + 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 (hidden := true) + "Now both sides are identical, so you can use `rfl` to close the goal." + rfl + +NewTactic rewrite rw + +Conclusion +" +If you want to see the entire proof you created, toggle \"Editor mode\" above. + +There you can also move your cursor around the proof to see the \"state\" of the proof at this point. + +Each tactic is written on a new line and Lean is sensitive to indentation (i.e. there must be no +spaces before any of the tactics) +" diff --git a/server/nng/NNG/Levels/Tutorial/Level_3.lean b/server/nng/NNG/Levels/Tutorial/Level_3.lean new file mode 100644 index 0000000..a65e434 --- /dev/null +++ b/server/nng/NNG/Levels/Tutorial/Level_3.lean @@ -0,0 +1,71 @@ +import NNG.Metadata +import NNG.MyNat.Definition + +Game "NNG" +World "Tutorial" +Level 3 +Title "Peano axioms" + +open MyNat + +Introduction +" +Now we start from the beginning, where we don't know about addition or multiplication on `ℕ`. + +All we get is the following data: + +* a term `(0 : ℕ)`, interpreted as the zero number. +* a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after $n$\". +* the principle of mathematical induction. + +These axioms are essentially the axioms isolated by Peano which uniquely characterise the natural +numbers (we also need recursion, but we can ignore it for now). +The first axiom says that $0$ is a natural number. +The second says that there is a $\\operatorname{succ}$ function which eats a number and spits out +the number after it, so $\\operatorname{succ}(0)=1$, $\\operatorname{succ}(1)=2$ and so on. + +Peano's last axiom is the principle of mathematical induction. This is a deeper fact. +It says that if we have infinitely many true/false statements $P(0)$, $P(1)$, $P(2)$ and so on, +and if $P(0)$ is true, and if for every natural number $d$ we know that $P(d)$ implies +$P(\\operatorname{succ}(d))$, then $P(n)$ must be true for every natural number $n$. +It's like saying that if you have a long line of dominoes, and if you knock the first +one down, and if you know that if a domino falls down then the one after it will fall +down too, then you can deduce that all the dominos will fall down. One can also think +of it as saying that every natural number can be built by starting at $0$ and then applying +$\\operatorname{succ}$ a finite number of times. + +Peano's insights were firstly that these axioms completely characterise the natural numbers, +and secondly that these axioms alone can be used to build a whole bunch of other structure +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`: +" + +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`. + + Notes: + + 1) We do not need brackets for function application the way we would write + 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]`." + Branch + rewrite [← h] + Hint (hidden := true) "Now both sides are identical…" + rewrite [h] + Hint (hidden := true) "Now both sides are identical…" + rfl + +Conclusion +" +You may also be wondering why we keep writing `succ b` instead of `b + 1`. +This is because we haven't defined addition yet! +On the next level, the final level of Tutorial World, +we will introduce addition, and then we'll be ready to enter Addition World. +" diff --git a/server/nng/NNG/Levels/Tutorial/Level_4.lean b/server/nng/NNG/Levels/Tutorial/Level_4.lean new file mode 100644 index 0000000..742c5ac --- /dev/null +++ b/server/nng/NNG/Levels/Tutorial/Level_4.lean @@ -0,0 +1,68 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +Game "NNG" +World "Tutorial" +Level 4 +Title "addition" + +open MyNat + +Introduction +" +Peano defined addition $a + b$ by induction on $b$, or, more precisely, by *recursion* on $b$. +He first explained how to add $0$ to a number: this is the base case. + +* `add_zero (a : ℕ) : a + 0 = a` + +We will call this theorem `add_zero`. +More precisely, `add_zero` is the name of the *proof* of the +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 +with `add_zero`. If you ever see `x + 0` in your goal, +`rewrite [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). + +Now here's the inductive step. If you know how to add $d$ to $a$, then Peano +tells you how to add $\\operatorname{succ} (d)$ to $a$. It looks like this: + +- `add_succ (a d : ℕ) : a + (succ d) = succ (a + d)` + +What's going on here is that we assume `a + d` is already defined, and we define +`a + (succ d)` to be the number after it. +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. +" + +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` + to make progress." + Hint (hidden := true) "Explicitely, type `rewrite [add_succ]`!" + rewrite [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) "Finally both sides are identical." + rfl + +NewLemma MyNat.add_succ MyNat.add_zero + +Conclusion +" +You have finished tutorial world! If you're happy, let's move onto Addition World, +and learn about proof by induction. + +## Inspection time + +If you want to examine the proof, toggle \"Editor mode\" and click somewhere +inside the proof to see the state at that point! +" diff --git a/server/nng/NNG/Metadata.lean b/server/nng/NNG/Metadata.lean new file mode 100644 index 0000000..faf9e98 --- /dev/null +++ b/server/nng/NNG/Metadata.lean @@ -0,0 +1,5 @@ +import GameServer.Commands +import NNG.Doc.Tactics +import NNG.Doc.Lemmas +import NNG.Doc.Definitions +import NNG.Modifications.Tactics diff --git a/server/nng/NNG/Modifications/Tactics.lean b/server/nng/NNG/Modifications/Tactics.lean new file mode 100644 index 0000000..4a488bd --- /dev/null +++ b/server/nng/NNG/Modifications/Tactics.lean @@ -0,0 +1,131 @@ +import Mathlib.Lean.Expr.Basic +import NNG.MyNat.Addition +import Lean.Elab.Tactic.Basic + +/-! +# Modified `rw` + +Modify `rw` to work like `rewrite`. + +This is mainly a copy of the implementation of `rewrite` in Lean core. +-/ + +namespace MyNat + +open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic + +/-- +Modified `rw` tactic. For this game, `rw` works exactly like `rewrite`. +-/ +syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic + +@[tactic MyNat.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do + let cfg ← elabRewriteConfig stx[1] + let loc := expandOptLocation stx[3] + withRWRulesSeq stx[0] stx[2] fun symm term => do + withLocation loc + (rewriteLocalDecl term symm · cfg) + (rewriteTarget term symm cfg) + (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal") + +/-! +# Modified `induction` tactic + +Modify `induction` tactic to always show `(0 : MyNat)` instead of `MyNat.zero` and +to support the lean3-style `while` keyword. + +This is mainly copied and modified from the mathlib-tactic `induction'`. +-/ + +def rec' {P : ℕ → Prop} (zero : P 0) + (succ : (n : ℕ) → (n_ih : P n) → P (succ n)) (t : ℕ) : P t := by + induction t with + | zero => assumption + | succ n => + apply succ + assumption + +end MyNat + +namespace Lean.Parser.Tactic +open Meta Elab Elab.Tactic + +open private getAltNumFields in evalCases ElimApp.evalAlts.go in +def ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax) + (numEqs := 0) (numGeneralized := 0) (toClear : Array FVarId := #[]) : + TermElabM (Array MVarId) := do + let mut names : List Syntax := withArg[1].getArgs |>.toList + let mut subgoals := #[] + for { name := altName, mvarId := g, .. } in alts do + let numFields ← getAltNumFields elimInfo altName + let (altVarNames, names') := names.splitAtD numFields (Unhygienic.run `(_)) + names := names' + let (fvars, g) ← g.introN numFields <| altVarNames.map (getNameOfIdent' ·[0]) + let some (g, subst) ← Cases.unifyEqs? numEqs g {} | pure () + let (_, g) ← g.introNP numGeneralized + let g ← liftM $ toClear.foldlM (·.tryClear) g + for fvar in fvars, stx in altVarNames do + g.withContext <| (subst.apply <| .fvar fvar).addLocalVarInfoForBinderIdent ⟨stx⟩ + subgoals := subgoals.push g + pure subgoals + +open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in + +/-- +Modified `induction` tactic for this game. + +Usage: `induction n with d hd`. + +*(The actual `induction` tactic has a more complex `with`-argument that works differently)* +-/ +elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+) + withArg:((" with " (colGt binderIdent)+)?) + : tactic => do + let targets ← elabCasesTargets tgts.1.getSepArgs + let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved + g.withContext do + let elimInfo ← getElimInfo `MyNat.rec' + let targets ← addImplicitTargets elimInfo targets + evalInduction.checkTargets targets + let targetFVarIds := targets.map (·.fvarId!) + g.withContext do + let forbidden ← mkGeneralizationForbiddenSet targets + let mut s ← getFVarSetToGeneralize targets forbidden + let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray) + let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag) + let elimArgs := result.elimApp.getAppArgs + ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds + g.assign result.elimApp + let subgoals ← ElimApp.evalNames elimInfo result.alts withArg + (numGeneralized := fvarIds.size) (toClear := targetFVarIds) + setGoals <| (subgoals ++ result.others).toList ++ gs + +end Lean.Parser.Tactic + + +/-! # `rfl` tactic + +Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`. +-/ + +namespace MyNat + +open Lean Meta Elab Tactic + +-- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a + +/-- Modified `rfl` tactic. + +`rfl` closes goals of the form `A = A`. + +Note that teh version for this game is somewhat weaker than the real one. -/ +syntax (name := rfl) "rfl" : tactic + +@[tactic MyNat.rfl] def evalRfl : Tactic := fun _ => + liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure [] + +-- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ => +-- liftMetaTactic fun mvarId => do mvarId.refl; pure [] +-- (with_reducible rfl) + +end MyNat diff --git a/server/nng/NNG/MyNat/Addition.lean b/server/nng/NNG/MyNat/Addition.lean new file mode 100644 index 0000000..9f482f4 --- /dev/null +++ b/server/nng/NNG/MyNat/Addition.lean @@ -0,0 +1,23 @@ +import NNG.MyNat.Definition + +namespace MyNat + +open MyNat + +def add : MyNat → MyNat → MyNat + | a, 0 => a + | a, MyNat.succ b => MyNat.succ (MyNat.add a b) + +instance : Add MyNat where + add := MyNat.add + +/-- +This theorem proves that if you add zero to a MyNat you get back the same number. +-/ + +theorem add_zero (a : MyNat) : a + 0 = a := by rfl + +/-- +This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat. +-/ +theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl diff --git a/server/nng/NNG/MyNat/Definition.lean b/server/nng/NNG/MyNat/Definition.lean new file mode 100644 index 0000000..f567b27 --- /dev/null +++ b/server/nng/NNG/MyNat/Definition.lean @@ -0,0 +1,37 @@ +--import Mathlib.Tactic.Basic +--import Mathlib.Tactic.Cases + +/-- Our copy of the natural numbers called `MyNat`. -/ +inductive MyNat where +| zero : MyNat +| succ : MyNat → MyNat +deriving BEq, DecidableEq, Inhabited + +@[inherit_doc] +notation "ℕ" => MyNat +-- Note: as long as we do not import `Mathlib.Init.Data.Nat.Notation` this is fine. + +namespace MyNat + +instance : Inhabited MyNat where + default := MyNat.zero + +def myNatFromNat (x : Nat) : MyNat := + match x with + | Nat.zero => MyNat.zero + | Nat.succ b => MyNat.succ (myNatFromNat b) + +def natFromMyNat (x : MyNat) : Nat := + match x with + | MyNat.zero => Nat.zero + | MyNat.succ b => Nat.succ (natFromMyNat b) + +instance ofNat {n : Nat} : OfNat MyNat n where + ofNat := myNatFromNat n + +instance : ToString MyNat where + toString p := toString (natFromMyNat p) + +theorem zero_eq_0 : MyNat.zero = 0 := rfl + +def one : MyNat := MyNat.succ 0 diff --git a/server/nng/NNG/MyNat/Inequality.lean b/server/nng/NNG/MyNat/Inequality.lean new file mode 100644 index 0000000..1fb0956 --- /dev/null +++ b/server/nng/NNG/MyNat/Inequality.lean @@ -0,0 +1,28 @@ +import NNG.MyNat.Multiplication + +-- this is one of *three* routes to +-- canonically_ordered_comm_semiring + +namespace MyNat + +def le (a b : MyNat) := ∃ (c : MyNat), b = a + c + +-- Another choice is to define it recursively: +-- | le 0 _ +-- | le (succ a) (succ b) = le ab + +-- notation +instance : LE MyNat := ⟨MyNat.le⟩ + +theorem le_def' : MyNat.le = (.≤.) := rfl + +theorem le_iff_exists_add (a b : MyNat) : a ≤ b ↔ ∃ (c : MyNat), b = a + c := Iff.rfl + +def lt_myNat (a b : MyNat) := a ≤ b ∧ ¬ (b ≤ a) + +instance : LT MyNat := ⟨lt_myNat⟩ + +theorem lt : ∀ (a b : MyNat), a < b ↔ a ≤ b ∧ ¬b ≤ a := fun _ _ => Iff.rfl + + +end MyNat \ No newline at end of file diff --git a/server/nng/NNG/MyNat/Multiplication.lean b/server/nng/NNG/MyNat/Multiplication.lean new file mode 100644 index 0000000..53dd6b3 --- /dev/null +++ b/server/nng/NNG/MyNat/Multiplication.lean @@ -0,0 +1,17 @@ +import NNG.MyNat.Addition + +namespace MyNat + +open MyNat + +def mul : MyNat → MyNat → MyNat + | _, 0 => 0 + | a, b + 1 => a + (MyNat.mul a b) + +instance : Mul MyNat where + mul := MyNat.mul + +axiom mul_zero (a : MyNat) : a * 0 = 0 + +axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a + diff --git a/server/nng/NNG/MyNat/Power.lean b/server/nng/NNG/MyNat/Power.lean new file mode 100644 index 0000000..a1a0a01 --- /dev/null +++ b/server/nng/NNG/MyNat/Power.lean @@ -0,0 +1,21 @@ +import NNG.MyNat.Definition +namespace MyNat +open MyNat + +def pow : MyNat → MyNat → MyNat +| _, zero => one +| m, (succ n) => pow m n * m + +instance : Pow MyNat MyNat where + pow := pow + +-- notation a ^ b := pow a b + +example : (1 : MyNat) ^ (1 : MyNat) = 1 := rfl + +lemma pow_zero (m : MyNat) : m ^ (0 : MyNat) = 1 := rfl + +lemma pow_succ (m n : MyNat) : m ^ (succ n) = m ^ n * m := rfl + +end MyNat + diff --git a/server/nng/NNG/MyNat/Theorems/Addition.lean b/server/nng/NNG/MyNat/Theorems/Addition.lean new file mode 100644 index 0000000..ed685f9 --- /dev/null +++ b/server/nng/NNG/MyNat/Theorems/Addition.lean @@ -0,0 +1,45 @@ +import NNG.Metadata +import NNG.MyNat.Addition + +open MyNat + +theorem MyNat.zero_add (n : ℕ) : 0 + n = n := by + induction n with n hn + · rw [add_zero] + rfl + · rw [add_succ] + rw [hn] + rfl + +theorem MyNat.add_assoc (a b c : ℕ) : (a + b) + c = a + (b + c) := by + induction c with c hc + · rw [add_zero] + rw [add_zero] + rfl + · rw [add_succ] + rw [add_succ] + rw [add_succ] + rw [hc] + rfl + +theorem MyNat.succ_add (a b : ℕ) : succ a + b = succ (a + b) := by + induction b with d hd + · rw [add_zero] + rfl + · rw [add_succ] + rw [hd] + rw [add_succ] + rfl + +theorem MyNat.add_comm (a b : ℕ) : a + b = b + a := by + induction b with d hd + · rw [zero_add] + rw [add_zero] + rfl + · rw [add_succ] + rw [hd] + rw [succ_add] + rfl + +theorem MyNat.one_eq_succ_zero : (1 : ℕ) = succ 0 := by + rfl diff --git a/server/nng/NNG/MyNat/Theorems/Proposition.lean b/server/nng/NNG/MyNat/Theorems/Proposition.lean new file mode 100644 index 0000000..9901853 --- /dev/null +++ b/server/nng/NNG/MyNat/Theorems/Proposition.lean @@ -0,0 +1 @@ +theorem not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := by simp only diff --git a/server/nng/lake-manifest.json b/server/nng/lake-manifest.json index fee354b..7534416 100644 --- a/server/nng/lake-manifest.json +++ b/server/nng/lake-manifest.json @@ -1,3 +1,28 @@ {"version": 4, "packagesDir": "lake-packages", - "packages": [{"path": {"name": "GameServer", "dir": "./../leanserver"}}]} + "packages": + [{"git": + {"url": "https://github.com/leanprover-community/mathlib4.git", + "subDir?": null, + "rev": "fc4a489c2af75f687338fe85c8901335360f8541", + "name": "mathlib", + "inputRev?": "fc4a489c2af75f687338fe85c8901335360f8541"}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "cc915afc9526e904a7b61f660d330170f9d60dd7", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", + "name": "aesop", + "inputRev?": "master"}}, + {"path": {"name": "GameServer", "dir": "./../leanserver"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f", + "name": "std", + "inputRev?": "main"}}]} diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean index 9ff2130..942473c 100644 --- a/server/nng/lakefile.lean +++ b/server/nng/lakefile.lean @@ -3,6 +3,9 @@ open Lake DSL require GameServer from ".."/"leanserver" + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541" package NNG @[default_target]