From 04c0466fa4c9c44dcc6e40c00ec77cf7d8050e4a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 12 Dec 2022 11:13:02 +0100 Subject: [PATCH] update to lean nightly 22-12-05 --- UPDATE_LEAN.sh | 15 ++++++++++++ package.json | 2 +- server/leanserver/lake-manifest.json | 1 + server/leanserver/lean-toolchain | 2 +- server/testgame/TestGame.lean | 4 ++++ server/testgame/TestGame/Levels/Level1.lean | 8 +++---- server/testgame/TestGame/Levels/Level2.lean | 10 ++++---- server/testgame/TestGame/Levels/Level3.lean | 16 ++++++------- server/testgame/TestGame/Levels/Level4.lean | 4 ++-- server/testgame/TestGame/Levels/Level5.lean | 20 ++++++++-------- .../TestGame/Levels/Logic/L01_Rfl.lean | 2 +- .../TestGame/Levels/Logic/L02_Rfl.lean | 2 +- .../TestGame/Levels/Logic/L03_Assumption.lean | 2 +- .../Levels/Logic/L03b_Assumption.lean | 2 +- .../TestGame/Levels/Logic/L04_Rewrite.lean | 2 +- .../TestGame/Levels/Logic/L05_Apply.lean | 2 +- .../TestGame/Levels/Logic/L05b_Apply.lean | 2 +- .../TestGame/Levels/Logic/L05c_Apply.lean | 2 +- .../TestGame/Levels/Logic/L06_Iff.lean | 2 +- .../TestGame/Levels/Logic/L06b_Iff.lean | 2 +- .../TestGame/Levels/Logic/L06c_Iff.lean | 2 +- .../TestGame/Levels/Logic/L06d_Iff.lean | 2 +- .../TestGame/Levels/Logic/L07_And.lean | 2 +- .../TestGame/Levels/Logic/L08_Or.lean | 2 +- .../TestGame/Levels/Logic/L08b_Or.lean | 2 +- .../TestGame/Levels/Logic/L08c_Or.lean | 2 +- .../TestGame/Levels/Naturals/L01_Ring.lean | 8 ------- .../TestGame/Levels/Naturals/L31_Sum.lean | 23 +++++++++++++++++++ .../Levels/Naturals/L32_Induction.lean | 23 +++++++++++++++++++ .../TestGame/Levels/Naturals/L33_Prime.lean | 23 +++++++++++++++++++ .../Levels/Naturals/L34_ExistsUnique.lean | 23 +++++++++++++++++++ .../{LeftOvers => Naturals}/Lxx_Prime.lean | 0 server/testgame/TestGame/Metadata.lean | 14 ++--------- server/testgame/lake-manifest.json | 2 +- server/testgame/lean-toolchain | 2 +- 35 files changed, 163 insertions(+), 69 deletions(-) create mode 100755 UPDATE_LEAN.sh create mode 100644 server/leanserver/lake-manifest.json create mode 100644 server/testgame/TestGame/Levels/Naturals/L31_Sum.lean create mode 100644 server/testgame/TestGame/Levels/Naturals/L32_Induction.lean create mode 100644 server/testgame/TestGame/Levels/Naturals/L33_Prime.lean create mode 100644 server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean rename server/testgame/TestGame/Levels/{LeftOvers => Naturals}/Lxx_Prime.lean (100%) diff --git a/UPDATE_LEAN.sh b/UPDATE_LEAN.sh new file mode 100755 index 0000000..3ea0fe4 --- /dev/null +++ b/UPDATE_LEAN.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env sh + +# Operate in the directory where this file is located +cd $(dirname $0) + +cd server + +cd testgame +lake update + +cp lake-packages/mathlib/lean-toolchain lean-toolchain +cp lake-packages/mathlib/lean-toolchain ../leanserver/lean-toolchain + +cd ../leanserver +lake update diff --git a/package.json b/package.json index 1f6e009..55056ea 100644 --- a/package.json +++ b/package.json @@ -55,7 +55,7 @@ "build_server": "server/build.sh", "build_client": "NODE_ENV=production webpack", "production": "NODE_ENV=production node server/index.mjs", - "update_lean": "cd server && (cd testgame && lake update) && cp testgame/lean-toolchain leanserver/lean-toolchain" + "update_lean": "./UPDATE_LEAN.sh" }, "eslintConfig": { "extends": [ diff --git a/server/leanserver/lake-manifest.json b/server/leanserver/lake-manifest.json new file mode 100644 index 0000000..b2e4207 --- /dev/null +++ b/server/leanserver/lake-manifest.json @@ -0,0 +1 @@ +{"version": 4, "packagesDir": "./lake-packages", "packages": []} diff --git a/server/leanserver/lean-toolchain b/server/leanserver/lean-toolchain index 5ca06ea..a01662b 100644 --- a/server/leanserver/lean-toolchain +++ b/server/leanserver/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-12-03 +leanprover/lean4:nightly-2022-12-05 diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index 65a60a7..a2eff0d 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -19,6 +19,10 @@ import TestGame.Levels.Naturals.L01_Ring import TestGame.Levels.Naturals.L02_Ring import TestGame.Levels.Naturals.L03_Exists import TestGame.Levels.Naturals.L04_Forall +import TestGame.Levels.Naturals.L31_Sum +import TestGame.Levels.Naturals.L32_Induction +import TestGame.Levels.Naturals.L33_Prime +import TestGame.Levels.Naturals.L34_ExistsUnique import TestGame.Levels.Negation.L01_False import TestGame.Levels.Negation.L02_Contra import TestGame.Levels.Negation.L03_Contra diff --git a/server/testgame/TestGame/Levels/Level1.lean b/server/testgame/TestGame/Levels/Level1.lean index 16230d3..f1cf148 100644 --- a/server/testgame/TestGame/Levels/Level1.lean +++ b/server/testgame/TestGame/Levels/Level1.lean @@ -1,12 +1,12 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Old" Level 1 Title "The reflexivity spell" -Introduction +Introduction " Let's learn a first spell: the `rfl` spell. `rfl` stands for \"reflexivity\", which is a fancy way of saying that it will prove any goal of the form `A = A`. It doesn't matter how @@ -16,7 +16,7 @@ right hand side (a computer scientist would say \"definitionally equal\"). I rea For example, `x * y + z = x * y + z` can be proved by `rfl`, but `x + y = y + x` cannot. This is a very low level spell, but you need to start somewhere. -After closing this message, type rfl in the invocation zone and hit Enter or click +After closing this message, type rfl in the invocation zone and hit Enter or click the \"Cast spell\" button. " @@ -25,4 +25,4 @@ rfl Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button." -Tactics rfl \ No newline at end of file +Tactics rfl diff --git a/server/testgame/TestGame/Levels/Level2.lean b/server/testgame/TestGame/Levels/Level2.lean index e5c2882..9201d72 100644 --- a/server/testgame/TestGame/Levels/Level2.lean +++ b/server/testgame/TestGame/Levels/Level2.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Old" Level 2 Title "The rewriting spell" @@ -14,7 +14,7 @@ goal mentions the left hand side `A` somewhere, then the `rewrite` tactic will replace the `A` in your goal with a `B`. The documentation for `rewrite` just appeared in your spell book. -Play around with the menus and see what is there currently. +Play around with the menus and see what is there currently. More information will appear as you progress. Take a look in the top right box at what we have. @@ -26,13 +26,13 @@ this substitution using the `rewrite` spell. This spell takes a list of equaliti or equivalences so you can cast `rewrite [h]`. " -Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by +Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by rewrite [h] rfl -Message (x : ℕ) (y : ℕ) (h : y = x + 7) : 2*(x + 7) = 2*(x + 7) => +Message (x : ℕ) (y : ℕ) (h : y = x + 7) : 2*(x + 7) = 2*(x + 7) => "Great! Now the goal should be easy to reach using the `rfl` spell." Conclusion "Congratulations for completing your second level!" -Tactics rfl rewrite \ No newline at end of file +Tactics rfl rewrite diff --git a/server/testgame/TestGame/Levels/Level3.lean b/server/testgame/TestGame/Levels/Level3.lean index 63f6e75..74f3018 100644 --- a/server/testgame/TestGame/Levels/Level3.lean +++ b/server/testgame/TestGame/Levels/Level3.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Old" Level 3 Title "Peano's axioms" @@ -40,9 +40,9 @@ This game is all about seeing how far these axioms of Peano can take us. Let's practice our use of the `rewrite` tactic in the following example. Our hypothesis `h` is a proof that `succ(a) = b` and we want to prove that `succ(succ(a))=succ(b)`. In words, we're going to prove that if -`b` is the number after `a` then `succ(b)` is the number after `succ(a)`. +`b` is the number after `a` then `succ(b)` is the number after `succ(a)`. Note that the system drops brackets when they're not -necessary, so `succ b` just means `succ(b)`. +necessary, so `succ b` just means `succ(b)`. Now here's a tricky question. Knowing that our goal is `succ (succ a) = succ b`, and our assumption is `h : succ a = b`, then what will the goal change @@ -56,23 +56,23 @@ the *right* hand side. Try and figure out how the goal will change, and then try it. " -Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by +Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by rewrite [h] rfl -Message (a : ℕ) (b : ℕ) (h : succ a = b) : succ b = succ b => +Message (a : ℕ) (b : ℕ) (h : succ a = b) : succ b = succ b => " Look: Lean changed `succ a` into `b`, so the goal became `succ b = succ b`. That goal is of the form `X = X`, so you know what to do. " -Conclusion "Congratulations for completing the third level! +Conclusion "Congratulations for completing the third level! You may be wondering whether we could have just substituted in the definition of `b` and proved the goal that way. To do that, we would want to replace the right hand side of `h` with the left hand side. You do this in Lean by writing `rewrite [<- h]`. You get the left-arrow by typing `\\l` and then a space; note that this is a small letter L, -not a number 1. You can just edit your proof and try it. +not a number 1. You can just edit your proof and try it. 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 @@ -80,4 +80,4 @@ of the tutorial, we will introduce addition, and then we'll be ready to enter Addition World. " -Tactics rfl rewrite \ No newline at end of file +Tactics rfl rewrite diff --git a/server/testgame/TestGame/Levels/Level4.lean b/server/testgame/TestGame/Levels/Level4.lean index e7a7b30..ccad6c9 100644 --- a/server/testgame/TestGame/Levels/Level4.lean +++ b/server/testgame/TestGame/Levels/Level4.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Old" Level 4 Title "Addition" @@ -61,4 +61,4 @@ of the game. Serious things start in the next level." Tactics rfl rewrite -Lemmas add_succ add_zero \ No newline at end of file +Lemmas add_succ add_zero diff --git a/server/testgame/TestGame/Levels/Level5.lean b/server/testgame/TestGame/Levels/Level5.lean index dbffa88..d302491 100644 --- a/server/testgame/TestGame/Levels/Level5.lean +++ b/server/testgame/TestGame/Levels/Level5.lean @@ -2,7 +2,7 @@ import TestGame.Metadata import TestGame.Tactics Game "TestGame" -World "TestWorld" +World "Old" Level 5 Title "The induction_on spell" @@ -26,7 +26,7 @@ a reminder of the things you're now equipped with which we'll need in this world * `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_on` (see below) - + ## Spells: @@ -34,17 +34,17 @@ a reminder of the things you're now equipped with which we'll need in this world * `rewrite [h]` : if h is a proof of `A = B`, changes all A's in the goal to B's. * `induction_on n with d hd` : we're going to learn this right now. -# Important thing: +# Important thing: This is a *really* good time to check you understand about the spell book and the inventory on -the left. Eveything you need is collected in those lists. They +the left. Eveything you need is collected in those lists. They will prove invaluable as the number of theorems we prove gets bigger. On the other hand, we only need to learn one more spell to really start going places, so let's learn about that spell right now. OK so let's see induction in action. We're going to prove - `zero_add (n : ℕ) : 0 + n = n`. + `zero_add (n : ℕ) : 0 + n = n`. That is: for all natural numbers $n$, $0+n=n$. Wait $-$ what is going on here? Didn't we already prove that adding zero to $n$ gave us $n$? @@ -89,13 +89,13 @@ focussing on the top goal, ignore the other one for now, it's not changing and we're not working on it. " -Message (n : ℕ) (ind_hyp: 0 + n = n) : 0 + succ n = succ n => +Message (n : ℕ) (ind_hyp: 0 + n = n) : 0 + succ n = succ n => " Great! You solved the base case. We are now be back down -to one goal -- the inductive step. +to one goal -- the inductive step. We have a fixed natural number `n`, and the inductive hypothesis `ind_hyp : 0 + n = n` -saying that we have a proof of `0 + n = n`. +saying that we have a proof of `0 + n = n`. Our goal is to prove `0 + succ n = succ n`. In words, we're showing that if the lemma is true for `n`, then it's also true for the number after `n`. That's the inductive step. Once we've proved this inductive step, we will have proved @@ -112,7 +112,7 @@ goal with the right hand side. We do this with the `rewrite` spell. You can writ figure them out itself). " -Message (n : ℕ) (ind_hyp: 0 + n = n) : succ (0 + n) = succ n => +Message (n : ℕ) (ind_hyp: 0 + n = n) : succ (0 + n) = succ n => "Well-done! We're almost there. It's time to use our induction hypothesis. Cast @@ -125,4 +125,4 @@ Conclusion "Congratulations for completing your first inductive proof!" Tactics rfl rewrite induction_on -Lemmas add_succ add_zero \ No newline at end of file +Lemmas add_succ add_zero diff --git a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean index 7894fa6..8593cf9 100644 --- a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Logic" Level 1 Title "Aller Anfang ist... ein Einzeiler?" diff --git a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean index 8b53a51..96b187b 100644 --- a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Logic" Level 2 Title "Definitionally equal" diff --git a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean index 98acf4c..b6fa2f0 100644 --- a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Logic" Level 3 Title "Annahmen" diff --git a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean index 33afcde..c5a7e89 100644 --- a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean +++ b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean @@ -2,7 +2,7 @@ import TestGame.Metadata import Mathlib.Data.Nat.Basic -- TODO Game "TestGame" -World "TestWorld" +World "Logic" Level 4 Title "Logische Aussagen: `Prop`" diff --git a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean index 704aa5c..e5cce32 100644 --- a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean +++ b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean @@ -2,7 +2,7 @@ import TestGame.Metadata import Mathlib Game "TestGame" -World "TestWorld" +World "Logic" Level 5 Title "Rewrite" diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean index 835190e..a565449 100644 --- a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean @@ -2,7 +2,7 @@ import TestGame.Metadata import Mathlib Game "TestGame" -World "TestWorld" +World "Logic" Level 6 Title "Implikation" diff --git a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean index e8e634c..cd04ddf 100644 --- a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Logic" Level 7 Title "Implikation" diff --git a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean index bbc1e80..8c79b34 100644 --- a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean @@ -3,7 +3,7 @@ import TestGame.Metadata set_option tactic.hygienic false Game "TestGame" -World "TestWorld" +World "Logic" Level 8 Title "Implikation" diff --git a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean index ed95dc5..423f6f6 100644 --- a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean @@ -4,7 +4,7 @@ import Init.Data.ToString #check List UInt8 Game "TestGame" -World "TestWorld" +World "Logic" Level 9 Title "Genau dann wenn" diff --git a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean index d5b35cd..f2bebfb 100644 --- a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Logic" Level 10 Title "Genau dann wenn" diff --git a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean index 30d1b2a..12568f5 100644 --- a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean @@ -5,7 +5,7 @@ import Mathlib.Tactic.Cases set_option tactic.hygienic false Game "TestGame" -World "TestWorld" +World "Logic" Level 11 Title "Genau dann wenn" diff --git a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean index 693c6f2..76365ef 100644 --- a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean @@ -1,7 +1,7 @@ import TestGame.Metadata Game "TestGame" -World "TestWorld" +World "Logic" Level 12 Title "Genau dann wenn" diff --git a/server/testgame/TestGame/Levels/Logic/L07_And.lean b/server/testgame/TestGame/Levels/Logic/L07_And.lean index b321755..a5681b3 100644 --- a/server/testgame/TestGame/Levels/Logic/L07_And.lean +++ b/server/testgame/TestGame/Levels/Logic/L07_And.lean @@ -4,7 +4,7 @@ import Std.Tactic.RCases set_option tactic.hygienic false Game "TestGame" -World "TestWorld" +World "Logic" Level 13 Title "Und" diff --git a/server/testgame/TestGame/Levels/Logic/L08_Or.lean b/server/testgame/TestGame/Levels/Logic/L08_Or.lean index 94bce99..b573a12 100644 --- a/server/testgame/TestGame/Levels/Logic/L08_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08_Or.lean @@ -5,7 +5,7 @@ import Mathlib.Tactic.LeftRight --set_option tactic.hygienic false Game "TestGame" -World "TestWorld" +World "Logic" Level 14 Title "Oder" diff --git a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean index 10b5aff..7d3c3ca 100644 --- a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean @@ -8,7 +8,7 @@ import Mathlib.Tactic.LeftRight Game "TestGame" -World "TestWorld" +World "Logic" Level 15 Title "Oder - Bonus" diff --git a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean index 776831b..5fda4e2 100644 --- a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean @@ -5,7 +5,7 @@ import Mathlib.Tactic.LeftRight set_option tactic.hygienic false Game "TestGame" -World "TestWorld" +World "Logic" Level 16 Title "Oder" diff --git a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean index 00ec9aa..599ae11 100644 --- a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean +++ b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean @@ -1,14 +1,6 @@ import TestGame.Metadata import Mathlib.Tactic.Ring --- TODOs: --- Natural numbers --- even / odd --- prime --- `ring` --- sum --- induction - --set_option tactic.hygienic false Game "TestGame" diff --git a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean new file mode 100644 index 0000000..ad47fb0 --- /dev/null +++ b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean @@ -0,0 +1,23 @@ +import TestGame.Metadata +import Mathlib.Tactic.Ring + +Game "TestGame" +World "Nat2" +Level 1 + +Title "Summe" + +Introduction +" +TODO: Summe + +" + +Statement : True := by + trivial + +Conclusion +" +" + +Tactics ring diff --git a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean new file mode 100644 index 0000000..9314c64 --- /dev/null +++ b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean @@ -0,0 +1,23 @@ +import TestGame.Metadata +import Mathlib.Tactic.Ring + +Game "TestGame" +World "Nat2" +Level 2 + +Title "Induktion" + +Introduction +" +TODO: Induktion (& induktion vs rcases) + +" + +Statement : True := by + trivial + +Conclusion +" +" + +Tactics ring diff --git a/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean b/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean new file mode 100644 index 0000000..06592b4 --- /dev/null +++ b/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean @@ -0,0 +1,23 @@ +import TestGame.Metadata +import Mathlib.Tactic.Ring + +Game "TestGame" +World "Nat2" +Level 3 + +Title "Primzahlen" + +Introduction +" +TODO: Primzahl + +" + +Statement : True := by + trivial + +Conclusion +" +" + +Tactics ring diff --git a/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean new file mode 100644 index 0000000..f669cf2 --- /dev/null +++ b/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean @@ -0,0 +1,23 @@ +import TestGame.Metadata +import Mathlib.Tactic.Ring + +Game "TestGame" +World "Nat2" +Level 5 + +Title "Exists unique" + +Introduction +" +TODO: Es existiert genau eine gerade Primzahl. + +" + +Statement : True := by + trivial + +Conclusion +" +" + +Tactics ring diff --git a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean b/server/testgame/TestGame/Levels/Naturals/Lxx_Prime.lean similarity index 100% rename from server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean rename to server/testgame/TestGame/Levels/Naturals/Lxx_Prime.lean diff --git a/server/testgame/TestGame/Metadata.lean b/server/testgame/TestGame/Metadata.lean index af1f449..a8444d6 100644 --- a/server/testgame/TestGame/Metadata.lean +++ b/server/testgame/TestGame/Metadata.lean @@ -1,5 +1,4 @@ import GameServer.Commands ---import TestGame.MyNat import TestGame.TacticDocs import TestGame.LemmaDocs import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ. @@ -21,15 +20,6 @@ with a level 1 spell book. Good luck." Conclusion "There is nothing else so far. Thanks for rescuing natural numbers!" -World "w1" -World "w2" -World "w3" -World "v1" -World "v2" -World "v3" -World "v4" - -Path TestWorld → w1 → w2 → w3 -Path w1 → v1 → v2 → v3 → w3 -Path v3 → v4 +Path Logic → Nat → Contradiction +Path Nat → Nat2 diff --git a/server/testgame/lake-manifest.json b/server/testgame/lake-manifest.json index b2d80c3..dac8477 100644 --- a/server/testgame/lake-manifest.json +++ b/server/testgame/lake-manifest.json @@ -28,7 +28,7 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "a461e549ebaac0c9b6a83969bcaa982bff6adafc", + "rev": "573c745b2edb348902bf14e5b4166e50c68db8f6", "name": "mathlib", "inputRev?": "master"}}, {"git": diff --git a/server/testgame/lean-toolchain b/server/testgame/lean-toolchain index 5ca06ea..a01662b 100644 --- a/server/testgame/lean-toolchain +++ b/server/testgame/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-12-03 +leanprover/lean4:nightly-2022-12-05