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

General organising

Browse Source
This commit is contained in:
Kevin Buzzard
2023-10-01 21:25:20 +01:00
parent 4dc5f5fb10
commit 3ffa370ade
22 changed files with 63 additions and 92 deletions
Download Patch File Download Diff File Expand all files Collapse all files

162
Game/Levels/OldProposition/FuncProgram.lean Normal file
View File

@@ -0,0 +1,162 @@
/-
Ideas for functional program world.
-/
import Mathlib.Tactic
/-
Tactics this needs: `intro` (could be removed if
required, only ever the first line in a tactic,
-/
/-
# Bonus Peano Axioms level
Explain that Peano had two extra axioms:
succ_inj (a b : ℕ) :
succ a = succ b → a = b
zero_ne_succ (a : ℕ) :
zero ≠ succ a
In Lean we don't need these axioms though, because they
follow from Lean's principles of reduction and recursion.
Principle of recursion: if two things are true:
* I know how to do it for 0
* Assuming (only) that I know how to do it for n.
I know how to do it for n+1.
Note the "only".
-/
#check Nat.succ
-- example of a definition by recursion
def double : ℕ → ℕ
| 0 => 0
| (n + 1) => 2 + double n
theorem double_eq_two_mul (n : ℕ) : double n = 2 * n := by
induction' n with d hd -- need hacked induction' so that it gives `0` not `Nat.zero`
show 0 = 2 * 0 -- system should do this
norm_num -- needs to be taught
show 2 + double d = 2 * d.succ
rw [hd]
rw [Nat.succ_eq_add_one] -- `ring` should do this
ring--
-- So you're happy that this is a definition by recursion
def f : ℕ → ℕ
| 0 => 37
| (n + 1) => (f n * 42 + 691)^2
-- So you're happy that this is a definition by recutsion
def pred : ℕ → ℕ
| 0 => 37
| (n + 1) => n
lemma pred_succ : pred (n.succ) = n :=
rfl -- true by definition
/-
## pred
pred(x)=x-1, at least when x > 0. If x=0 then there's no
answer so we just let the answer be a junk value because
it's the simplest way of dealing with this case.
If a mathematician asks us what pred of 0 is, we tell
them that it's a stupid question by saying 37, it's
like a poo emoji. But Peano was a cultured mathematician
and this proof of `succ_inj` will only use `pred` on
positive naturals, just like today's cultured mathematician
never divides by zero.
We need to learn how to deal wiht a goal of the form `P → Q`
-/
lemma succ_inj (a b : ℕ) : a.succ = b.succ → a = b := by
-- assume `a.succ=b.succ`
intro this
-- apply pred to both sides
apply_fun pred at this
-- pred and succ cancel by lemma `pred_succ`
rw [pred_succ, pred_succ] at this
-- and we're done
exact this
lemma succ_inj' (a b : ℕ) : a.succ = b.succ → a = b := by
intro h
apply_fun pred at h
-- `exact` works up to definitional equality, and
-- pred (succ n) = n is true *by definition*
-- (this is why the proof is `rfl`)
exact h
lemma succ_inj'' (a b : ℕ) : a.succ = b.succ → a = b := by
intro h
-- `apply_fun` is just a wrapper for congrArg.
-- congrArg : (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂
-- This is a fundamental property of equality.
-- You prove it by induction on equality, by the way.
-- But that's a story for another time.
apply congrArg pred h
-- functional programming point of view: the proof is just
-- a function applied to a function whose output
-- is another function.
lemma succ_inj''' (a b : ℕ) : a.succ = b.succ → a = b :=
congrArg pred
/-
Poss boring
## Interlude ; 3n+1 problem
unsafe def collatz : ℕ → ℕ
| 0 => 37
| 1 => 37
| m => if m % 2 = 0 then collatz (m / 2) else collatz (3 * m + 1)
-- theorem proof_of_collatz_conjecture : ∀ n, ∃ (t : ℕ), collatz ^ t n = 1 := by
-- sorry
Here is a crank proof I was sent of the 3n+1
problem. Explanaiton of problem. Proof: By induction.
Define f(1)=stop.
Got to prove that for all n, it terminates.
For even numbers this is obvious so they're all done.
For odd numbers, if n is odd then 3n+1 is even, but
as we already observed it's obvious for all even numbers,
so we're done.
## zero_ne_succ
zero_ne_succ (a : ℕ) :
zero ≠ succ a
What does `≠` even *mean*?
By *definition*, `zero ≠ succ a` *means* `zero = succ a → false`
-/
def is_zero : ℕ → Bool
| 0 => Bool.true
| (n + 1) => Bool.false
lemma is_zero_zero : is_zero 0 = true := rfl
lemma is_zero_succ : is_zero (n + 1) = false := rfl
lemma zero_ne_succ (n : ℕ) : 0 ≠ n.succ := by
by_contra h
apply_fun is_zero at h
rw [is_zero_zero, is_zero_succ] at h
cases h -- splits into all the cases where this is true

51
Game/Levels/OldProposition/Level_1.lean Normal file
View File

@@ -0,0 +1,51 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 1
Title "the `exact` tactic"
open MyNat
Introduction
"
What's going on in this world?
We're going to learn about manipulating propositions and proofs.
Fortunately, we don't need to learn a bunch of new tactics -- the
ones we just learnt (`exact`, `intro`, `have`, `apply`) will be perfect.
The levels in proposition world are \"back to normal\", we're proving
theorems, not constructing elements of sets. Or are we?
"
/-- If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true. -/
Statement
(P Q : Prop) (p : P) (h : P → Q) : Q := by
Hint
"
In this situation, we have true/false statements $P$ and $Q$,
a proof $p$ of $P$, and $h$ is the hypothesis that $P\\implies Q$.
Our goal is to construct a proof of $Q$. It's clear what to do
*mathematically* to solve this goal, $P$ is true and $P$ implies $Q$
so $Q$ is true. But how to do it in Lean?
Adopting a point of view wholly unfamiliar to many mathematicians,
Lean interprets the hypothesis $h$ as a function from proofs
of $P$ to proofs of $Q$, so the rather surprising approach
```
exact h p
```
works to close the goal.
Note that `exact h P` (with a capital P) won't work;
this is a common error I see from beginners. \"We're trying to solve `P`
so it's exactly `P`\". The goal states the *theorem*, your job is to
construct the *proof*. $P$ is not a proof of $P$, it's $p$ that is a proof of $P$.
In Lean, Propositions, like sets, are types, and proofs, like elements of sets, are terms.
"
exact h p

64
Game/Levels/OldProposition/Level_2.lean Normal file
View File

@@ -0,0 +1,64 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 2
Title "intro"
open MyNat
Introduction
"
Let's prove an implication. Let $P$ be a true/false statement,
and let's prove that $P\\implies P$. You can see that the goal of this level is
`P → P`. Constructing a term
of type `P → P` (which is what solving this goal *means*) in this
case amounts to proving that $P\\implies P$, and computer scientists
think of this as coming up with a function which sends proofs of $P$
to proofs of $P$.
To define an implication $P\\implies Q$ we need to choose an arbitrary
proof $p : P$ of $P$ and then, perhaps using $p$, construct a proof
of $Q$. The Lean way to say \"let's assume $P$ is true\" is `intro p`,
i.e., \"let's assume we have a proof of $P$\".
## Note for worriers.
Those of you who know
something about the subtle differences between truth and provability
discovered by Goedel -- these are not relevant here. Imagine we are
working in a fixed model of mathematics, and when I say \"proof\"
I actually mean \"truth in the model\", or \"proof in the metatheory\".
## Rule of thumb:
If your goal is to prove `P → Q` (i.e. that $P\\implies Q$)
then `intro p`, meaning \"assume $p$ is a proof of $P$\", will make progress.
"
/-- If $P$ is a proposition then $P\\implies P$. -/
Statement
{P : Prop} : P → P := by
Hint "
To solve this goal, you have to come up with a function from
`P` (thought of as the set of proofs of $P$!) to itself. Start with
```
intro p
```
"
intro p
Hint "
Our job now is to construct a proof of $P$. But ${p}$ is a proof of $P$.
So
`exact {p}`
will close the goal. Note that `exact P` will not work -- don't
confuse a true/false statement (which could be false!) with a proof.
We will stick with the convention of capital letters for propositions
and small letters for proofs.
"
exact p

109
Game/Levels/OldProposition/Level_3.lean Normal file
View File

@@ -0,0 +1,109 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 3
Title "have"
open MyNat
Introduction
"
Say you have a whole bunch of propositions and implications between them,
and your goal is to build a certain proof of a certain proposition.
If it helps, you can build intermediate proofs of other propositions
along the way, using the `have` command. `have q : Q := ...` is the Lean analogue
of saying \"We now see that we can prove $Q$, because...\"
in the middle of a proof.
It is often not logically necessary, but on the other hand
it is very convenient, for example it can save on notation, or
it can break proofs up into smaller steps.
In the level below, we have a proof of $P$ and we want a proof
of $U$; during the proof we will construct proofs of
of some of the other propositions involved. The diagram of
propositions and implications looks like this pictorially:
$$
\\begin{CD}
P @>{h}>> Q @>{i}>> R \\\\
@. @VV{j}V \\\\
S @>>{k}> T @>>{l}> U
\\end{CD}
$$
and so it's clear how to deduce $U$ from $P$.
"
/-- In the maze of logical implications above, if $P$ is true then so is $U$. -/
Statement
(P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R)
(j : Q → T) (k : S → T) (l : T → U) : U := by
Hint "Indeed, we could solve this level in one move by typing
```
exact l (j (h p))
```
But let us instead stroll more lazily through the level.
We can start by using the `have` tactic to make a proof of $Q$:
```
have q := h p
```
"
have q := h p
Hint "
and then we note that $j {q}$ is a proof of $T$:
```
have t : T := j {q}
```
"
have t := j q
Hint "
(note how we explicitly told Lean what proposition we thought ${t}$ was
a proof of, with that `: T` thing before the `:=`)
and we could even define $u$ to be $l {t}$:
```
have u : U := l {t}
```
"
have u := l t
Hint " and now finish the level with `exact {u}`."
exact u
DisabledTactic apply
Conclusion
"
If you solved the level using `have`, then click on the last line of your proof
(you do know you can move your cursor around with the arrow keys
and explore your proof, right?) and note that the local context at that point
is in something like the following mess:
```
Objects:
P Q R S T U : Prop
Assumptions:
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
q : Q
t : T
u : U
Goal :
U
```
It was already bad enough to start with, and we added three more
terms to it. In level 4 we will learn about the `apply` tactic
which solves the level using another technique, without leaving
so much junk behind.
"

59
Game/Levels/OldProposition/Level_4.lean Normal file
View File

@@ -0,0 +1,59 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 4
Title "apply"
open MyNat
Introduction
"
Let's do the same level again:
$$
\\begin{CD}
P @>{h}>> Q @>{i}>> R \\\\
@. @VV{j}V \\\\
S @>>{k}> T @>>{l}> U
\\end{CD}
$$
We are given a proof $p$ of $P$ and our goal is to find a proof of $U$, or
in other words to find a path through the maze that links $P$ to $U$.
In level 3 we solved this by using `have`s to move forward, from $P$
to $Q$ to $T$ to $U$. Using the `apply` tactic we can instead construct
the path backwards, moving from $U$ to $T$ to $Q$ to $P$.
"
/-- We can solve a maze. -/
Statement
(P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R)
(j : Q → T) (k : S → T) (l : T → U) : U := by
Hint "Our goal is to prove $U$. But $l:T\\implies U$ is
an implication which we are assuming, so it would suffice to prove $T$.
Tell Lean this by starting the proof below with
```
apply l
```
"
apply l
Hint "Notice that our assumptions don't change but *the goal changes*
from `U` to `T`.
Keep `apply`ing implications until your goal is `P`, and try not
to get lost!"
Branch
apply k
Hint "Looks like you got lost. \"Undo\" the last step."
apply j
apply h
Hint "Now solve this goal
with `exact p`. Note: you will need to learn the difference between
`exact p` (which works) and `exact P` (which doesn't, because $P$ is
not a proof of $P$)."
exact p
DisabledTactic «have»

77
Game/Levels/OldProposition/Level_5.lean Normal file
View File

@@ -0,0 +1,77 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 5
Title "P → (Q → P)"
open MyNat
Introduction
"
In this level, our goal is to construct an implication, like in level 2.
```
P → (Q → P)
```
So $P$ and $Q$ are propositions, and our goal is to prove
that $P\\implies(Q\\implies P)$.
We don't know whether $P$, $Q$ are true or false, so initially
this seems like a bit of a tall order. But let's give it a go.
"
/-- For any propositions $P$ and $Q$, we always have
$P\\implies(Q\\implies P)$. -/
Statement
(P Q : Prop) : P → (Q → P) := by
Hint "Our goal is `P → X` for some true/false statement $X$, and if our
goal is to construct an implication then we almost always want to use the
`intro` tactic from level 2, Lean's version of \"assume $P$\", or more precisely
\"assume $p$ is a proof of $P$\". So let's start with
```
intro p
```
"
intro p
Hint "We now have a proof $p$ of $P$ and we are supposed to be constructing
a proof of $Q\\implies P$. So let's assume that $Q$ is true and try
and prove that $P$ is true. We assume $Q$ like this:
```
intro q
```
"
intro q
Hint "Now we have to prove $P$, but have a proof handy:
```
exact {p}
```
"
exact p
Conclusion
"
A mathematician would treat the proposition $P\\implies(Q\\implies P)$
as the same as the proposition $P\\land Q\\implies P$,
because to give a proof of either of these is just to give a method which takes
a proof of $P$ and a proof of $Q$, and returns a proof of $P$. Thinking of the
goal as $P\\land Q\\implies P$ we see why it is provable.
## Did you notice?
I wrote `P → (Q → P)` but Lean just writes `P → Q → P`. This is because
computer scientists adopt the convention that `→` is *right associative*,
which is a fancy way of saying \"when we write `P → Q → R`, we mean `P → (Q → R)`.
Mathematicians would never dream of writing something as ambiguous as
$P\\implies Q\\implies R$ (they are not really interested in proving abstract
propositions, they would rather work with concrete ones such as Fermat's Last Theorem),
so they do not have a convention for where the brackets go. It's important to
remember Lean's convention though, or else you will get confused. If your goal
is `P → Q → R` then you need to know whether `intro h` will create `h : P` or `h : P → Q`.
Make sure you understand which one.
"

55
Game/Levels/OldProposition/Level_6.lean Normal file
View File

@@ -0,0 +1,55 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 6
Title "(P → (Q → R)) → ((P → Q) → (P → R))"
open MyNat
Introduction
"
You can solve this level completely just using `intro`, `apply` and `exact`,
but if you want to argue forwards instead of backwards then don't forget
that you can do things like `have j : Q → R := f p` if `f : P → (Q → R)`
and `p : P`.
"
/-- If $P$ and $Q$ and $R$ are true/false statements, then
$$
(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).
$$ -/
Statement
(P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) := by
Hint "I recommend that you start with `intro f` rather than `intro p`
because even though the goal starts `P → ...`, the brackets mean that
the goal is not the statement that `P` implies anything, it's the statement that
$P\\implies (Q\\implies R)$ implies something. In fact you can save time by starting
with `intro f h p`, which introduces three variables at once, although you'd
better then look at your tactic state to check that you called all those new
terms sensible things. "
intro f
intro h
intro p
Hint "
If you try `have j : {Q} → {R} := {f} {p}`
now then you can `apply j`.
Alternatively you can `apply ({f} {p})` directly.
What happens if you just try `apply {f}`?
"
-- TODO: This hint needs strictness to make sense
-- Branch
-- apply f
-- Hint "Can you figure out what just happened? This is a little
-- `apply` easter egg. Why is it mathematically valid?"
-- Hint (hidden := true) "Note that there are two goals now, first you need to
-- provide an element in ${P}$ which you did not provide before."
have j : Q → R := f p
apply j
Hint (hidden := true) "Is there something you could apply? something of the form
`_ → Q`?"
apply h
exact p

26
Game/Levels/OldProposition/Level_7.lean Normal file
View File

@@ -0,0 +1,26 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 7
Title "(P → Q) → ((Q → R) → (P → R))"
open MyNat
Introduction ""
/-- From $P\\implies Q$ and $Q\\implies R$ we can deduce $P\\implies R$. -/
Statement
(P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) := by
Hint (hidden := true)"If you start with `intro hpq` and then `intro hqr`
the dust will clear a bit."
intro hpq
Hint (hidden := true) "Now try `intro hqr`."
intro hqr
Hint "So this level is really about showing transitivity of $\\implies$,
if you like that sort of language."
intro p
apply hqr
apply hpq
exact p

72
Game/Levels/OldProposition/Level_8.lean Normal file
View File

@@ -0,0 +1,72 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 8
Title "(P → Q) → (¬ Q → ¬ P)"
open MyNat
Introduction
"
There is a false proposition `False`, with no proof. It is
easy to check that $\\lnot Q$ is equivalent to $Q\\implies {\\tt False}$.
In lean, this is true *by definition*, so you can view and treat `¬A` as an implication
`A → False`.
"
/-- If $P$ and $Q$ are propositions, and $P\\implies Q$, then
$\\lnot Q\\implies \\lnot P$. -/
Statement
(P Q : Prop) : (P → Q) → (¬ Q → ¬ P) := by
Hint "However, if you would like to *see* `¬ Q` as `Q → False` because it makes you help
understanding, you can call
```
repeat rw [Not]
```
to get rid of the two occurences of `¬`. (`Not` is the name of `¬`)
I'm sure you can take it from there."
Branch
repeat rw [Not]
Hint "Note that this did not actually change anything internally. Once you're done, you
could delete the `rw [Not]` and your proof would still work."
intro f
intro h
intro p
-- TODO: It is somewhat cumbersome to have these hints several times.
-- defeq option in hints would help
Hint "Now you have to prove `False`. I guess that means you must be proving something by
contradiction. Or are you?"
Hint (hidden := true) "If you `apply {h}` the `False` magically dissappears again. Can you make
mathematical sense of these two steps?"
apply h
apply f
exact p
intro f
intro h
Hint "Note that `¬ P` should be read as `P → False`, so you can directly call `intro p` on it, even
though it might not look like an implication."
intro p
Hint "Now you have to prove `False`. I guess that means you must be proving something by
contradiction. Or are you?"
Hint "If you're stuck, you could do `rw [Not] at {h}`. Maybe that helps."
Branch
rw [Not] at h
Hint "If you `apply {h}` the `False` magically dissappears again. Can you make
mathematical sense of these two steps?"
apply h
apply f
exact p
-- TODO: It this the right place? `repeat` is also introduced in `Multiplication World` so it might be
-- nice to introduce it earlier on the `Function world`-branch.
NewTactic «repeat»
NewDefinition False Not
Conclusion "If you used `rw [Not]` or `rw [Not] at h` anywhere, go through your proof in
the \"Editor Mode\" and delete them all. Observe that your proof still works."

56
Game/Levels/OldProposition/Level_9.lean Normal file
View File

@@ -0,0 +1,56 @@
import Game.Metadata
import Game.MyNat.Addition
World "Proposition"
Level 9
Title "a big maze."
open MyNat
Introduction
"
In Lean3 there was a tactic `cc` which stands for \"congruence closure\"
which could solve all these mazes automatically. Currently this tactic has
not been ported to Lean4, but it will eventually be available!
For now, you can try to do this final level manually to appreciate the use of such
automatisation ;)
"
-- TODO:
-- "Lean's "congruence closure" tactic `cc` is good at mazes. You might want to try it now.
-- Perhaps I should have mentioned it earlier."
/-- There is a way through the following maze. -/
Statement
(A B C D E F G H I J K L : Prop)
(f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
(f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
(f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by
Hint (hidden := true) "You should, once again, start with `intro a`."
intro a
Hint "Use a mixture of `apply` and `have` calls to find your way through the maze."
apply f15
apply f11
apply f9
apply f8
apply f5
apply f2
apply f1
exact a
-- TODO: Once `cc` is implemented,
-- NewTactic cc
Conclusion
"
Now move onto advanced proposition world, where you will see
how to prove goals such as `P ∧ Q` ($P$ and $Q$), `P ∨ Q` ($P$ or $Q$),
`P ↔ Q` ($P\\iff Q$).
You will need to learn five more tactics: `constructor`, `rcases`,
`left`, `right`, and `exfalso`,
but they are all straightforward, and furthermore they are
essentially the last tactics you
need to learn in order to complete all the levels of the Natural Number Game,
including all the 17 levels of Inequality World.
"