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

delete/move dead code

Browse Source
This commit is contained in:
Kevin Buzzard
2023-09-26 16:23:17 +01:00
parent 1a2b99f2af
commit 107a02d6e6
21 changed files with 0 additions and 635 deletions
Download Patch File Download Diff File Expand all files Collapse all files

92
Game/Levels/Addition/Level_1.lean
View File

@@ -1,92 +0,0 @@
import Game.Metadata
import Game.MyNat.Addition
World "Addition"
Level 1
Title "the induction tactic."
--namespace MyNat
open MyNat
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`.
"
/-- For all natural numbers $n$, we have $0 + n = n$. -/
Statement MyNat.zero_add
(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]
Branch
simp? -- TODO
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
LemmaTab "Add"
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). Any of the people there might be able to help.
Good luck! Click on \"Next\" to solve some levels on your own.
"

60
Game/Levels/Addition/Level_2.lean
View File

@@ -1,60 +0,0 @@
import Game.Levels.Addition.Level_1
World "Addition"
Level 2
Title "add_assoc (associativity of addition)"
open MyNat
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.
"
/-- 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). $ -/
Statement MyNat.add_assoc
(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
-- Adding this instance to make `ac_rfl` work.
instance : Lean.IsAssociative (α := ℕ) (·+·) := ⟨MyNat.add_assoc⟩
NewLemma MyNat.zero_add
LemmaTab "Add"

53
Game/Levels/Addition/Level_3.lean
View File

@@ -1,53 +0,0 @@
import Game.Levels.Addition.Level_2
World "Addition"
Level 3
Title "succ_add"
open MyNat
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\".
"
/-- For all natural numbers $a, b$, we have
$ \operatorname{succ}(a) + b = \operatorname{succ}(a + b)$. -/
Statement MyNat.succ_add
(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]
rw [add_zero]
rfl
· rw [add_succ]
rw [hd]
rw [add_succ]
rfl
LemmaTab "Add"
Conclusion
"
"

53
Game/Levels/Addition/Level_4.lean
View File

@@ -1,53 +0,0 @@
import Game.Levels.Addition.Level_3
World "Addition"
Level 4
Title "`add_comm` (boss level)"
open MyNat
Introduction
"
[boss battle music]
Look in your inventory to see the proofs you have available.
These should be enough.
"
/-- 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$. -/
Statement MyNat.add_comm
(a b : ℕ) : a + b = b + a := by
Hint (hidden := true) "You might want to start by induction."
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
-- Adding this instance to make `ac_rfl` work.
instance : Lean.IsCommutative (α := ℕ) (·+·) := ⟨MyNat.add_comm⟩
LemmaTab "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.
"

42
Game/Levels/Addition/Level_5.lean
View File

@@ -1,42 +0,0 @@
import Game.Levels.Addition.Level_4
import Game.MyNat.DecidableEq
World "Addition"
Level 5
Title "succ_eq_add_one"
open MyNat
Introduction
"
I've just added `one_eq_succ_zero` (a proof of `1 = 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.
"
/-- For any natural number $n$, we have
$ \\operatorname{succ}(n) = n+1$ . -/
Statement MyNat.succ_eq_add_one
(n : ℕ) : succ n = n + 1 := by
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rfl
NewLemma MyNat.one_eq_succ_zero
NewDefinition One
LemmaTab "Add"
Conclusion
"
Well done! On to the last level!
"

158
Game/Levels/Addition/Level_6.lean
View File

@@ -1,158 +0,0 @@
import Game.Levels.Addition.Level_5
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.
"
attribute [simp] MyNat.add_zero
attribute [simp] MyNat.add_succ
attribute [simp] MyNat.zero_add
attribute [simp] MyNat.succ_add
-- TODO: like this, `simp` does not do assoc. and comm. and
-- I don't think it does IRL either, does it?
/-- For all natural numbers $a, b$ and $c$, we have
$a + b + c = a + c + b$. -/
Statement MyNat.add_right_comm
(a b c : ℕ) : a + b + c = a + c + b := by
Hint (hidden := true) "You want to change your goal to `a + (b + c) = _`
so that you can then use commutativity."
Branch
induction c
· Branch
simp
rw [add_zero, add_zero]
rfl
· Branch
simp [n_ih]
rw [add_succ, n_ih, add_succ, succ_add]
rfl
rw [add_assoc]
Hint "Here you need to be 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`."
Branch
ac_rfl
Branch
rw [add_comm]
Hint "`rw [add_comm]` just rewrites to first instance of `_ + _` it finds, which
is not what you want to do here. Instead you can provide the arguments explicitely:
* `rw [add_comm b c]`
* `rw [add_comm b]`
* `rw [add_comm b _]`
* `rw [add_comm _ c]`
would all have worked. You should go back and try again.
"
rw [add_comm b c]
Branch
rw [add_assoc]
rfl
rw [←add_assoc]
rfl
LemmaTab "Add"
Conclusion
"
If you have got this far, then you have become very good at
manipulating equalities in Lean.
One last thing -- didn't you think that solving this level
`add_right_comm` was boring? Check out this AI that can do it for us.
From now on, the `simp` AI becomes accessible (it's just an advanced
tactic really), and can nail some really tedious-for-a-human-to-solve
goals. For example, this level can be solved with the following:
```
theorem MyNat.add_right_comm (a b c : ℕ) : a + b + c = a + c + b := by
induction c
simp
simp [n_ih]
```
Lemmas which are clearly a simplification, like `add_zero: a + 0 = a` are marked as
`simp`-lemmas and the tactic tries to apply them (and use `rfl` at the end).
This means `simp` will get stronger the more levels you solve!
You are now done with addition world. Go back to the main menu (top left)
and decide whether to press on with multiplication world and power world
(which can be solved with `rw`, `rfl` and `induction`), or to go on
to Function World where you can learn the tactics needed to prove
goals of the form $P\\implies Q$, thus enabling you to solve more
advanced addition world levels such as $a+t=b+t\\implies a=b$. Note that
Function World is more challenging mathematically; but if you can do Addition
World you can surely do Multiplication World and Power World.
"
-- -- NOTE: I dont think this is up to date, and `simp` cannot prove the lemma below when
-- -- I tried in may 2023's mathlib.
-- If you have got this far, then you have become very good at
-- manipulating equalities in Lean. You can also now collect
-- four collectibles (or `instance`s, as Lean calls them)
-- ```
-- MyNat.addSemigroup -- (after level 2)
-- MyNat.addMonoid -- (after level 2)
-- MyNat.addCommSemigroup -- (after level 4)
-- MyNat.addCommMonoid -- (after level 4)
-- ```
-- These say that `ℕ` is a commutative semigroup/monoid.
-- In Multiplication World you will be able to collect such
-- advanced collectibles as `MyNat.commSemiring` and
-- `MyNat.distrib`, and then move on to power world and
-- the famous collectible at the end of it.
-- One last thing -- didn't you think that solving this level
-- `add_right_comm` was boring? Check out this AI that can do it for us.
-- From now on, the `simp` AI becomes accessible (it's just an advanced
-- tactic really), and can nail some really tedious-for-a-human-to-solve
-- goals. For example check out this one-line proof:
-- ```
-- example (a b c d e : ℕ ) :
-- (((a + b) + c) + d) + e = (c + ((b + e) + a)) + d := by
-- simp
-- ```
-- Imagine having to do that one by hand! The AI closes the goal
-- because it knows how to use associativity and commutativity
-- sensibly in a commutative monoid.
-- First we have to get the `AddCommMonoid` collectible,
-- which we do by saying the magic words which make Lean's type class inference
-- system give it to us.
-- -/
-- instance : add_comm_monoid mynat := by structure_helper

13
Game/Levels/Addition/add_zero_is_a_function.txt
View File

@@ -1,13 +0,0 @@
/-
I want to stress that `add_zero` is a *function*. It's a function which eats
a *number* and spits out a *proof*. More precisely, it spits out *the proof of
a theorem*. It doesn't matter what the proof *is*, that's none of your business.
It's the
For example, if we put in the number $37$ then we get out
the proof that $37 + 0 = 37$. And if we put in the number $x$
we get out a proof that $x + 0 = x$.
-/

4
Game/Levels/Addition/addition_overview
View File

@@ -1,4 +0,0 @@
The sub-bosses: (1) 2+2=4. (2) x+y=y+x. And (3) (d+f+c+a+e... :-)

3
Game/Levels/Addition/tutorial_notes.txt
View File

@@ -1,3 +0,0 @@
Need to emphasize that `add_comm` is a function.
more intro levels. Explain the difference between `rw [add_comm]` and `rw [add_comm x]`

