greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

more tutorial tinkering

Browse Source
This commit is contained in:
Kevin Buzzard
2023-08-25 02:56:40 +01:00
parent 5de7fadb89
commit 89b751356e
9 changed files with 129 additions and 88 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
Game/Levels/Tutorial.lean
View File

@@ -1,16 +1,20 @@
import Game.Levels.Tutorial.L01rfl
import Game.Levels.Tutorial.L02rw
import Game.Levels.Tutorial.L03rw_practice
import Game.Levels.Tutorial.L04onetwothree
import Game.Levels.Tutorial.L05add_zero
import Game.Levels.Tutorial.L06add_succ
import Game.Levels.Tutorial.L03three_eq_sss0
import Game.Levels.Tutorial.L04add_zero
import Game.Levels.Tutorial.L05add_succ
import Game.Levels.Tutorial.L06twoaddone
import Game.Levels.Tutorial.L07twoaddtwo
World "Tutorial"
Title "Tutorial World"
Introduction
"
In this world we start introducing the natural numbers `ℕ` and addition. We will also learn some basic tactics, which are the tools we will use to prove theorems in this game.
In this world we introduce two basic tactics (`rfl` and `rw`).
We also introduce several mathematical concepts: the (natural) numbers `ℕ`,
explicit examples of numbers such as 0 and 3, and addition of two numbers.
The final boss is to prove that `2 + 2 = 4`. Good luck!
Click on \"Next\" to dive right in!
Click on \"Next\" to begin your quest.
"

4
Game/Levels/Tutorial/L01rfl.lean
View File

@@ -82,8 +82,8 @@ Conclusion
"
Congratulations! You completed your first verified proof!
If you ever want information about the `rfl` tactic, just click on `rfl`
in the inventory on the right.
Remember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,
just click on the `rfl` box in the inventory on the right. **TODO** make more precise.
Now click on \"Next\" to continue the journey.
"

6
Game/Levels/Tutorial/L02rw.lean
View File

@@ -18,12 +18,12 @@ and `h` is a secret proof of this statement (in kind of the same way that `x` is
a secret number). It is important in games like this
to have a clear separation in your mind about the difference between the
*statement* of a theorem and its *proof*. The statement is
`y = x + 7`, and the proof is `h`, and the notation is `h : y = x + 7`.
`y = x + 7`, the proof is `h`, and the notation is `h : y = x + 7`.
The goal of this level is to prove, assuming hypothesis `h`,
that $2y=2(x+7)$. Now `rfl` won't work directly.
We want to prove this theorem by first using `h` to *replace* `y` in the goal with `x + 7` and
*then* using `rfl`. The tactic which we use to
We want to prove this theorem by first using `h` to *replace* `y` in the goal with `x + 7`, and
then `rfl` gets us home. The tactic which we use to
do this kind of \"substituting in\" is called the *rewrite* tactic `rw`.
The spell `rw [h]` will replace all occurences of the left hand side $y$ of `h`
in the goal, with the right hand side $x+7$. Try it and see.

10
Game/Levels/Tutorial/L03three_eq_sss0.lean
View File

@@ -12,16 +12,16 @@ 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 the natural numbers is based on
numbers from scratch. Our definition of (natural) numbers is based on
Giuseppe Peano's, and consists of three axioms:
* `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.
The final boss of tutorial world is `2 + 2 = 4`. If you can prove this theorem,
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*
tht theorem because we haven't yet defined `2` or `+` or `4`. Let's worry about `+`
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.
# Counting to four.
@@ -29,11 +29,11 @@ later; before we learn to add we learn to count, so let's count 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).
does not *need* brackets for function inputs, although you can use them if you want after the space).
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 name for this axiom, which is `three_eq_succ_two`. This should
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\"

16
Game/Levels/Tutorial/L04add_zero.lean
View File

@@ -21,21 +21,17 @@ 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.
So firstly you have to say how to add `0` to something.
And secondly, imagine you've already said how to add `d` to something.
Then you have to explain how to add `succ d` to something. Once you've explained
those two things, \"That's it!\", or the principle of mathematical recursion,
says that you've defined how to add `y` to something for all natural numbers `y`.
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.
So we now have two jobs to do, and let's do the simplest one in this level:
let's decide how to define `x + 0`. If we want addition to agree with our intuition
we should define this to be `x`. So let's throw in a new axiom or hypothesis
or however you want to think about it, saying this:
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:
* `add_zero (a : ℕ) : a + 0 = a`
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 + r)` is a proof that `p * q + r + 0 = p * q + r`.
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:
* `add_zero : ∀ (a : ℕ), a + 0 = a`

34
Game/Levels/Tutorial/L05add_succ.lean
View File

