extract NNG
Jon Eugster
2 years ago
parent
a8909cb6bb
commit
cddb28fe73
@ -1,2 +0,0 @@
|
||||
build/
|
||||
lake-packages/
|
||||
@ -1,64 +0,0 @@
|
||||
import GameServer.Commands
|
||||
|
||||
import NNG.Levels.Tutorial
|
||||
import NNG.Levels.Addition
|
||||
import NNG.Levels.Multiplication
|
||||
import NNG.Levels.Power
|
||||
import NNG.Levels.Function
|
||||
import NNG.Levels.Proposition
|
||||
import NNG.Levels.AdvProposition
|
||||
import NNG.Levels.AdvAddition
|
||||
import NNG.Levels.AdvMultiplication
|
||||
--import NNG.Levels.Inequality
|
||||
|
||||
Game "NNG"
|
||||
Title "Natural Number Game"
|
||||
Introduction
|
||||
"
|
||||
# Natural Number Game
|
||||
|
||||
##### version 3.0.1
|
||||
|
||||
Welcome to the natural number game -- a game which shows the power of induction.
|
||||
|
||||
In this game, you get own version of the natural numbers, in an interactive
|
||||
theorem prover called Lean. Your version of the natural numbers satisfies something called
|
||||
the principle of mathematical induction, and a couple of other things too (Peano's axioms).
|
||||
Unfortunately, nobody has proved any theorems about these
|
||||
natural numbers yet! For example, addition will be defined for you,
|
||||
but nobody has proved that `x + y = y + x` yet. This is your job. You're going to
|
||||
prove mathematical theorems using the Lean theorem prover. In other words, you're going to solve
|
||||
levels in a computer game.
|
||||
|
||||
You're going to prove these theorems using *tactics*. The introductory world, Tutorial World,
|
||||
will take you through some of these tactics. During your proofs, the assistant shows your
|
||||
\"goal\" (i.e. what you're supposed to be proving) and keeps track of the state of your proof.
|
||||
|
||||
Click on the blue \"Tutorial World\" to start your journey!
|
||||
|
||||
## Save progress
|
||||
|
||||
The game stores your progress locally in your browser storage.
|
||||
If you delete it, your progress will be lost!
|
||||
|
||||
(usually the *website data* gets deleted together with cookies.)
|
||||
|
||||
## Credits
|
||||
|
||||
* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar
|
||||
* **Content adaptation**: Jon Eugster
|
||||
* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot
|
||||
|
||||
## Resources
|
||||
|
||||
* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum
|
||||
* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
|
||||
* [A textbook-style (lean4) version of the NN-game](https://lovettsoftware.com/NaturalNumbers/TutorialWorld/Level1.lean.html)
|
||||
|
||||
"
|
||||
|
||||
Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition → AdvMultiplication
|
||||
Path Addition → Multiplication → AdvMultiplication -- → Inequality
|
||||
Path Multiplication → Power
|
||||
|
||||
MakeGame
|
||||
@ -1,17 +0,0 @@
|
||||
import NNG.Levels.AdvMultiplication.Level_1
|
||||
import NNG.Levels.AdvMultiplication.Level_2
|
||||
import NNG.Levels.AdvMultiplication.Level_3
|
||||
import NNG.Levels.AdvMultiplication.Level_4
|
||||
|
||||
|
||||
Game "NNG"
|
||||
World "AdvMultiplication"
|
||||
Title "Advanced Multiplication World"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Welcome to Advanced Multiplication World! Before attempting this
|
||||
world you should have completed seven other worlds, including
|
||||
Multiplication World and Advanced Addition World. There are four
|
||||
levels in this world.
|
||||
"
|
||||
@ -1,23 +0,0 @@
|
||||
import NNG.Levels.AdvProposition.Level_1
|
||||
import NNG.Levels.AdvProposition.Level_2
|
||||
import NNG.Levels.AdvProposition.Level_3
|
||||
import NNG.Levels.AdvProposition.Level_4
|
||||
import NNG.Levels.AdvProposition.Level_5
|
||||
import NNG.Levels.AdvProposition.Level_6
|
||||
import NNG.Levels.AdvProposition.Level_7
|
||||
import NNG.Levels.AdvProposition.Level_8
|
||||
import NNG.Levels.AdvProposition.Level_9
|
||||
import NNG.Levels.AdvProposition.Level_10
|
||||
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Title "Advanced Proposition World"
|
||||
|
||||
Introduction
|
||||
"
|
||||
In this world we will learn five key tactics needed to solve all the
|
||||
levels of the Natural Number Game, namely `constructor`, `rcases`, `left`, `right`, and `exfalso`.
|
||||
These, and `use` (which we'll get to in Inequality World) are all the
|
||||
tactics you will need to beat all the levels of the game.
|
||||
"
|
||||
@ -1,40 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Level 1
|
||||
Title "the `split` tactic"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
The logical symbol `∧` means \"and\". If $P$ and $Q$ are propositions, then
|
||||
$P\\land Q$ is the proposition \"$P$ and $Q$\".
|
||||
"
|
||||
|
||||
Statement
|
||||
"If $P$ and $Q$ are true, then $P\\land Q$ is true."
|
||||
(P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
|
||||
Hint "If your *goal* is `P ∧ Q` then
|
||||
you can make progress with the `constructor` tactic, which turns one goal `P ∧ Q`
|
||||
into two goals, namely `P` and `Q`."
|
||||
constructor
|
||||
Hint "Now you have two goals. The first one is `P`, which you can proof now. The
|
||||
second one is `Q` and you see it in the queue \"Other Goals\". You will have to prove it afterwards."
|
||||
Hint (hidden := true) "This first goal can be proved with `exact p`."
|
||||
exact p
|
||||
-- Hint "Observe that now the first goal has been proved, so it disappears and you continue
|
||||
-- proving the second goal."
|
||||
-- Hint (hidden := true) "Like the first goal, this is a case for `exact`."
|
||||
-- -- TODO: It looks like these hints get shown above as well, but weirdly the hints from
|
||||
-- -- above to not get shown here.
|
||||
exact q
|
||||
|
||||
NewTactic constructor
|
||||
NewDefinition And
|
||||
|
||||
Conclusion
|
||||
"
|
||||
"
|
||||
@ -1,49 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Level 2
|
||||
Title "the `rcases` tactic"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
If `P ∧ Q` is in the goal, then we can make progress with `constructor`.
|
||||
But what if `P ∧ Q` is a hypothesis? In this case, the `rcases` tactic will enable
|
||||
us to extract proofs of `P` and `Q` from this hypothesis.
|
||||
"
|
||||
|
||||
Statement -- and_symm
|
||||
"If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. "
|
||||
(P Q : Prop) : P ∧ Q → Q ∧ P := by
|
||||
Hint "The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,
|
||||
symmetry of the \"and\" relation. The obvious first move is
|
||||
|
||||
```
|
||||
intro h
|
||||
```
|
||||
|
||||
because the goal is an implication and this tactic is guaranteed
|
||||
to make progress."
|
||||
intro h
|
||||
Hint "Now `{h} : P ∧ Q` is a hypothesis, and
|
||||
|
||||
```
|
||||
rcases {h} with ⟨p, q⟩
|
||||
```
|
||||
|
||||
will change `{h}`, the proof of `P ∧ Q`, into two proofs `p : P`
|
||||
and `q : Q`.
|
||||
|
||||
You can write `⟨p, q⟩` with `\\<>` or `\\<` and `\\>`. Note that `rcases h` by itself will just
|
||||
automatically name the new assumptions."
|
||||
rcases h with ⟨p, q⟩
|
||||
Hint "Now a combination of `constructor` and `exact` will get you home."
|
||||
constructor
|
||||
exact q
|
||||
exact p
|
||||
|
||||
NewTactic rcases
|
||||
|
||||
@ -1,46 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Level 3
|
||||
Title "and_trans"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
Here is another exercise to `rcases` and `constructor`.
|
||||
"
|
||||
|
||||
Statement --and_trans
|
||||
"If $P$, $Q$ and $R$ are true/false statements, then $P\\land Q$ and
|
||||
$Q\\land R$ together imply $P\\land R$."
|
||||
(P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by
|
||||
Hint "Here's a trick:
|
||||
|
||||
Your first steps would probably be
|
||||
```
|
||||
intro h
|
||||
rcases h with ⟨p, q⟩
|
||||
```
|
||||
i.e. introducing a new assumption and then immediately take it appart.
|
||||
|
||||
In that case you could do that in a single step:
|
||||
|
||||
```
|
||||
intro ⟨p, q⟩
|
||||
```
|
||||
"
|
||||
intro hpq
|
||||
rcases hpq with ⟨p, q⟩
|
||||
intro hqr
|
||||
rcases hqr with ⟨q', r⟩
|
||||
constructor
|
||||
assumption
|
||||
assumption
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,45 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Level 4
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `rcases`
|
||||
and `constructor` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need
|
||||
to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to.
|
||||
|
||||
"
|
||||
|
||||
Statement --iff_trans
|
||||
"If $P$, $Q$ and $R$ are true/false statements, then
|
||||
$P\\iff Q$ and $Q\\iff R$ together imply $P\\iff R$."
|
||||
(P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
|
||||
Hint "Similar to \"and\", you can use `intro` and `rcases` to add the `P ↔ Q` to your
|
||||
assumptions and split it into its constituent parts."
|
||||
Branch
|
||||
intro hpq
|
||||
intro hqr
|
||||
Hint "Now you want to use `rcases {hpq} with ⟨pq, qp⟩`."
|
||||
rcases hpq with ⟨hpq, hqp⟩
|
||||
rcases hqr with ⟨hqr, hrq⟩
|
||||
intro ⟨pq, qp⟩
|
||||
intro ⟨qr, rq⟩
|
||||
Hint "If you want to prove an iff-statement, you can use `constructor` to split it
|
||||
into its two implications."
|
||||
constructor
|
||||
· intro p
|
||||
apply qr
|
||||
apply pq
|
||||
exact p
|
||||
· intro r
|
||||
apply qp
|
||||
apply rq
|
||||
exact r
|
||||
|
||||
NewDefinition Iff
|
||||
@ -1,76 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Level 5
|
||||
Title "Easter eggs."
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
Let's try this again. Try proving it in other ways. (Note that `rcases` is temporarily disabled.)
|
||||
|
||||
### A trick.
|
||||
|
||||
Instead of using `rcases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P`
|
||||
directly with `h.1` and `h.2`. So you can solve this level with
|
||||
|
||||
```
|
||||
intro hpq hqr
|
||||
constructor
|
||||
intro p
|
||||
apply hqr.1
|
||||
…
|
||||
```
|
||||
|
||||
### Another trick
|
||||
|
||||
Instead of using `rcases` on `h : P ↔ Q`, you can just `rw [h]`, and this will change all `P`s to `Q`s
|
||||
in the goal. You can use this to create a much shorter proof. Note that
|
||||
this is an argument for *not* running the `rcases` tactic on an iff statement;
|
||||
you cannot rewrite one-way implications, but you can rewrite two-way implications.
|
||||
|
||||
|
||||
"
|
||||
-- TODO
|
||||
-- ### Another trick
|
||||
-- `cc` works on this sort of goal too.
|
||||
|
||||
Statement --iff_trans
|
||||
"If $P$, $Q$ and $R$ are true/false statements, then `P ↔ Q` and `Q ↔ R` together imply `P ↔ R`.
|
||||
"
|
||||
(P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
|
||||
intro hpq hqr
|
||||
Hint "Make a choice and continue either with `constructor` or `rw`.
|
||||
|
||||
* if you use `constructor`, you will use `{hqr}.1, {hqr}.2, …` later.
|
||||
* if you use `rw`, you can replace all `P`s with `Q`s using `rw [{hpq}]`"
|
||||
Branch
|
||||
rw [hpq]
|
||||
Branch
|
||||
exact hqr
|
||||
rw [hqr]
|
||||
Hint "Now `rfl` can close this goal.
|
||||
|
||||
TODO: Note that the current modification of `rfl` is too weak to prove this. For now, you can
|
||||
use `simp` instead (which calls the \"real\" `rfl` internally)."
|
||||
simp
|
||||
constructor
|
||||
intro p
|
||||
Hint "Now you can directly `apply {hqr}.1`"
|
||||
apply hqr.1
|
||||
apply hpq.1
|
||||
assumption
|
||||
intro r
|
||||
apply hpq.2
|
||||
apply hqr.2
|
||||
assumption
|
||||
|
||||
DisabledTactic rcases
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,52 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "AdvProposition"
|
||||
Level 9
|
||||
Title "`exfalso` and proof by contradiction. "
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
It's certainly true that $P\\land(\\lnot P)\\implies Q$ for any propositions $P$
|
||||
and $Q$, because the left hand side of the implication is false. But how do
|
||||
we prove that `False` implies any proposition $Q$? A cheap way of doing it in
|
||||
Lean is using the `exfalso` tactic, which changes any goal at all to `False`.
|
||||
You might think this is a step backwards, but if you have a hypothesis `h : ¬ P`
|
||||
then after `rw not_iff_imp_false at h,` you can `apply h,` to make progress.
|
||||
Try solving this level without using `cc` or `tauto`, but using `exfalso` instead.
|
||||
"
|
||||
|
||||
Statement --contra
|
||||
"If $P$ and $Q$ are true/false statements, then
|
||||
$$(P\\land(\\lnot P))\\implies Q.$$"
|
||||
(P Q : Prop) : (P ∧ ¬ P) → Q := by
|
||||
Hint "Start as usual with `intro ⟨p, np⟩`."
|
||||
Branch
|
||||
exfalso
|
||||
-- TODO: This hint needs to be strict
|
||||
-- Hint "Not so quick! Now you just threw everything away."
|
||||
intro h
|
||||
Hint "You should also call `rcases` on your assumption `{h}`."
|
||||
rcases h with ⟨p, np ⟩
|
||||
-- TODO: This hint should before the last `exact p` step again.
|
||||
Hint "Now you can call `exfalso` to throw away your goal `Q`. It will be replaced with `False` and
|
||||
which means you will have to prove a contradiction."
|
||||
Branch
|
||||
-- TODO: Would `contradiction` not be more useful to introduce than `exfalso`?
|
||||
contradiction
|
||||
exfalso
|
||||
Hint "Recall that `{np} : ¬ P` means `np : P → False`, which means you can simply `apply {np}` now.
|
||||
|
||||
You can also first call `rw [Not] at {np}` to make this step more explicit."
|
||||
Branch
|
||||
rw [Not] at np
|
||||
apply np
|
||||
exact p
|
||||
|
||||
-- TODO: `contradiction`?
|
||||
NewTactic exfalso
|
||||
-- DisabledTactic cc
|
||||
LemmaTab "Prop"
|
||||
@ -1,72 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
-- TODO: Cannot import level from different world.
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 1
|
||||
Title "the `exact` tactic"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
## A new kind of goal.
|
||||
|
||||
All through addition world, our goals have been theorems,
|
||||
and it was our job to find the proofs.
|
||||
**The levels in function world aren't theorems**. This is the only world where
|
||||
the levels aren't theorems in fact. In function world the object of a level
|
||||
is to create an element of the set in the goal. The goal will look like `Goal: X`
|
||||
with $X$ a set and you get rid of the goal by constructing an element of $X$.
|
||||
I don't know if you noticed this, but you finished
|
||||
essentially every goal of Addition World (and Multiplication World and Power World,
|
||||
if you played them) with `rfl`.
|
||||
This tactic is no use to us here.
|
||||
We are going to have to learn a new way of solving goals – the `exact` tactic.
|
||||
|
||||
|
||||
## The `exact` tactic
|
||||
|
||||
If you can explicitly see how to make an element of your goal set,
|
||||
i.e. you have a formula for it, then you can just write `exact <formula>`
|
||||
and this will close the goal.
|
||||
"
|
||||
|
||||
Statement
|
||||
"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true."
|
||||
(P Q : Prop) (p : P) (h : P → Q) : Q := by
|
||||
Hint
|
||||
"In this situation, we have sets $P$ and $Q$ (but Lean calls them types),
|
||||
and an element $p$ of $P$ (written `p : P`
|
||||
but meaning $p\\in P$). We also have a function $h$ from $P$ to $Q$,
|
||||
and our goal is to construct an
|
||||
element of the set $Q$. It's clear what to do *mathematically* to solve
|
||||
this goal -- we can
|
||||
make an element of $Q$ by applying the function $h$ to
|
||||
the element $p$. But how to do it in Lean? There are at least two ways
|
||||
to explain this idea to Lean,
|
||||
and here we will learn about one of them, namely the method which
|
||||
uses the `exact` tactic.
|
||||
|
||||
Concretely, `h p` is an element of type `Q`, so you can use `exact h p` to use it.
|
||||
|
||||
Note that while in mathematics you might write $h(p)$, in Lean you always avoid brackets
|
||||
for function application: `h p`. Brackets are only used for grouping elements, for
|
||||
example for repeated funciton application, you could write `g (h p)`.
|
||||
"
|
||||
Hint (hidden := true) "
|
||||
**Important note**: Note that `exact h P,` won't work (with a capital $P$);
|
||||
this is a common error I see from beginners.
|
||||
$P$ is not an element of $P$, it's $p$ that is an element of $P$.
|
||||
|
||||
So try `exact h p`.
|
||||
"
|
||||
exact h p
|
||||
|
||||
NewTactic exact simp
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,93 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 3
|
||||
Title "the have tactic"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
Say you have a whole bunch of sets and functions between them,
|
||||
and your goal is to build a certain element of a certain set.
|
||||
If it helps, you can build intermediate elements of other sets
|
||||
along the way, using the `have` command. `have` is the Lean analogue
|
||||
of saying \"let's define an element $q\\in Q$ by...\" in the middle of a calculation.
|
||||
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 or calculations up into smaller steps.
|
||||
|
||||
In the level below, we have an element of $P$ and we want an element
|
||||
of $U$; during the proof we will make several intermediate elements
|
||||
of some of the other sets involved. The diagram of sets and
|
||||
functions 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 make the element of $U$ from the element of $P$.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Given an element of $P$ we can define an element of $U$."
|
||||
(P Q R S T U: Type) (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 an element of $Q$:
|
||||
|
||||
```
|
||||
have q := h p
|
||||
```
|
||||
"
|
||||
Branch
|
||||
exact l (j (h p))
|
||||
have q := h p
|
||||
Hint "
|
||||
and now we note that $j(q)$ is an element of $T$
|
||||
|
||||
```
|
||||
have t : T := j q
|
||||
```
|
||||
|
||||
(notice how we can explicitly tell Lean
|
||||
what set we thought $t$ was in, with that `: T` thing before the `:=`.
|
||||
This is optional unless Lean can not figure it out by itself.)
|
||||
"
|
||||
have t : T := j q
|
||||
Hint "
|
||||
Now we could even define $u$ to be $l(t)$:
|
||||
|
||||
```
|
||||
have u : U := l t
|
||||
```
|
||||
"
|
||||
have u : U := l t
|
||||
Hint "…and then finish the level with `exact u`."
|
||||
exact u
|
||||
|
||||
NewTactic «have»
|
||||
|
||||
Conclusion
|
||||
"
|
||||
If you solved the level using `have`, then you might have observed
|
||||
that before the final step the context got quite messy by all the intermediate
|
||||
variables we introduced. You can click \"Toggle Editor\" and then move the cursor
|
||||
around to see the proof you created.
|
||||
|
||||
The context 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.
|
||||
"
|
||||
@ -1,64 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 4
|
||||
Title "the `apply` tactic"
|
||||
|
||||
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 $p \\in P$ and our goal is to find an element 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$.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Given an element of $P$ we can define an element of $U$."
|
||||
(P Q R S T U: Type)
|
||||
(p : P)
|
||||
(h : P → Q)
|
||||
(i : Q → R)
|
||||
(j : Q → T)
|
||||
(k : S → T)
|
||||
(l : T → U) : U :=
|
||||
by
|
||||
Hint "Our goal is to construct an element of the set $U$. But $l:T\\to U$ is
|
||||
a function, so it would suffice to construct an element of $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 functions 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 an element of $P$)."
|
||||
exact p
|
||||
|
||||
NewTactic apply
|
||||
DisabledTactic «have»
|
||||
@ -1,56 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 5
|
||||
Title "P → (Q → P)"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
In this level, our goal is to construct a function, like in level 2.
|
||||
|
||||
```
|
||||
P → (Q → P)
|
||||
```
|
||||
|
||||
So $P$ and $Q$ are sets, and our goal is to construct a function
|
||||
which takes an element of $P$ and outputs a function from $Q$ to $P$.
|
||||
We don't know anything at all about the sets $P$ and $Q$, so initially
|
||||
this seems like a bit of a tall order. But let's give it a go.
|
||||
"
|
||||
|
||||
Statement
|
||||
"We define an element of $\\operatorname{Hom}(P,\\operatorname{Hom}(Q,P))$."
|
||||
(P Q : Type) : P → (Q → P) := by
|
||||
Hint "Our goal is `P → X` for some set $X=\\operatorname\{Hom}(Q,P)$, and if our
|
||||
goal is to construct a function then we almost always want to use the
|
||||
`intro` tactic from level 2, Lean's version of \"let $p\\in P$ be arbitrary.\"
|
||||
So let's start with
|
||||
|
||||
```
|
||||
intro p
|
||||
```"
|
||||
intro p
|
||||
Hint "
|
||||
We now have an arbitrary element $p\\in P$ and we are supposed to be constructing
|
||||
a function $Q\to P$. Well, how about the constant function, which
|
||||
sends everything to $p$?
|
||||
This will work. So let $q\\in Q$ be arbitrary:
|
||||
|
||||
```
|
||||
intro q
|
||||
```"
|
||||
intro q
|
||||
Hint "and then let's output `p`.
|
||||
|
||||
```
|
||||
exact p
|
||||
```"
|
||||
exact p
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,65 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
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`. Remember the trick with the colon in `have`:
|
||||
we could just write `have j := f p,` but this way we can be sure that `j` is
|
||||
what we actually expect it to be.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Whatever the sets $P$ and $Q$ and $R$ are, we
|
||||
make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,\\operatorname{Hom}(Q,R)),
|
||||
\\operatorname{Hom}(\\operatorname{Hom}(P,Q),\\operatorname{Hom}(P,R)))$."
|
||||
(P Q R : Type) : (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 a function from `P` to anything, it's a function from
|
||||
`P → (Q → R)` to 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
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,37 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 7
|
||||
Title "(P → Q) → ((Q → F) → (P → F))"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
Have you noticed that, in stark contrast to earlier worlds,
|
||||
we are not amassing a large collection of useful theorems?
|
||||
We really are just constructing abstract levels with sets and
|
||||
functions, and then solving them and never using the results
|
||||
ever again. Here's another one, which should hopefully be
|
||||
very easy for you now. Advanced mathematician viewers will
|
||||
know it as contravariance of $\\operatorname{Hom}(\\cdot,F)$
|
||||
functor.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Whatever the sets $P$ and $Q$ and $F$ are, we
|
||||
make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
|
||||
\\operatorname{Hom}(\\operatorname{Hom}(Q,F),\\operatorname{Hom}(P,F)))$."
|
||||
(P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := by
|
||||
intro f
|
||||
intro h
|
||||
intro p
|
||||
apply h
|
||||
apply f
|
||||
exact p
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,49 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 8
|
||||
Title "(P → Q) → ((Q → empty) → (P → empty))"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
Level 8 is the same as level 7, except we have replaced the
|
||||
set $F$ with the empty set $\\emptyset$. The same proof will work (after all, our
|
||||
previous proof worked for all sets, and the empty set is a set).
|
||||
"
|
||||
|
||||
Statement
|
||||
"Whatever the sets $P$ and $Q$ are, we
|
||||
make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
|
||||
\\operatorname{Hom}(\\operatorname{Hom}(Q,\\emptyset),\\operatorname{Hom}(P,\\emptyset)))$."
|
||||
(P Q : Type) : (P → Q) → ((Q → Empty) → (P → Empty)) := by
|
||||
Hint (hidden := true) "Maybe start again with `intro`."
|
||||
intros f h p
|
||||
Hint "
|
||||
Note that now your job is to construct an element of the empty set!
|
||||
This on the face of it seems hard, but what is going on is that
|
||||
our hypotheses (we have an element of $P$, and functions $P\\to Q$
|
||||
and $Q\\to\\emptyset$) are themselves contradictory, so
|
||||
I guess we are doing some kind of proof by contradiction at this point? However,
|
||||
if your next line is
|
||||
|
||||
```
|
||||
apply {h}
|
||||
```
|
||||
|
||||
then all of a sudden the goal
|
||||
seems like it might be possible again. If this is confusing, note
|
||||
that the proof of the previous world worked for all sets $F$, so in particular
|
||||
it worked for the empty set, you just probably weren't really thinking about
|
||||
this case explicitly beforehand. [Technical note to constructivists: I know
|
||||
that we are not doing a proof by contradiction. But how else do you explain
|
||||
to a classical mathematician that their goal is to prove something false
|
||||
and this is OK because their hypotheses don't add up?]
|
||||
"
|
||||
apply h
|
||||
apply f
|
||||
exact p
|
||||
|
||||
Conclusion ""
|
||||
@ -1,43 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Game "NNG"
|
||||
World "Function"
|
||||
Level 9
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
I asked around on Zulip and apparently there is not a tactic for this, perhaps because
|
||||
this level is rather artificial. In world 6 we will see a variant of this example
|
||||
which can be solved by a tactic. It would be an interesting project to make a tactic
|
||||
which could solve this sort of level in Lean.
|
||||
|
||||
You can of course work both forwards and backwards, or you could crack and draw a picture.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Given a bunch of functions, we can define another one."
|
||||
(A B C D E F G H I J K L : Type)
|
||||
(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 "In any case, start with `intro a`!"
|
||||
intro a
|
||||
Hint "Now use a combination of `have` and `apply`."
|
||||
apply f15
|
||||
apply f11
|
||||
apply f9
|
||||
apply f8
|
||||
apply f5
|
||||
apply f2
|
||||
apply f1
|
||||
exact a
|
||||
|
||||
|
||||
Conclusion
|
||||
"
|
||||
That's the end of Function World! Next it's Proposition world, and the tactics you've learnt in Function World are enough
|
||||
to solve all nine levels! In fact, the levels in Proposition world might look strangely familiar$\\ldots$.
|
||||
"
|
||||
@ -1,50 +0,0 @@
|
||||
import NNG.Levels.Inequality.Level_1
|
||||
-- import NNG.Levels.Inequality.Level_2
|
||||
-- import NNG.Levels.Inequality.Level_3
|
||||
-- import NNG.Levels.Inequality.Level_4
|
||||
-- import NNG.Levels.Inequality.Level_5
|
||||
-- import NNG.Levels.Inequality.Level_6
|
||||
-- import NNG.Levels.Inequality.Level_7
|
||||
-- import NNG.Levels.Inequality.Level_8
|
||||
-- import NNG.Levels.Inequality.Level_9
|
||||
-- import NNG.Levels.Inequality.Level_10
|
||||
-- import NNG.Levels.Inequality.Level_11
|
||||
-- import NNG.Levels.Inequality.Level_12
|
||||
-- import NNG.Levels.Inequality.Level_13
|
||||
-- import NNG.Levels.Inequality.Level_14
|
||||
-- import NNG.Levels.Inequality.Level_15
|
||||
-- import NNG.Levels.Inequality.Level_16
|
||||
-- import NNG.Levels.Inequality.Level_17
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Title "Inequality World"
|
||||
|
||||
Introduction
|
||||
"
|
||||
A new import, giving us a new definition. If `a` and `b` are naturals,
|
||||
`a ≤ b` is *defined* to mean
|
||||
|
||||
`∃ (c : mynat), b = a + c`
|
||||
|
||||
The upside-down E means \"there exists\". So in words, $a\\le b$
|
||||
if and only if there exists a natural $c$ such that $b=a+c$.
|
||||
|
||||
If you really want to change an `a ≤ b` to `∃ c, b = a + c` then
|
||||
you can do so with `rw le_iff_exists_add`:
|
||||
|
||||
```
|
||||
le_iff_exists_add (a b : mynat) :
|
||||
a ≤ b ↔ ∃ (c : mynat), b = a + c
|
||||
```
|
||||
|
||||
But because `a ≤ b` is *defined as* `∃ (c : mynat), b = a + c`, you
|
||||
do not need to `rw le_iff_exists_add`, you can just pretend when you see `a ≤ b`
|
||||
that it says `∃ (c : mynat), b = a + c`. You will see a concrete
|
||||
example of this below.
|
||||
|
||||
A new construction like `∃` means that we need to learn how to manipulate it.
|
||||
There are two situations. Firstly we need to know how to solve a goal
|
||||
of the form `⊢ ∃ c, ...`, and secondly we need to know how to use a hypothesis
|
||||
of the form `∃ c, ...`.
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 10
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 11
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 12
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 13
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 14
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 15
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 16
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 17
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 4
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 5
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 6
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 7
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 8
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,25 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.LE
|
||||
import Mathlib.Tactic.Use
|
||||
|
||||
Game "NNG"
|
||||
World "Inequality"
|
||||
Level 9
|
||||
Title ""
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
: true := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
"
|
||||
@ -1,48 +0,0 @@
|
||||
import NNG.Levels.Proposition.Level_1
|
||||
import NNG.Levels.Proposition.Level_2
|
||||
import NNG.Levels.Proposition.Level_3
|
||||
import NNG.Levels.Proposition.Level_4
|
||||
import NNG.Levels.Proposition.Level_5
|
||||
import NNG.Levels.Proposition.Level_6
|
||||
import NNG.Levels.Proposition.Level_7
|
||||
import NNG.Levels.Proposition.Level_8
|
||||
import NNG.Levels.Proposition.Level_9 -- `cc` is not ported
|
||||
|
||||
|
||||
Game "NNG"
|
||||
World "Proposition"
|
||||
Title "Proposition World"
|
||||
|
||||
Introduction
|
||||
"
|
||||
A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`.
|
||||
Just like we can have concrete sets in Lean like `mynat`, and abstract
|
||||
sets called things like `X`, we can also have concrete propositions like
|
||||
`2 + 2 = 5` and abstract propositions called things like `P`.
|
||||
|
||||
Mathematicians are very good at conflating a theorem with its proof.
|
||||
They might say \"now use theorem 12 and we're done\". What they really
|
||||
mean is \"now use the proof of theorem 12...\" (i.e. the fact that we proved
|
||||
it already). Particularly problematic is the fact that mathematicians
|
||||
use the word Proposition to mean \"a relatively straightforward statement
|
||||
which is true\" and computer scientists use it to mean \"a statement of
|
||||
arbitrary complexity, which might be true or false\". Computer scientists
|
||||
are far more careful about distinguishing between a proposition and a proof.
|
||||
For example: `x + 0 = x` is a proposition, and `add_zero x`
|
||||
is its proof. The convention we'll use is capital letters for propositions
|
||||
and small letters for proofs.
|
||||
|
||||
In this world you will see the local context in the following kind of state:
|
||||
|
||||
```
|
||||
Objects:
|
||||
P : Prop
|
||||
Assumptions:
|
||||
p : P
|
||||
```
|
||||
|
||||
Here `P` is the true/false statement (the statement of proposition), and `p` is its proof.
|
||||
It's like `P` being the set and `p` being the element. In fact computer scientists
|
||||
sometimes think about the following analogy: propositions are like sets,
|
||||
and their proofs are like their elements.
|
||||
"
|
||||
@ -1,51 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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?
|
||||
"
|
||||
|
||||
Statement
|
||||
"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true."
|
||||
(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
|
||||
@ -1,64 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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.
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
"If $P$ is a proposition then $P\\implies P$."
|
||||
{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
|
||||
@ -1,109 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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$.
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
"In the maze of logical implications above, if $P$ is true then so is $U$."
|
||||
(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.
|
||||
"
|
||||
@ -1,59 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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$.
|
||||
"
|
||||
|
||||
Statement
|
||||
"We can solve a maze."
|
||||
(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»
|
||||
@ -1,77 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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.
|
||||
"
|
||||
|
||||
Statement
|
||||
"For any propositions $P$ and $Q$, we always have
|
||||
$P\\implies(Q\\implies P)$."
|
||||
(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.
|
||||
|
||||
"
|
||||
@ -1,55 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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`.
|
||||
"
|
||||
|
||||
Statement
|
||||
"If $P$ and $Q$ and $R$ are true/false statements, then
|
||||
$$
|
||||
(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).
|
||||
$$"
|
||||
(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
|
||||
@ -1,27 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
World "Proposition"
|
||||
Level 7
|
||||
Title "(P → Q) → ((Q → R) → (P → R))"
|
||||
|
||||
open MyNat
|
||||
|
||||
Introduction ""
|
||||
|
||||
Statement
|
||||
"From $P\\implies Q$ and $Q\\implies R$ we can deduce $P\\implies R$."
|
||||
(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
|
||||
|
||||
@ -1,72 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.MyNat.Addition
|
||||
|
||||
Game "NNG"
|
||||
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`.
|
||||
"
|
||||
|
||||
Statement
|
||||
"If $P$ and $Q$ are propositions, and $P\\implies Q$, then
|
||||
$\\lnot Q\\implies \\lnot P$. "
|
||||
(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."
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue