From 9beb91412084cdf6aaaaa0930adf9f7471e2a0a5 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Fri, 22 Sep 2023 19:49:19 +0100 Subject: [PATCH] waffle edits in tutorial world intro + 1-4 --- Game.lean | 6 +- Game/Levels/Tutorial.lean | 8 +- Game/Levels/Tutorial/L01rfl.lean | 11 +- Game/Levels/Tutorial/L02rw.lean | 66 ++++----- Game/Levels/Tutorial/L03three_eq_sss0.lean | 62 ++++---- Game/Levels/Tutorial/L04add_zero.lean | 135 +++++++++++------- .../Tutorial/set_theory_rant_BLOG_THIS.txt | 27 ++++ 7 files changed, 179 insertions(+), 136 deletions(-) create mode 100644 Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt diff --git a/Game.lean b/Game.lean index e3d3702..4d14fb2 100644 --- a/Game.lean +++ b/Game.lean @@ -24,17 +24,15 @@ Introduction In this game, we will build the basic theory of the natural numbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove -that `2 + 2 = 4`. After that we'll prove that `x + y = y + x`. +that `2 + 2 = 4`. Next we'll prove that `x + y = y + x`. And at the end we'll see if we can prove Fermat's Last Theorem. -**TODO** link to github repo if I get funded We'll do this by solving levels of a computer puzzle game called `Lean`. To learn more about these puzzles, click on \"Tutorial World\". -(**TODO** ensure they can't click on level 1 directly) ## More -Open the \"Game Info\" in the burger menu on the top right for resources, +Open \"Game Info\" in the burger menu on the top right for resources, links, and ways to interact with the Lean community. " diff --git a/Game/Levels/Tutorial.lean b/Game/Levels/Tutorial.lean index 9303d4e..55eb9fd 100644 --- a/Game/Levels/Tutorial.lean +++ b/Game/Levels/Tutorial.lean @@ -1,5 +1,3 @@ -/- **TODO** need that brief apache2 and author string? --/ import Game.Levels.Tutorial.L01rfl import Game.Levels.Tutorial.L02rw import Game.Levels.Tutorial.L03three_eq_sss0 @@ -13,8 +11,8 @@ import Game.Levels.Tutorial.L07twoaddtwo This file defines Tutorial World. Like all worlds, this world has a name, a title, an introduction, and most importantly -a finite set of levels (imported above). Each level has an -associated level number defined in it, and that's what determines +a finite set of levels (imported above). Each level has a +level number defined within it, and that's what determines the order of the levels. -/ World "Tutorial" @@ -24,7 +22,7 @@ Introduction "In Tutorial World, you're going to learn how to prove theorems about numbers. The boss level of this world is to prove that `2 + 2 = 4`. -You prove theorems like this using tools called *tactics*. Each +You prove theorems by solving puzzles using tools called *tactics*. Each tactic performs a certain logical idea, and the puzzle is to prove the theorem by applying the tactics in the right order. diff --git a/Game/Levels/Tutorial/L01rfl.lean b/Game/Levels/Tutorial/L01rfl.lean index b0a20c2..3aca808 100644 --- a/Game/Levels/Tutorial/L01rfl.lean +++ b/Game/Levels/Tutorial/L01rfl.lean @@ -8,17 +8,16 @@ Title "The rfl tactic" DefinitionDoc MyNat as "ℕ" " -The natural numbers, defined as an inductive type, with two constructors: +`ℕ` is the natural numbers, defined as an inductive type, with two constructors: * `0 : ℕ` * `succ (n : ℕ) : ℕ` ## Game Implementation -*The game uses its own copy of the natural numbers, called `MyNat` or `ℕ`. -If you ever see `Nat`, then you probably need to use `(1 : ℕ)` instead of `1` somewhere to tell Lean -to work in `MyNat`.* -" +*The game uses its own copy of the natural numbers, called `MyNat` with notation `ℕ`. +It is distinct from the Lean natural numbers `Nat`, which should hopefully +never leak into the natural number game.*" NewDefinition MyNat @@ -94,5 +93,5 @@ Congratulations! You completed your first verified proof! Remember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic, just click on `rfl` in the list of tactics on the right. -Now click on \"Next\" to continue the journey. +Now click on \"Next\" to learn about the `rw` tactic. " diff --git a/Game/Levels/Tutorial/L02rw.lean b/Game/Levels/Tutorial/L02rw.lean index cbb83ce..98d8136 100644 --- a/Game/Levels/Tutorial/L02rw.lean +++ b/Game/Levels/Tutorial/L02rw.lean @@ -18,13 +18,14 @@ and `h` is a secret *proof* of that proposition, in the same kind of way that `x` and `y` are secret numbers. Before we can use `rfl`, we have to \"sub in for $y$\". -We do this in Lean by *rewriting* with the hypothesis `h`. +We do this in Lean by *rewriting* the hypothesis `h`, +using the `rw` tactic. " /-- If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$. -/ Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by - Hint "You can use `rw [h]` to replace the `y` with `x + 7`." + Hint "You can execute `rw [h]` to replace the `y` with `x + 7`." rw [h] Hint "Now `rfl` will work." rfl @@ -37,84 +38,69 @@ all `X`s in the goal to `Y`s. ## Variants -`rw [←h]` (changes `Y` to `X`) +`rw [←h]` (changes `Y` to `X`, get the back arrow by typing `\\left ` or `\\l `.) `rw [h1, h2]` (a sequence of rewrites) -`rw [h] at h2` (changes `X` to `Y` in hypothesis `h2`) -`rw [h] at h1 h2 ⊢ (rewrite at two hypotheses and the goal) +`rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`) +`rw [h] at h1 h2 ⊢ (rewrites at two hypotheses and the goal) ## Details The `rw` tactic is a way to do \"substituting in\". There are two distinct situations where you can use this tactic. -1) Basic usage: if `h : A = B` is an assumption, -and if the goal contains one or more `A`s, then `rw h` +1) Basic usage: if `h : A = B` is an assumption or +the proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]` will change them all to `B`'s. The tactic will error if there are no `A`s in the goal. -2) Advanced usage: Assumptions coming from *theorems* +2) Advanced usage: Assumptions coming from theorems often have missing pieces. For example `add_zero` -is a proof that `? + 0 = ?` because `add_zero` really a function, +is a proof that `? + 0 = ?` because `add_zero` really is a function, and we didn't give it enough inputs yet. -In this situation `rw` will look through the term -for any subterm of the form `x + 0` and the moment it +In this situation `rw` will look through the goal +for any subterm of the form `x + 0`, and the moment it finds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s. Exercise: think about why `rw [add_zero]` changes the term `(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to `0 + (x + 0) + 0 + (x + 0)` -**** UP TO HERE ***** - -. The `rw` tactic will also work with proofs of theorems -which are equalities (look for them in the drop down -menu on the left, within Theorem Statements). -For example, in world 1 level 4 -we learn about `add_zero x : x + 0 = x`, and `rw add_zero` -will change `x + 0` into `x` in your goal (or fail with -an error if Lean cannot find `x + 0` in the goal). +If you can't remember the name of an equality lemma, look it up in +the list of lemmas on the right. Important note: if `h` is not a proof of the form `A = B` or `A ↔ B` (for example if `h` is a function, an implication, or perhaps even a proposition itself rather than its proof), then `rw` is not the tactic you want to use. For example, -`rw (P = Q)` is never correct: `P = Q` is the true-false -statement itself, not the proof. -If `h : P = Q` is its proof, then `rw h` will work. +`rw (P = Q)` is never correct: `P = Q` is the theorem *statement*, +not the proof. If `h : P = Q` is the proof, then `rw [h]` will work. -Pro tip 1: If `h : A = B` and you want to change -`B`s to `A`s instead, try `rw ←h` (get the arrow with `\\l` and -note that this is a small letter L, not a number 1). ### Example: -If it looks like this in the top right hand box: +If you have the assumption `h : x = y + y` and your goal is ``` -x y : mynat -h : x = y + y -⊢ succ (x + 0) = succ (y + y) +succ (x + 0) = succ (y + y) ``` then -`rw add_zero,` +`rw [add_zero]` -will change the goal into `⊢ succ x = succ (y + y)`, and then +will change the goal into `succ x = succ (y + y)`, and then -`rw h,` +`rw [h]` -will change the goal into `⊢ succ (y + y) = succ (y + y)`, which -can be solved with `refl,`. +will change the goal into `succ (y + y) = succ (y + y)`, which +can be solved with `rfl,`. ### Example: You can use `rw` to change a hypothesis as well. -For example, if your local context looks like this: +For example, if you have two hypotheses ``` -x y : mynat h1 : x = y + 3 h2 : 2 * y = x -⊢ y = 3 ``` -then `rw h1 at h2` will turn `h2` into `h2 : 2 * y = y + 3`. +then `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`. -/ " @@ -122,7 +108,7 @@ NewTactic rw Conclusion " -If you want to inspect the proof you created, toggle \"Editor mode\" by clicking +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 around the proof and see the state of Lean's brain at any point. If you want to go back to interactive mode with hints, click the button again. diff --git a/Game/Levels/Tutorial/L03three_eq_sss0.lean b/Game/Levels/Tutorial/L03three_eq_sss0.lean index 7ed596c..ce12ef6 100644 --- a/Game/Levels/Tutorial/L03three_eq_sss0.lean +++ b/Game/Levels/Tutorial/L03three_eq_sss0.lean @@ -10,34 +10,34 @@ namespace MyNat Introduction " -The goals of the previous levels in the tutorial mentioned things like addition and -multiplication of numbers. But now we start the game itself: building -numbers from scratch. Our definition of (natural) numbers is based on -Giuseppe Peano's, and consists of three axioms: + +# The birth of number. + +Now you know some tactics, let's begin the game. We were talking +about numbers in the previous levels, but now let's go back to basics. +What are numbers? Numbers in Lean can be defined by three axioms, an +idea going back to Giuseppe Peano. Here are the first two of them. * `0` is a number. -* If `n` is a number, then the *successor* `succ n` of `n` (that is, the number after `n`) is a number. -* That's it. +* If `n` is a number, then the *successor* `succ n` of `n` (that is, the number after `n`) +is a number. -The final boss of this world is `2 + 2 = 4`. If you can prove this theorem, -you've mastered the basics. Our problem right now is that we cannot even *state* -the theorem because we haven't yet defined `2` or `+` or `4`. Let's worry about `+` -later; before we learn to add we learn to count, so let's count to four. +What numbers can we make in this system? Let's figure out how to count, +and name a few small numbers. # Counting to four. -What kind of numbers can we make from Peano's axioms? Well, Peano gives us the number `0` for free, -but the only other thing we have is this successor function, which eats a number and -spits out the number after it. So we could *define* `1` to be `succ 0` (Note that Lean -does not *need* brackets for function inputs, although you can use them if you want after the space). +The first axiom gives us the number `0` for free. The other gives us +the successor function `succ`. If we apply this function to `0` +then we get a new number `succ 0`, the number after `0`. Let's +call this new number `1`. -Let's define `2` to be `succ 1`, `3` to be `succ 2` and `4` to be `succ 3`. -You can think of a statement like `3 = succ 2` as an axiom or hypothesis, and -this game has a special name for this hypothesis, which is `three_eq_succ_two`. This should -be the first theorem you rewrite with in the proof of the theorem below; -the natural flow of the proof is to break down the larger more complex numbers -into simpler ones, and ultimately down to a hugely inefficient \"normal form\" -`succ (succ (succ (succ ... 0))..) +We can define `2` to be `succ 1`, then set `3 = succ 2` and `4 = succ 3`. +This gives us plenty of numbers to be getting along with. + +You can think of a statement like `3 = succ 2` as an axiom or hypothesis or +theorem, and this game has a special name for the proof of this theorem: +it's called `three_eq_succ_two`. Use the `rw` tactic to prove that 3 is the number after the number after the number after 0. @@ -45,8 +45,8 @@ Use the `rw` tactic to prove that 3 is the number after the number after the num /-- $3=\operatorname{succ}\operatorname{succ}(\operatorname{succ}(0))$. -/ Statement : 3 = succ (succ (succ 0)) := by - Hint "Take a look at the names of the proofs in the `numerals` tab on the right. - Start to think about how to guess the names of proofs automatically." + Hint "Use the lemmas in the *numerals* section to break `3` down into + basic pieces." rw [three_eq_succ_two] rw [two_eq_succ_one] rw [one_eq_succ_zero] @@ -56,17 +56,25 @@ LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "numerals" "`one_eq_succ_zero` is a proof of `1 = succ 0`." LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "numerals" -"`two_eq_succ_one is a proof of `2 = succ 1`." +"`two_eq_succ_one` is a proof of `2 = succ 1`." LemmaDoc MyNat.three_eq_succ_two as "three_eq_succ_two" in "numerals" -"`three_eq_succ_two is a proof of `3 = succ 2`." +"`three_eq_succ_two` is a proof of `3 = succ 2`." LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals" -"`four_eq_succ_three is a proof of `4 = succ 3`." +"`four_eq_succ_three` is a proof of `4 = succ 3`." LemmaDoc MyNat.five_eq_succ_four as "five_eq_succ_four" in "numerals" -"`five_eq_succ_four is a proof of `5 = succ 4`." +"`five_eq_succ_four` is a proof of `5 = succ 4`." + +-- **todo** do we need 5? NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two MyNat.four_eq_succ_three MyNat.five_eq_succ_four LemmaTab "numerals" + +Conclusion +" +Why did we not just define `succ n` to be `n + 1`? Because we have not +even *defined* addition yet! We'll do that in the next level. +" diff --git a/Game/Levels/Tutorial/L04add_zero.lean b/Game/Levels/Tutorial/L04add_zero.lean index daf7f69..1a820b0 100644 --- a/Game/Levels/Tutorial/L04add_zero.lean +++ b/Game/Levels/Tutorial/L04add_zero.lean @@ -10,81 +10,108 @@ open MyNat Introduction " -We have defined all the numbers up to 4 (note that in this game, by \"number\" - I *always* mean \"natural number\"), but we still cannot state - the theorem that `2 + 2 = 4` because we have not yet defined addition. - Let's now fix this. +We have defined all the numbers up to 4, but we still cannot *state* + the theorem that `2 + 2 = 4` because we haven't yet defined addition. + Before we do this, we need to informally introduce the final axiom + used in this game. + +# \"There's only two ways to make numbers\" + + Peano's third axiom, informally, says that `0` and `succ` are *the + only ways to make numbers*. More precisely: if we want to do something + for *every number*, then all we have to do is two things: + + * Do it for `0`. + + * Assuming we've done it for `n`, do it for `succ n`. + + The axiom then guarantees that we've done it for all numbers. # The definition of addition -Say `x` and `y` are numbers. How are we going to define `x + y`? -This is where Peano's third axiom comes in. \"That's it\" means -that if you want to define how to add `y` to something, you only have -to say how to do it in the two ways that numbers can be born. -More explicitly, you have to explain how to add zero to something, and how to add -a successor to something. So let's start with adding zero. +Let's try and define the function which adds `37` to a number, using +this principle. We have to do two things. -We need to decide how to define `x + 0`. We want addition to agree with our intuition, -so we should define `x + 0` to be `x`. Let's throw in a new axiom or hypothesis -or proof or however you want to think about it, saying this: +* We must define `37 + 0`. -* `add_zero (a : ℕ) : a + 0 = a` +* If we already know what `37 + n` is, we must define `37 + succ n`. -In fact `add_zero` is a *family* of proofs. For example `add_zero 37` is a proof -that `37 + 0 = 37`, and `add_zero (p * q)` is a proof that `p * q + 0 = p * q`. -Mathematicians might encourage you to think of `add_zero` as just one proof: +# Adding 0 -* `add_zero : ∀ (a : ℕ), a + 0 = a` +To make addition agree with our intuition, we should define `37 + 0` +to be `37`. More generally, we should define `x + 0` to be `x` for +any number `x`. The name of this hypothesis in Lean is `add_zero x`. -but here it is very helpful to invoke the principle coming from computer science -(not always true, but true here) that a proof is the same as a function. Lean -is a functional programming language and you should think of `add_zero` as a function -which eats a number and spits out a proof. +`add_zero 37 : 37 + 0 = 37` + +`add_zero x : x + 0 = x` + +You can think of `add_zero` as a function which eats a number, and spits +out a proof about that number. " namespace MyNat -/-- $a+(0+0)+(0+0+0)=a.$ -/ -Statement (a : ℕ) : (a + (0 + 0)) + (0 + 0 + 0) = a := by - Hint "I will walk you through this level so I can show you some - techniques which will speed up your proving. - - This is an annoying goal. One of `rw [add_zero a]` and `rw [add_zero 0]` - will work, but not the other. Can you figure out which? Try the one - that works." - Branch - rw [add_zero 0] - Hint "Walkthrough: Now `rw [add_zero a]` will work, so try that next." - rw [add_zero a] - Hint "OK this is getting old really quickly. And if we end up with more complex - goals and have to type weird stuff like `rw [add_zero (a + 0)]` it will be - even worse. - - Fortunately `rw` can do smart rewriting. Go back to the very start - of this proof by clicking \"Delete\" to remove all the moves you've - made so far and then try `rw [add_zero]` few times. Then delete all of - these and try `repeat rw [add_zero]`. - " - repeat rw [add_zero] - Hint "`rw [add_zero]` will change `? + 0` into `?` - where `?` is arbitrary; `rw` will use the - first solution which matches for `?`." +/-- $a+(b+0)+(c+0)=a+b+c.$ -/ +Statement (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by + Hint "`rw [add_zero b]` will change `b + 0` into `b`." + repeat rw [add_zero b] + Hint "`rw [add_zero]` will change `? + 0` into `?` for the first value of `?` which works." + rw [add_zero] rfl +Conclusion "Those of you interested in speedrunning the game may want to know +that `repeat rw [add_zero]` will do both rewrites at once." + + + +DefinitionDoc Add as "+" "`Add a b`, with notation `a + b`, is +the usual sum of natural numbers. Internally it is defined by +recursion on b, with the two \"equation lemmas\" being + +* `add_zero a : a + 0 = a` + +* `add_succ a b : a + succ b = succ (a + b) + +Other theorems about naturals, such as `zero_add a : 0 + a = a`, are proved +by induction from these two basic theorems." + +NewDefinition Add + +LemmaTab "Add" + LemmaDoc MyNat.add_zero as "add_zero" in "Add" "`add_zero n` is a proof that `n + 0 = n`. -This is one of the two axioms for addition." +You can think of `add_zero` as a function, which +eats a number, and returns a proof of a theorem +about that number. For example `add_zero 37` is +a proof that `37 + 0 = 37`. -DefinitionDoc Add as "+" "`Add a b`, with notation `a + b`, is -the usual sum of natural numbers. Internally it is defined by -induction on one of the variables, but that is an implementation issue; -All you need to know is that `add_zero` and `zero_add` are both theorems." +A mathematician sometimes thinks of `add_zero` +as \"one thing\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$$`." NewLemma MyNat.add_zero + +TacticDoc «repeat» " +## Summary + +`repeat t` repeatedly applies the tactic `t` +to the goal. + +## Example + +`repeat rw [add_zero]` will turn the goal +`⊢ a + 0 + (0 + (0 + 0)) = b + 0 + 0` +into the goal +`⊢ a = b` + +## Variant + +`repeat' t` applies `t` to all subgoals +more reliably. +" NewTactic «repeat» -- TODO: Do we want it to be unlocked here? -NewDefinition Add -LemmaTab "Add" Conclusion " diff --git a/Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt b/Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt new file mode 100644 index 0000000..065569c --- /dev/null +++ b/Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt @@ -0,0 +1,27 @@ + +A set theorist would object to the idea of `add_zero` +being an actual *function*. But in Lean, a *theorem statement +is a set too*, and the elements of the set are the proofs +of the statement. In particular it's totally fine to have +a function sending a number to a proof. + +An *extremely pedantic* set theorist would object to the +use of the word \"function\" because the target space appears +to be the \"set of all proofs\" and it's a *theorem* that +there is no set of all groups, so how do we know there is +definitely a set of all proofs as formalised within ZFC set +theory. And we say no of course we don't want to consider +all proofs at once, the idea is that the input is a natural +number `n` and the output is a proof that `n + 0 = n`. +And the *extremely extremely pedantic* set theorist would +then say that the target set, namely the theorem +statement `n + 0 = n`, depends on the *input* from source set! +A function from `X` to `Y` means that you have to say +in advance what `Y` is, you can't let `Y` change according +to the input! And so you tell this extremely extremely pedantic +set theorist that technically you're right and it's +actually a section of a fibre bundle `add_zero → ℕ`, or +equivalently a function sending a natual number `n` to a proof +of `n + 0 = n`, the fibre of `add_zero → ℕ` at `n`. + +This is one of the two axioms for addition.