0
Game/Levels/Addition/L10annoying.lean → Game/Levels/AdvAddition/L10annoying.lean
View File

0
Game/Levels/Addition/L11ac_rfl.lean → Game/Levels/AdvAddition/L11ac_rfl.lean
View File

0
Game/Levels/Addition/addition_notes.txt → Game/Levels/AdvAddition/addition_notes.txt
View File

0
Game/Levels/Addition/decide_level.lean → Game/Levels/AdvAddition/decide_level.lean
View File

0
Game/Levels/Addition/simultaneous_linear_equations.txt → Game/Levels/AdvAddition/simultaneous_linear_equations.txt
View File

0
Game/Levels/Multiplication/mul_left_comm.lean → Game/Levels/AdvMultiplication/mul_left_comm.lean
View File

43
Game/Levels/Tutorial/dump_this_L03rw_practice.lean
View File

@@ -1,43 +0,0 @@
import Game.Metadata
import Game.MyNat.Multiplication
import Game.MyNat.Power
World "Tutorial"
Level 3
Title "rw practice"
Introduction
"
In this level we have three hypotheses `hap : a = p`, `hbq : b = q` and `hcr : c = r`.
Use the `rw` tactic to prove that $ab + 2bc^3 + 7 = pq + 2qr^3 + 7$. Remember that `rw` eats
*proofs*, not *statements*.
Here are some more facts about `rw`.
* `rw` can take more than one proof at a time. For example try `rw [hap, hcr]`.
* If `h` is a proof of `X = Y`, then `rw [h]` changes *all* `X`s in the goal to `Y`s.
* If you want to change all `Y`s to `X`s, then try `rw [←h]`. Get the back-arrow by
typing `\\l` (`l` for left).
"
/-- If $a=p$, $b=q$ and $c=r$, then $ab+2c^3+7=pq+2r^3+7.$ -/
Statement (a b c p q r : ℕ) (hap : a = p) (hbq : b = q) (hcr : c = r) :
a * b + 2 * b * c ^ 3 + 7 = p * q + 2 * q * r ^ 3 + 7 := by
Hint "Switch to editor mode if you want to experiment with `rw` more easily.
Note that each tactic needs to start at the beginning of a line."
rw [hap, hbq, hcr]
Hint "If you didn't already, try going to editor mode, proving this
theorem with `rw [hap, hbq, hcr]` and then clicking around the commas"
rfl
Conclusion
"
In editor mode, you can click around the proof and see the state of Lean's brain at
any point in the proof.
You can also edit your proof and experiment more with it.
There is no need to use editor mode, especially if you just want to beat
the final boss.
"

25
Game/Levels/Tutorial/induction_stuff_cut_from_level
View File

@@ -1,25 +0,0 @@
The first thing one learns about numbers as a child is how to *count*. Peano's axioms give us
the ability to count: we can switch the machine
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 `rw` with this new function `succ`:

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

@@ -1,34 +0,0 @@
import Game.Metadata
import Game.MyNat.Addition
import Game.Levels.Tutorial.L05add_succ
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` but `succ_eq_add_one` is even more useful"
rw [three_eq_succ_two]
rw [succ_eq_add_one]
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
" Did you spot the two-rewrite proof? `rw [three_eq_succ_two, succ_eq_add_one]`
and then `rfl`?
Do you think you're ready for `2 + 2 = 4`?
"

27
Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt
View File

@@ -1,27 +0,0 @@
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.

5
Game/Levels/Tutorial/why_is_succ_not_add_one.txt
View File

@@ -1,5 +0,0 @@
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.

23
Game/MyNat/AddCommMonoid.lean
View File

@@ -1,23 +0,0 @@
import Game.Metadata
import Game.MyNat.Addition
namespace MyNat
-- TODO: Do we need these instances?
-- (kmb) I wanted to introduce these instances as "collectibles" as
-- one went through the "main route" from addition world to power
-- world. If you could make some extra window with those collectibles
-- in, and whenever you have an instance sorry-free it awards you
-- the collectible, that would be great! These things were just
-- precisely the oddball (to my eyes) classes which nat was an instance of,
-- but I think they would make great collectibles.
-- instance addSemigroup : AddSemigroup ℕ :=
-- {
-- zero := 0
-- }
-- MyNat.addMonoid -- (after level 2)
-- MyNat.addCommSemigroup -- (after level 4)
-- MyNat.addCommMonoid -- (after level 4)