|
|
import TestGame.Metadata
|
|
|
|
|
|
Level 3
|
|
|
|
|
|
Title "Peano's axioms"
|
|
|
|
|
|
Introduction
|
|
|
"
|
|
|
The team that salvaged the type `ℕ` of natural numbers actually got us three things:
|
|
|
|
|
|
* a term `0 : ℕ`, interpreted as the number zero.
|
|
|
* a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after $n$\".
|
|
|
* The principle of mathematical induction.
|
|
|
|
|
|
These 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 `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 `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.
|
|
|
|
|
|
Let's practice our use of the `rewrite` tactic in the following example.
|
|
|
Our hypothesis `h` is a proof that `succ(a) = b` and we want to prove that
|
|
|
`succ(succ(a))=succ(b)`. In words, we're going to prove that if
|
|
|
`b` is the number after `a` then `succ(b)` is the number after `succ(a)`.
|
|
|
Note that the system drops brackets when they're not
|
|
|
necessary, so `succ b` just means `succ(b)`.
|
|
|
|
|
|
Now here's a tricky question. Knowing that our goal is `succ (succ a) = succ b`,
|
|
|
and our assumption is `h : succ a = b`, then what will the goal change
|
|
|
to when we type
|
|
|
|
|
|
`rewrite [h]`
|
|
|
|
|
|
and hit enter? Remember that `rewrite [h]` will
|
|
|
look for the *left* hand side of `h` in the goal, and will replace it with
|
|
|
the *right* hand side. Try and figure out how the goal will change, and
|
|
|
then try it.
|
|
|
"
|
|
|
|
|
|
Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by
|
|
|
rewrite [h]
|
|
|
rfl
|
|
|
|
|
|
Message (a : ℕ) (b : ℕ) (h : succ a = b) : succ b = succ b =>
|
|
|
"
|
|
|
Look: Lean changed `succ a` into `b`, so the goal became `succ b = succ b`.
|
|
|
That goal is of the form `X = X`, so you know what to do.
|
|
|
"
|
|
|
|
|
|
|
|
|
Conclusion "Congratulations for completing the third level!
|
|
|
You may be wondering whether we could have just substituted in the definition of `b`
|
|
|
and proved the goal that way. To do that, we would want to replace the right hand
|
|
|
side of `h` with the left hand side. You do this in Lean by writing `rewrite [<- h]`. You get the
|
|
|
left-arrow by typing `\\l` and then a space; note that this is a small letter L,
|
|
|
not a number 1. You can just edit your proof and try it.
|
|
|
|
|
|
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 the tutorial, we will introduce addition, and then
|
|
|
we'll be ready to enter Addition World.
|
|
|
"
|
|
|
|
|
|
Tactics rfl rewrite |