@@ -7,18 +7,36 @@ Title "add_succ"
open MyNat
-- So firstly you have to say how to add `0` to something.
-- And secondly, imagine you've already said how to add `d` to something.
-- Then you have to explain how to add `succ d` to something. Once you've explained
-- those two things, \"That's it!\", or the principle of mathematical recursion,
-- says that you've defined how to add `y` to something for all natural numbers `y`.
-- So we now have two jobs to do, and let's do the simplest one in this level:
Introduction
"
Our remaining job if we want to cover all cases of addition,
is defining `x + succ d`, assuming that we already know the answer to `x + d`.
Clearly `x + succ d` is one more than `x + d`, so it's the number after `x + d`.
Thus it makes sense to define a family of hypotheses
We are defining addition. We have defined `x + 0` but still
need to figure out how to add successors. We need a definition for `x + succ d`,
but we are allowed to assume in our definition that we already know the
answer to `x + d`, because `d` was \"born before\" `succ d`.
Just thinking normally mathematically for a moment, `x + succ d` is one more
than `x + d`, so it's the number after `x + d`. Thus it makes sense to define
a family of hypotheses
* `add_succ (a b : ℕ) : a + succ b = succ (a + b)`
This axiom tells you that you can move a `succ` left over an `+`.
`add_succ` is a function which eats two variables and spits out a proof.
For example `add_succ 2 1` is the proof that `2 + succ 1 = succ (2 + 1)`.
The axiom tells you that you can move a `succ` left over an `+`.
We can now state the theorem about the successor function which has been
`add_zero` and `add_succ` and \"That's it!\" (the principle of mathematical
recursion) now enables us to conclude that we have defined `x + y` for all
numbers `x` and `y`.
We can also now state the theorem about the successor function which has been
part of our mental model: `succ n = n + 1`. See if you can rewrite your
way to a proof of it.
"
@@ -36,13 +54,11 @@ Statement succ_eq_add_one n : succ n = n + 1 := by
LemmaDoc MyNat.add_succ as "add_succ" in "Add"
"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
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.add_succ MyNat.succ_eq_add_one
LemmaTab "Add"
Conclusion
"You begin to hear boss music. Click next to begin the cutscene."
"You begin to hear dramatic music. Click next to begin the cutscene."

53
Game/Levels/Tutorial/L06add_succ.lean
View File

@@ -1,53 +0,0 @@
import Game.Metadata
import Game.MyNat.Addition
World "Tutorial"
Level 6
Title "add_succ"
open MyNat
Introduction
"
Peano's second axiom was this:
* `add_succ : ∀ (a b : ℕ), a + succ b = succ (a + b)`
It tells you that you can move a `succ` left over an `+`. See if you can rewrite
your way to a proof of this.
"
namespace MyNat
/-- For all natural numbers $a$, we have $a + \operatorname{succ}(0) = \operatorname{succ}(a)$. -/
Statement : a + succ 0 = succ a := by
Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
to make progress."
Hint (hidden := true) "Explicitely, you can type `rw [add_succ a 0]`
if you want to be precise, or just `rw [add_succ]` if you want Lean to figure
out the inputs to this function."
rw [add_succ]
Branch
simp?
Hint (hidden := true) "Now you see a term of the form `… + 0`, so you can use `add_zero`."
rw [add_zero]
Hint (hidden := true) "Finally both sides are identical."
rfl
LemmaDoc MyNat.add_succ as "add_succ" in "Add"
"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
NewLemma MyNat.add_succ
LemmaTab "Add"
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 your proofs, toggle \"Editor mode\" and click somewhere
inside the proof to see the state of Lean's brain at that point.
"

35
Game/Levels/Tutorial/L06twoaddone.lean Normal file
View File

@@ -0,0 +1,35 @@
import Game.Metadata
import Game.MyNat.Addition
import Game.Levels.Tutorial.L03three_eq_sss0
World "Tutorial"
Level 6
Title "2+1=3"
open MyNat
Introduction
" First you need to face the sub-boss `2 + 1 = 3`.
"
namespace MyNat
/-- $2+2=4$. -/
Statement two_add_one_eq_three : (2 : ℕ) + 1 = 3 := by
Hint (hidden := true) "`rw [one_eq_succ_zero]` unlocks `add_succ`"
rw [one_eq_succ_zero]
Hint (hidden := true) "Now you can `rw [add_succ]`"
rw [add_succ]
rw [add_zero]
rw [three_eq_succ_two]
rfl
LemmaDoc MyNat.two_add_one_eq_three as "two_add_one_eq_three" in "Add"
"`two_add_one` is the proof of `2 + 1 = 3`."
NewLemma MyNat.two_add_one_eq_three
LemmaTab "Add"
Conclusion
"
Do you think you're ready for `2 + 2 = 4`?
"

43
Game/Levels/Tutorial/L07twoaddtwo.lean Normal file
View File

@@ -0,0 +1,43 @@
import Game.Metadata
import Game.MyNat.Addition
import Game.Levels.Tutorial.L06twoaddone
World "Tutorial"
Level 7
Title "2+2=4"
open MyNat
Introduction
"
Use your tools. You only have two tactics, `rw` and `rfl`, but you have
a lot of proofs which you can rewrite. Look at your collection of proofs
on the right hand side. As you progress through the game, you will get
many more.
One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.
If you only want to change one of them, say the 37th one, then use
`nth_rewrite 37 [h]`
"
namespace MyNat
/-- $2+2=4$. -/
Statement : (2 : ℕ) + 2 = 4 := by
Hint (hidden := true) "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`."
nth_rewrite 2 [two_eq_succ_one]
Hint (hidden := true) "Now you can `rw [add_succ]`"
rw [add_succ]
Hint (hidden := true) "There is now a short way and a long way..."
rw [two_add_one_eq_three]
rw [four_eq_succ_three]
rfl
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 your proofs, toggle \"Editor mode\" and click somewhere
inside the proof to see the state of Lean's brain at that point.
"