completed first draft of Properties save for exercises
This commit is contained in:
wadler
parent
33640cf86e
commit
db395b3d89
2 changed files with 398 additions and 89 deletions
|
|
@ -122,7 +122,7 @@ that are on your keyboard.
|
|||
|
||||
## The story of creation
|
||||
|
||||
Let's look again at the definition of natural numbers:
|
||||
Let's look again at the rules that define the natural numbers:
|
||||
|
||||
+ *Base case*: `zero` is a natural number.
|
||||
+ *Inductive case*: if `m` is a natural number, then `suc m` is also a
|
||||
|
|
@ -130,7 +130,7 @@ Let's look again at the definition of natural numbers:
|
|||
|
||||
Wait a minute! The second line defines natural numbers
|
||||
in terms of natural numbers. How can that posssibly be allowed?
|
||||
Isn't this as useless as claiming "Brexit means Brexit"?
|
||||
Isn't this as meaningless as claiming "Brexit means Brexit"?
|
||||
|
||||
In fact, it is possible to assign our definition a meaning without
|
||||
resorting to any unpermitted circularities. Furthermore, we can do so
|
||||
|
|
@ -142,7 +142,7 @@ no natural numbers at all.
|
|||
|
||||
-- in the beginning, there are no natural numbers
|
||||
|
||||
Now, we apply the two cases to all the natural numbers we know about. The
|
||||
Now, we apply the rules to all the natural numbers we know about. The
|
||||
base case tells us that `zero` is a natural number, so we add it to the set
|
||||
of known natural numbers. The inductive case tells us that if `m` is a
|
||||
natural number (on the day before today) then `suc m` is also a
|
||||
|
|
@ -150,17 +150,17 @@ natural number (today). We didn't know about any natural numbers
|
|||
before today, so the inductive case doesn't apply.
|
||||
|
||||
-- on the first day, there is one natural number
|
||||
zero
|
||||
zero : ℕ
|
||||
|
||||
Then we repeat the process, so on the next day we know about all the
|
||||
numbers from the day before, plus any numbers added by the two cases. The
|
||||
numbers from the day before, plus any numbers added by the rules. The
|
||||
base case tells us that `zero` is a natural number, but we already knew
|
||||
that. But now the inductive case tells us that since `zero` was a natural
|
||||
number yesterday, then `suc zero` is a natural number today.
|
||||
|
||||
-- on the second day, there are two natural numbers
|
||||
zero
|
||||
suc zero
|
||||
zero : ℕ
|
||||
suc zero : ℕ
|
||||
|
||||
And we repeat the process again. Now the inductive case
|
||||
tells us that since `zero` and `suc zero` are both natural numbers, then
|
||||
|
|
@ -168,17 +168,17 @@ tells us that since `zero` and `suc zero` are both natural numbers, then
|
|||
the first of these, but the second is new.
|
||||
|
||||
-- on the third day, there are three natural numbers
|
||||
zero
|
||||
suc zero
|
||||
suc (suc zero)
|
||||
zero : ℕ
|
||||
suc zero : ℕ
|
||||
suc (suc zero) : ℕ
|
||||
|
||||
You've probably got the hang of it by now.
|
||||
|
||||
-- on the fourth day, there are four natural numbers
|
||||
zero
|
||||
suc zero
|
||||
suc (suc zero)
|
||||
suc (suc (suc zero))
|
||||
zero : ℕ
|
||||
suc zero : ℕ
|
||||
suc (suc zero) : ℕ
|
||||
suc (suc (suc zero)) : ℕ
|
||||
|
||||
The process continues. On the *n*th day there will be *n* distinct
|
||||
natural numbers. Every natural number will appear on some given day.
|
||||
|
|
@ -200,14 +200,19 @@ we would have no numbers in the beginning, and still no numbers on the
|
|||
second day, and on the third, and so on. An inductive definition lacking
|
||||
a base case is useless, as in the phrase "Brexit means Brexit".
|
||||
|
||||
A philosopher might note that our reference to the first day, second
|
||||
day, and so on, implicitly involves an understanding of natural
|
||||
|
||||
## Philosophy and history
|
||||
|
||||
A philosopher might observe that our reference to the first day,
|
||||
second day, and so on, implicitly involves an understanding of natural
|
||||
numbers. In this sense, our definition might indeed be regarded as in
|
||||
some sense circular. We won't worry about the philosophy, but are ok
|
||||
with taking some intuitive notions---such as counting---as given.
|
||||
some sense circular. We need not let this circularity disturb us.
|
||||
Everyone possesses a good informal understanding of the natural
|
||||
numbers, which we may take as a foundation for their formal
|
||||
description.
|
||||
|
||||
While the natural numbers have been understood for as long as people
|
||||
could count, the inductive definition of the natural numbers is relatively
|
||||
can count, the inductive definition of the natural numbers is relatively
|
||||
recent. It can be traced back to Richard Dedekind's paper "*Was sind
|
||||
und was sollen die Zahlen?*" (What are and what should be the
|
||||
numbers?), published in 1888, and Giuseppe Peano's book "*Arithmetices
|
||||
|
|
@ -457,52 +462,58 @@ definition to equivalent inference rules for judgements about equality.
|
|||
|
||||
Here we assume we have already defined the infinite set of natural
|
||||
numbers, specifying the meaning of the judgment `n : ℕ`. The first
|
||||
inference rule asserts that if `n` is a natural number then adding
|
||||
zero to it gives `n`, and the second rule asserts that if adding `m`
|
||||
and `n` gives `p`, then adding `suc m` and `n` gives `suc p`.
|
||||
inference rule is the base case, and corresponds to line (i) of the
|
||||
definition. It asserts that if `n` is a natural number then adding
|
||||
zero to it gives `n`. The second inference rule is the inductive
|
||||
case, and corresponds to line (ii) of the definition. It asserts that
|
||||
if adding `m` and `n` gives `p`, then adding `suc m` and `n` gives
|
||||
`suc p`.
|
||||
|
||||
Now we can resort to a similar creation story, where now we are
|
||||
Again we resort to a creation story, where this time we are
|
||||
concerned with judgements about addition.
|
||||
|
||||
-- in the beginning, we know nothing about addition
|
||||
-- in the beginning, we know nothing about addition
|
||||
|
||||
Now, we apply the rules to all the judgment we know about.
|
||||
One rule tells us that `zero + n = n` for every natural `n`,
|
||||
so we add all those equations. The other rule tells us that if
|
||||
The base case tells us that `zero + n = n` for every natural `n`,
|
||||
so we add all those equations. The inductive case tells us that if
|
||||
`m + n = p` (on the day before today) then `suc m + n = suc p`
|
||||
(today). We didn't know any equations about addition before today,
|
||||
so that rule doesn't give us any equations.
|
||||
so that rule doesn't give us any new equations.
|
||||
|
||||
-- on the first day, we know about addition of 0
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ...
|
||||
-- on the first day, we know about addition of 0
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ...
|
||||
|
||||
Then we repeat the process, so on the next day we know about all the
|
||||
equations from the day before, plus any equations added by the rules. One
|
||||
rule tells us that `zero + n = n` for every natural `n`, but we already knew
|
||||
that. But now the other rule tells us that for every equation `m + n = p`
|
||||
that we knew yesterday, we know `suc m + n = suc p` today.
|
||||
equations from the day before, plus any equations added by the rules.
|
||||
The base case tells us nothing new, but now the inductive case adds
|
||||
more equations.
|
||||
|
||||
-- on the second day, we know about addition of 0 and 1
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ...
|
||||
1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 ...
|
||||
-- on the second day, we know about addition of 0 and 1
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ...
|
||||
1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ...
|
||||
|
||||
And we repeat the process again.
|
||||
|
||||
-- on the third day, we know about addition of 0, 1, and 2
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ...
|
||||
1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 ...
|
||||
2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 ...
|
||||
-- on the third day, we know about addition of 0, 1, and 2
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ...
|
||||
1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ...
|
||||
2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 2 + 3 = 5 ...
|
||||
|
||||
You've probably got the hang of it by now.
|
||||
|
||||
The process continues. On the *m*th day we will know all the equations
|
||||
where the first number is less than *m*. As before, there is both a
|
||||
base case (line (i) of the definition) and an inductive case (line
|
||||
(ii)).
|
||||
-- on the fourth day, we know about addition of 0, 1, 2, and 3
|
||||
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ...
|
||||
1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ...
|
||||
2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 2 + 3 = 5 ...
|
||||
3 + 0 = 3 3 + 1 = 4 3 + 2 = 5 3 + 3 = 6 ...
|
||||
|
||||
As we can see, the reasoning that justifies inductive and
|
||||
recursive definitions is quite similar, and they might be considered
|
||||
as two sides of the same coin.
|
||||
The process continues. On the *m*th day we will know all the
|
||||
equations where the first number is less than *m*.
|
||||
|
||||
As we can see, the reasoning that justifies inductive and recursive
|
||||
definitions is quite similar. They might be considered two sides of
|
||||
the same coin.
|
||||
|
||||
|
||||
## Precedence
|
||||
|
|
@ -560,6 +571,11 @@ In this chapter we use the following.
|
|||
→ U+2192 RIGHTWARDS ARROW (\to, \r)
|
||||
∸ U+2238 DOT MINUS (\.-)
|
||||
|
||||
Each line consists of the unicode character (ℕ), the corresponding
|
||||
Each line consists of the Unicode character (ℕ), the corresponding
|
||||
code point (U+2115), the name of the character (DOUBLE-STRUCK CAPITAL N),
|
||||
and the sequence to type into Emacs to generate the character (\bN).
|
||||
|
||||
The command \r is a little different to the others, because it gives
|
||||
access to a wide variety of Unicode arrows. After typing \r, one can access
|
||||
the many available arrows by using the left, right, up, and down
|
||||
keys on the keyboard to navigate.
|
||||
|
|
|
|||
|
|
@ -84,31 +84,33 @@ case*.
|
|||
|
||||
Proofs by induction follow the structure of this definition. To prove
|
||||
a property of natural numbers by induction, we need prove two cases.
|
||||
First is the *base case*, where we need to show the property holds for
|
||||
`zero`. Second is the *inductive case*, where we assume as the
|
||||
*inductive hypothesis* that the property holds for an arbitary natural
|
||||
`m` and then show that the property must also hold for `suc m`.
|
||||
First is the *base case*, where we show the property holds for `zero`.
|
||||
Second is the *inductive case*, where we assume the the property holds for
|
||||
an arbitary natural `m` (we call this the *inductive hypothesis*), and
|
||||
then show that the property must also hold for `suc m`.
|
||||
|
||||
If we write `P m` for a property of `m`, then we can write out the principle
|
||||
of induction as an inference rule:
|
||||
If we write `P m` for a property of `m`, then what we need to
|
||||
demonstrate are the following two inference rules:
|
||||
|
||||
------
|
||||
P zero
|
||||
∀ (m : ℕ) → P m → P (suc m)
|
||||
-----------------------------
|
||||
∀ (m : ℕ) → P m
|
||||
|
||||
Let's unpack this rule. The first hypothesis is the base case, and
|
||||
requires we show that property `P` holds for `zero`. The second
|
||||
hypothesis is the inductive case, and requires that for any natural
|
||||
`m` assuming the the induction hypothesis `P` holds for `m` we must
|
||||
then show that `P` also holds for `suc m`.
|
||||
P m
|
||||
---------
|
||||
P (suc m)
|
||||
|
||||
Let's unpack these rules. The first rule is the base case, and
|
||||
requires we show that property `P` holds for `zero`. The second rule
|
||||
is the inductive case, and requires we show that if we assume the
|
||||
inductive hypothesis, that `P` holds for `m`, then it follows that
|
||||
`P` also holds for `suc m`.
|
||||
|
||||
Why does this work? Again, it can be explained by a creation story.
|
||||
To start with, we know no properties.
|
||||
|
||||
-- in the beginning, no properties are known
|
||||
|
||||
Now, we apply the two cases to all the properties we know about. The
|
||||
Now, we apply the two rules to all the properties we know about. The
|
||||
base case tells us that `P zero` holds, so we add it to the set of
|
||||
known properties. The inductive case tells us that if `P m` holds (on
|
||||
the day before today) then `P (suc m)` also holds (today). We didn't
|
||||
|
|
@ -119,8 +121,8 @@ apply.
|
|||
P zero
|
||||
|
||||
Then we repeat the process, so on the next day we know about all the
|
||||
properties from the day before, plus any properties added by the two
|
||||
cases. The base case tells us that `P zero` holds, but we already
|
||||
properties from the day before, plus any properties added by the rules.
|
||||
The base case tells us that `P zero` holds, but we already
|
||||
knew that. But now the inductive case tells us that since `P zero`
|
||||
held yesterday, then `P (suc zero)` holds today.
|
||||
|
||||
|
|
@ -157,14 +159,18 @@ In order to prove associativity, we take `P m` to be the property
|
|||
|
||||
(m + n) + p ≡ m + (n + p)
|
||||
|
||||
Then the appropriate instance of the inference rule becomes:
|
||||
Then the appropriate instances of the inference rules, which
|
||||
we must show to hold, become:
|
||||
|
||||
n : ℕ p : ℕ
|
||||
-------------------------------
|
||||
(zero + n) + p ≡ zero + (n + p)
|
||||
∀ (m : ℕ) → (m + n) + p ≡ m + (n + p) → (suc m + n) + p ≡ (suc m + n) + p
|
||||
-----------------------------------------------------------------------------
|
||||
∀ (m : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
|
||||
In the inference rule, `n` and `p` are any arbitary natural numbers, so when we
|
||||
(m + n) + p ≡ m + (n + p)
|
||||
---------------------------------
|
||||
(suc m + n) + p ≡ (suc m + n) + p
|
||||
|
||||
In the inference rules, `n` and `p` are any arbitary natural numbers, so when we
|
||||
are done with the proof we know it holds for any `n` and `p` as well as any `m`.
|
||||
|
||||
Recall the definition of addition.
|
||||
|
|
@ -221,11 +227,11 @@ induction hypothesis.
|
|||
|
||||
## Encoding the proof in Agda
|
||||
|
||||
We can encode this proof in Agda as follows.
|
||||
We encode this proof in Agda as follows.
|
||||
\begin{code}
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p rewrite assoc+ m n p = refl
|
||||
-- assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
-- assoc+ zero n p = refl
|
||||
-- assoc+ (suc m) n p rewrite assoc+ m n p = refl
|
||||
\end{code}
|
||||
Here we have named the proof `assoc+`. In Agda, identifiers can consist of
|
||||
any sequence of characters not including spaces or the characters `@.(){};_`.
|
||||
|
|
@ -236,13 +242,15 @@ proposition
|
|||
|
||||
∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
|
||||
Such a proof is a function that takes three natural
|
||||
numbers---corresponding to `m`, `n`, and `p`---and returns
|
||||
a proof of the proposition `(m + n) + p ≡ m + (n + p)`.
|
||||
Proof by induction corresponds exactly to a recursive
|
||||
definition. Here we are inducting on the first
|
||||
argument `m`, and leaving the other two arguments `n` and `p`
|
||||
fixed.
|
||||
The upside down A is pronounced "for all", and the proposition
|
||||
asserts that for all natural numbers `m`, `n`, and `p` that
|
||||
the equations `(m + n) + p ≡ m + (n + p)` holds. Such a proof
|
||||
is a function that accepts three natural numbers---corresponding to
|
||||
to `m`, `n`, and `p`---and returns a proof of the equation.
|
||||
|
||||
Proof by induction corresponds exactly to a recursive definition.
|
||||
Here we are induct on the first argument `m`, and leave the other two
|
||||
arguments `n` and `p` fixed.
|
||||
|
||||
The base case corresponds to instantiating `m` by
|
||||
pattern matching on `zero`, so what we are required to
|
||||
|
|
@ -269,18 +277,303 @@ becomes:
|
|||
|
||||
After rewriting with the inductive hypothesis these two terms are
|
||||
equal, and the proof is again given by `refl`.
|
||||
|
||||
Rewriting by a given equation is indicated by the keyword `rewrite`
|
||||
followed by a proof of that equation. Here the inductive hypothesis
|
||||
is not assumed, but instead proved by a recursive invocation of the
|
||||
function we are definining, `assoc+ m n p`. As with addition, this is
|
||||
well founded because associativity of larger numbers is defined in
|
||||
terms of associativity of smaller numbers. In this case,
|
||||
`assoc (suc m) n p` is defined in terms of `assoc m n p`.
|
||||
followed by a proof of that equation.
|
||||
|
||||
This correspondence between proof by induction and definition by
|
||||
Here the inductive hypothesis is not assumed, but instead proved by a
|
||||
recursive invocation of the function we are definining, `assoc+ m n p`.
|
||||
As with addition, this is well founded because associativity of
|
||||
larger numbers is proved in terms of associativity of smaller numbers.
|
||||
In this case, `assoc (suc m) n p` is proved using `assoc m n p`.
|
||||
|
||||
The correspondence between proof by induction and definition by
|
||||
recursion is one of the most appealing aspects of Agda.
|
||||
|
||||
|
||||
## Building proofs interactively
|
||||
|
||||
Agda is designed to be used with the Emacs text editor, and the two
|
||||
in combination provide features that help to create proofs interactively.
|
||||
|
||||
Begin by typing
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ m n p = ?
|
||||
|
||||
The question mark indicates that you would like Agda to help with
|
||||
filling in that part of the code. If you type `^C ^L` (control-C
|
||||
followed by control-L), the question mark will be replaced.
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ m n p = { }0
|
||||
|
||||
The empty braces are called a *hole*, and 0 is a number used for
|
||||
referring to the hole. The hole may display highlighted in green.
|
||||
Emacs will also create a new window at the bottom of the screen
|
||||
displaying the text
|
||||
|
||||
?0 : ((m + n) + p) ≡ (m + (n + p))
|
||||
|
||||
This indicates that hole 0 is to be filled in with a proof of
|
||||
the stated judgement.
|
||||
|
||||
We wish to prove the proposition by induction on `m`. More
|
||||
the cursor into the hole and type `^C ^C`. You will be given
|
||||
the prompt:
|
||||
|
||||
pattern variables to case:
|
||||
|
||||
Typing `m` will cause a split on that variable, resulting
|
||||
in an update to the code.
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = { }0
|
||||
assoc+ (suc m) n p = { }1
|
||||
|
||||
There are now two holes, and the window at the bottom tells you what
|
||||
each is required to prove:
|
||||
|
||||
?0 : ((zero + n) + p) ≡ (zero + (n + p))
|
||||
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))
|
||||
|
||||
Going into hole 0 and typing `^C ^,` will display the text:
|
||||
|
||||
Goal: (n + p) ≡ (n + p)
|
||||
————————————————————————————————————————————————————————————
|
||||
p : ℕ
|
||||
n : ℕ
|
||||
|
||||
This indicates that after simplification the goal for hole 0 is as
|
||||
stated, and that variables `p` and `n` of the stated types are
|
||||
available to use in the proof. The proof of the given goal is
|
||||
trivial, and going into the goal and typing `^C ^R` will fill it in,
|
||||
renumbering the remaining hole to 0:
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p = { }0
|
||||
|
||||
Going into the new hold 0 and typing `^C ^,` will display the text:
|
||||
|
||||
Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
|
||||
————————————————————————————————————————————————————————————
|
||||
p : ℕ
|
||||
n : ℕ
|
||||
m : ℕ
|
||||
|
||||
Again, this gives the simplified goal and the available variables.
|
||||
In this case, we need to rewrite by the induction
|
||||
hypothesis, so let's edit the text accordingly:
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p rewrite assoc+ m n p = { }0
|
||||
|
||||
Going into the remaining hole and typing `^C ^,` will show the
|
||||
goal is now trivial:
|
||||
|
||||
Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
|
||||
————————————————————————————————————————————————————————————
|
||||
p : ℕ
|
||||
n : ℕ
|
||||
m : ℕ
|
||||
|
||||
The proof of the given goal is trivial, and going into the goal and
|
||||
typing `^C ^R` will fill it in, completing the proof:
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p rewrite assoc+ m n p = refl
|
||||
|
||||
|
||||
## Creation, one last time
|
||||
|
||||
Again, it may be helpful to view the recursive definition as
|
||||
a creation story. This time we are concerned with judgements
|
||||
asserting associativity.
|
||||
|
||||
-- in the beginning, we know nothing about associativity
|
||||
|
||||
Now, we apply the rules to all the judgements we know about. The base
|
||||
case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural
|
||||
`n` and `p`. The inductive case tells us that if `(m + n) + p ≡ m +
|
||||
(n + p)` (on the day before today) then `(suc m + n) + p ≡ suc m + (n
|
||||
+ p)` (today). We didn't know any judgments about associativity
|
||||
before today, so that rule doesn't give us any new judgments.
|
||||
|
||||
-- on the first day, we know about associativity of 0
|
||||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||||
|
||||
Then we repeat the process, so on the next day we know about all the
|
||||
judgements from the day before, plus any judgements added by the rules.
|
||||
The base case tells us nothing new, but now the inductive case adds
|
||||
more judgements.
|
||||
|
||||
-- on the second day, we know about associativity of 0 and 1
|
||||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||||
(1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ...
|
||||
|
||||
And we repeat the process again.
|
||||
|
||||
-- on the third day, we know about associativity of 0, 1, and 2
|
||||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||||
(1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ...
|
||||
(2 + 0) + 0 ≡ 2 + (0 + 0) ... (2 + 4) + 5 ≡ 2 + (4 + 5) ...
|
||||
|
||||
You've probably got the hang of it by now.
|
||||
|
||||
-- on the fourth day, we know about associativity of 0, 1, 2, and 3
|
||||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||||
(1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ...
|
||||
(2 + 0) + 0 ≡ 2 + (0 + 0) ... (2 + 4) + 5 ≡ 2 + (4 + 5) ...
|
||||
|
||||
The process continues. On the *m*th day we will know all the
|
||||
judgements where the first number is less than *m*.
|
||||
|
||||
|
||||
## Our second proof: commutativity
|
||||
|
||||
Another important property of addition is that it is commutative. To show
|
||||
this by induction, we take `P m` to be the property
|
||||
|
||||
m + n ≡ n + m
|
||||
|
||||
Then the appropriate instances of the inference rules, which
|
||||
we must show to hold, become:
|
||||
|
||||
n : ℕ
|
||||
-------------------
|
||||
zero + n ≡ n + zero
|
||||
|
||||
m + n ≡ n + m
|
||||
---------------------
|
||||
suc m + n ≡ n + suc m
|
||||
|
||||
In the inference rules, `n` is any arbitary natural number, so when we
|
||||
are done with the proof we know it holds for any `n` as well as any `m`.
|
||||
|
||||
By equation (i) of the definition of addition, the left-hand side of
|
||||
the conclusion of the base case simplifies to `n`, so the base case
|
||||
will hold if we can show
|
||||
|
||||
n + zero ≡ n -- (x)
|
||||
|
||||
By equation (ii) of the definition of addition, the left-hand side of
|
||||
the conclusion of the inductive case simplifies to `suc (m + n)`, so
|
||||
the inductive case will hold if we can show
|
||||
|
||||
n + suc m ≡ suc (n + m) -- (xi)
|
||||
|
||||
and then apply the inductive hypothesis to rewrite `m + n` to `n + m`.
|
||||
We use induction two more times, on `n` this time rather than `m`, to
|
||||
show both (x) and (xi).
|
||||
|
||||
Here is the proof written out in full, using tabular form.
|
||||
|
||||
Proposition.
|
||||
|
||||
m + n ≡ n + m
|
||||
|
||||
Proof. By induction on `m`.
|
||||
|
||||
Base case.
|
||||
|
||||
zero + n
|
||||
≡ (i)
|
||||
n
|
||||
≡ (x)
|
||||
n + zero
|
||||
|
||||
Inductive case.
|
||||
|
||||
suc m + n
|
||||
≡ (ii)
|
||||
suc (m + n)
|
||||
≡ (inductive hypothesis)
|
||||
suc (n + m)
|
||||
≡ (xi)
|
||||
n + suc m
|
||||
|
||||
QED.
|
||||
|
||||
As with other tabular prooofs, it is best understood by reading from top
|
||||
down and bottom up and meeting in the middle.
|
||||
|
||||
We now prove each of the two required lemmas, (x) and (xi).
|
||||
|
||||
Lemma (x).
|
||||
|
||||
n + zero ≡ n
|
||||
|
||||
Proof. By induction on `n`.
|
||||
|
||||
Base case.
|
||||
|
||||
zero + zero
|
||||
≡ (i)
|
||||
zero
|
||||
|
||||
Inductive case.
|
||||
|
||||
suc n + zero
|
||||
≡ (ii)
|
||||
suc (n + zero)
|
||||
≡ (inductive hypothesis)
|
||||
suc n
|
||||
|
||||
QED.
|
||||
|
||||
Lemma (xi).
|
||||
|
||||
n + suc m ≡ suc (n + m)
|
||||
|
||||
Proof. By induction on `n`.
|
||||
|
||||
Base case.
|
||||
|
||||
zero + suc m
|
||||
≡ (i)
|
||||
suc m
|
||||
≡ (i)
|
||||
suc (zero + m)
|
||||
|
||||
Inductive case.
|
||||
|
||||
suc n + suc m
|
||||
≡ (ii)
|
||||
suc (n + suc m)
|
||||
≡ (inductive hypothesis)
|
||||
suc (suc (n + m))
|
||||
≡ (ii)
|
||||
suc (suc n + m)
|
||||
|
||||
QED.
|
||||
|
||||
## Encoding the proofs in Agda
|
||||
|
||||
These proofs can be encoded concisely in Agda.
|
||||
\begin{code}
|
||||
com+zero : ∀ (n : ℕ) → n + zero ≡ n
|
||||
com+zero zero = refl
|
||||
com+zero (suc n) rewrite com+zero n = refl
|
||||
|
||||
com+suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
|
||||
com+suc m zero = refl
|
||||
com+suc m (suc n) rewrite com+suc m n = refl
|
||||
|
||||
com : ∀ (m n : ℕ) → m + n ≡ n + m
|
||||
com zero n rewrite com+zero n = refl
|
||||
com (suc m) n rewrite com+suc m n | com m n = refl
|
||||
\end{code}
|
||||
Here we have renamed Lemma (x) and (xi) to `com+zero` and `com+suc`,
|
||||
respectively. In the final line, rewriting with two equations
|
||||
(lemma (xi) and the inductive hypothesis) is indicated by
|
||||
separating the two proofs of the relevant equations by a vertical bar;
|
||||
the rewrites on the left is performed before that on the right.
|
||||
|
||||
|
||||
|
||||
|
||||
## Unicode
|
||||
|
||||
In this chapter we use the following unicode.
|
||||
|
|
|
|||
Loading…
Reference in a new issue