From 2d16f7f3b39a1e9b8d3687f18b753ae9c80904d9 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 23 Oct 2023 13:08:52 +0100 Subject: [PATCH] removing some TODOs --- Game/Levels/Addition.lean | 10 ++++------ Game/Levels/Addition/L05add_right_comm.lean | 15 +++++---------- Game/Levels/Tutorial/L02rw.lean | 19 ------------------- Game/Levels/Tutorial/L07add_succ.lean | 2 -- Game/Levels/Tutorial/L08twoaddtwo.lean | 16 +++++++++------- 5 files changed, 18 insertions(+), 44 deletions(-) diff --git a/Game/Levels/Addition.lean b/Game/Levels/Addition.lean index a22e6cc..6597b8f 100644 --- a/Game/Levels/Addition.lean +++ b/Game/Levels/Addition.lean @@ -15,10 +15,8 @@ This will enable us to defeat the boss level of this world, namely `x + y = y + The tactics `rw`, `rfl` and `induction` are the only tactics you'll need to beat all the levels in Addition World, Multiplication World, and Power World. Power World contains the final boss of the game. -" --- **TODO** put this comment back when it becomes true --- There are plenty more tactics in this game, but you'll only need to know them if you --- want to explore the game further (for example if you decide to 100% --- the game). --- " +There are plenty more tactics in this game, but you'll only need to know them if you +want to explore the game further (for example if you decide to 100% +the game). +" diff --git a/Game/Levels/Addition/L05add_right_comm.lean b/Game/Levels/Addition/L05add_right_comm.lean index 4a4f28e..b817e9f 100644 --- a/Game/Levels/Addition/L05add_right_comm.lean +++ b/Game/Levels/Addition/L05add_right_comm.lean @@ -39,14 +39,9 @@ LemmaTab "Add" Conclusion " You've now seen all the tactics you need to beat the final boss of the game. -You can begin the journey towards this boss by entering Multiplication -World. -" - -/- -Or you can go off the beaten track and learn some new tactics in Advanced -Addition World (except that ). These tactics let you prove more facts about addition, such as -how to deduce `a = b` from `x + a = x + b`. --/ +You can begin the journey towards this boss by entering Multiplication World. --- **TODO** choose a better example from advanced addition world once it's written +Or you can go off the beaten track and learn some new tactics in Implication +World. These tactics let you prove more facts about addition, such as +how to deduce `a = 0` from `x + a = x`. +" diff --git a/Game/Levels/Tutorial/L02rw.lean b/Game/Levels/Tutorial/L02rw.lean index 744c290..d6e0cef 100644 --- a/Game/Levels/Tutorial/L02rw.lean +++ b/Game/Levels/Tutorial/L02rw.lean @@ -167,22 +167,3 @@ Statement Conclusion "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey. " -/- - -**TODO** where to put this? Not this early. - -You can now press on by clicking \"Next\", but if you want to inspect the -proof you just created, toggle \"Editor mode\" by clicking -on the `` button in the top right. In editor mode, -you can click or move your cursor around the proof to see the state of Lean's brain at any point. -If you want to go back to the default (command line) mode with hints, -click the button again (it now displays `>_`). - -In editor mode, note that 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). - -If you are just learning the game, I would recommend staying in command -line mode in general, because you do not get hints during a level -in editor mode, and hints are used to teach new tactics. -" --/ diff --git a/Game/Levels/Tutorial/L07add_succ.lean b/Game/Levels/Tutorial/L07add_succ.lean index 1f253e1..808827b 100644 --- a/Game/Levels/Tutorial/L07add_succ.lean +++ b/Game/Levels/Tutorial/L07add_succ.lean @@ -18,8 +18,6 @@ NewLemma MyNat.add_succ LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add" "`succ_eq_add_one n` is the proof that `succ n = n + 1`." -NewLemma MyNat.succ_eq_add_one - Introduction " Every number in Lean is either 0 or a successor. We know how to add $0$, diff --git a/Game/Levels/Tutorial/L08twoaddtwo.lean b/Game/Levels/Tutorial/L08twoaddtwo.lean index 9c8413a..3ef8a0d 100644 --- a/Game/Levels/Tutorial/L08twoaddtwo.lean +++ b/Game/Levels/Tutorial/L08twoaddtwo.lean @@ -48,13 +48,7 @@ Statement : (2 : ℕ) + 2 = 4 := by Conclusion " -Below is an example proof showing off various techniques. You can copy -and paste it directly into Lean if you switch into editor mode, and then -you can inspect it by clicking around within the proof or moving your cursor -down the lines. -Click on `` and `>_` in the top right to switch between editor mode -and command line mode. Switch back to command line mode -when you've finished, if you prefer to see hints. +Here is an example proof of 2+2=4 showing off various techniques. ```lean nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`. @@ -66,6 +60,14 @@ rw [← four_eq_succ_three] rfl ``` +Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking +on the `` button in the top right. You can now see your proof +written as several lines of code. Move your cursor between lines to see +the goal state at any point. Now cut and paste your code elsewhere if you +want to save it, and paste the above proof in instead. Move your cursor +around to investigate. When you've finished, click the `>_` button to +move back into command line mode. + You have finished tutorial world! Now let's move onto Addition World, and learn the `induction` tactic. "