Acknowledgements
This material is taken verbatim from Software Foundations V4.0
Copyright (c) 2016
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
Assumed Knowledge:
* Some familiarity with the basics of Coq
Learning Outcomes:
* Write your first proofs by induction, rewriting, and case analysis in Coq.
First, we import all of our definitions from the previous
chapter.
For the
Require Export to work, you first need to use
coqc to compile
Basics.v into
Basics.vo. This is like
making a .class file from a .java file, or a .o file from a .c
file. There are two ways to do it:
 In CoqIDE:
Open Basics.v. In the "Compile" menu, click on "Compile
Buffer".
 From the command line:
Run coqc Basics.v
Proof by Induction
We proved in the last chapter that
0 is a neutral element
for
+ on the left using an easy argument based on
simplification. The fact that it is also a neutral element on the
right...
... cannot be proved in the same simple way. Just applying
reflexivity doesn't work, since the n in n + 0 is an arbitrary
unknown number, so the match in the definition of + can't be
simplified.
Proof.
intros n.
simpl.
Abort.
And reasoning by cases using destruct n doesn't get us much
further: the branch of the case analysis where we assume n = 0
goes through fine, but in the branch where n = S n' for some n' we
get stuck in exactly the same way. We could use destruct n' to
get one step further, but, since n can be arbitrarily large, if we
try to keep on like this we'll never be done.
Theorem plus_n_O_secondtry :
∀n:
nat,
n =
n + 0.
Proof.
intros n.
destruct n as [
n'].

reflexivity.

simpl.
Abort.
To prove interesting facts about numbers, lists, and other
inductively defined sets, we usually need a more powerful
reasoning principle:
induction.
Recall (from high school, a discrete math course, etc.) the
principle of induction over natural numbers: If
P(n) is some
proposition involving a natural number
n and we want to show
that
P holds for
all numbers
n, we can reason like this:
 show that P(O) holds;
 show that, for any n', if P(n') holds, then so does
P(S n');
 conclude that P(n) holds for all n.
In Coq, the steps are the same but the order is backwards: we
begin with the goal of proving
P(n) for all
n and break it
down (by applying the
induction tactic) into two separate
subgoals: first showing
P(O) and then showing
P(n') → P(S
n'). Here's how this works for the theorem at hand:
Theorem plus_n_O :
∀n:
nat,
n =
n + 0.
Proof.
intros n.
induction n as [
n' IHn'].

reflexivity.

simpl.
rewrite ← IHn'.
reflexivity.
Qed.
Like destruct, the induction tactic takes an as...
clause that specifies the names of the variables to be introduced
in the subgoals. In the first branch, n is replaced by 0 and
the goal becomes 0 + 0 = 0, which follows by simplification. In
the second, n is replaced by S n' and the assumption n' + 0 =
n' is added to the context (with the name IHn', i.e., the
Induction Hypothesis for n' — notice that this name is
explicitly chosen in the as... clause of the call to induction
rather than letting Coq choose one arbitrarily). The goal in this
case becomes (S n') + 0 = S n', which simplifies to S (n' + 0)
= S n', which in turn follows from IHn'.
Theorem minus_diag :
∀n,
minus n n = 0.
Proof.
intros n.
induction n as [
n' IHn'].

simpl.
reflexivity.

simpl.
rewrite → IHn'.
reflexivity.
Qed.
(The use of the
intros tactic in these proofs is actually
redundant. When applied to a goal that contains quantified
variables, the
induction tactic will automatically move them
into the context as needed.)
Exercise: 2 stars, recommended (basic_induction)
Prove the following using induction. You might need previously
proven results.
☐
Exercise: 2 stars (double_plus)
Consider the following function, which doubles its argument:
Use induction to prove this simple fact about double:
☐
Exercise: 2 stars, optional (evenb_S)
One inconveninent aspect of our definition of
evenb n is that it
may need to perform a recursive call on
n  2. This makes proofs
about
evenb n harder when done by induction on
n, since we may
need an induction hypothesis about
n  2. The following lemma
gives a better characterization of
evenb (S n):
☐
Exercise: 1 star (destruct_induction)
Briefly explain the difference between the tactics
destruct
and
induction.
☐
Proofs Within Proofs
In Coq, as in informal mathematics, large proofs are often
broken into a sequence of theorems, with later proofs referring to
earlier theorems. But sometimes a proof will require some
miscellaneous fact that is too trivial and of too little general
interest to bother giving it its own toplevel name. In such
cases, it is convenient to be able to simply state and prove the
needed "subtheorem" right at the point where it is used. The
assert tactic allows us to do this. For example, our earlier
proof of the
mult_0_plus theorem referred to a previous theorem
named
plus_O_n. We could instead use
assert to state and
prove
plus_O_n inline:
Theorem mult_0_plus' :
∀n m :
nat,
(0 +
n) *
m =
n *
m.
Proof.
intros n m.
assert (
H: 0 +
n =
n). {
reflexivity. }
rewrite → H.
reflexivity.
Qed.
The
assert tactic introduces two subgoals. The first is
the assertion itself; by prefixing it with
H: we name the
assertion
H. (We can also name the assertion with
as just as
we did above with
destruct and
induction, i.e.,
assert (0 + n
= n) as H.) Note that we surround the proof of this assertion
with curly braces
{ ... }, both for readability and so that,
when using Coq interactively, we can see more easily when we have
finished this subproof. The second goal is the same as the one
at the point where we invoke
assert except that, in the context,
we now have the assumption
H that
0 + n = n. That is,
assert generates one subgoal where we must prove the asserted
fact and a second subgoal where we can use the asserted fact to
make progress on whatever we were trying to prove in the first
place.
The
assert tactic is handy in many sorts of situations. For
example, suppose we want to prove that
(n + m) + (p + q) = (m +
n) + (p + q). The only difference between the two sides of the
= is that the arguments
m and
n to the first inner
+ are
swapped, so it seems we should be able to use the commutativity of
addition (
plus_comm) to rewrite one into the other. However,
the
rewrite tactic is a little stupid about
where it applies
the rewrite. There are three uses of
+ here, and it turns out
that doing
rewrite → plus_comm will affect only the
outer
one...
To get plus_comm to apply at the point where we want it to, we
can introduce a local lemma stating that n + m = m + n (for the
particular m and n that we are talking about here), prove this
lemma using plus_comm, and then use it to do the desired
rewrite.
Theorem plus_rearrange :
∀n m p q :
nat,
(
n +
m) + (
p +
q) = (
m +
n) + (
p +
q).
Proof.
intros n m p q.
assert (
H:
n +
m =
m +
n).
{
rewrite → plus_comm.
reflexivity. }
rewrite → H.
reflexivity.
Qed.
More Exercises
Exercise: 3 stars, recommended (mult_comm)
Use
assert to help prove this theorem. You shouldn't need to
use induction on
plus_swap.
Now prove commutativity of multiplication. (You will probably
need to define and prove a separate subsidiary theorem to be used
in the proof of this one. You may find that plus_swap comes in
handy.)
☐
Exercise: 3 stars, optional (more_exercises)
Take a piece of paper. For each of the following theorems, first
think about whether (a) it can be proved using only
simplification and rewriting, (b) it also requires case
analysis (
destruct), or (c) it also requires induction. Write
down your prediction. Then fill in the proof. (There is no need
to turn in your piece of paper; this is just to encourage you to
reflect before you hack!)
☐
Exercise: 2 stars, optional (beq_nat_refl)
Prove the following theorem. (Putting the
true on the lefthand
side of the equality may look odd, but this is how the theorem is
stated in the Coq standard library, so we follow suit. Rewriting
works equally well in either direction, so we will have no problem
using the theorem no matter which way we state it.)
☐
Exercise: 2 stars, optional (plus_swap')
The
replace tactic allows you to specify a particular subterm to
rewrite and what you want it rewritten to:
replace (t) with (u)
replaces (all copies of) expression
t in the goal by expression
u, and generates
t = u as an additional subgoal. This is often
useful when a plain
rewrite acts on the wrong part of the goal.
Use the
replace tactic to do a proof of
plus_swap', just like
plus_swap but without needing
assert (n + m = m + n).
☐
Exercise: 3 stars, recommended (binary_commute)
Recall the
incr and
bin_to_nat functions that you
wrote for the
binary exercise in the
Basics chapter. Prove
that the following diagram commutes:
bin 
incr >
bin
 
bin_to_nat bin_to_nat
 
v v
nat 
S >
nat
That is, incrementing a binary number and then converting it to
a (unary) natural number yields the same result as first converting
it to a natural number and then incrementing.
Name your theorem
bin_to_nat_pres_incr ("pres" for "preserves").
Before you start working on this exercise, please copy the
definitions from your solution to the
binary exercise here so
that this file can be graded on its own. If you find yourself
wanting to change your original definitions to make the property
easier to prove, feel free to do so!
☐
Exercise: 5 stars, advanced (binary_inverse)
This exercise is a continuation of the previous exercise about
binary numbers. You will need your definitions and theorems from
there to complete this one.
(a) First, write a function to convert natural numbers to binary
numbers. Then prove that starting with any natural number,
converting to binary, then converting back yields the same
natural number you started with.
(b) You might naturally think that we should also prove the
opposite direction: that starting with a binary number,
converting to a natural, and then back to binary yields the
same number we started with. However, this is not true!
Explain what the problem is.
(c) Define a "direct" normalization function — i.e., a function
normalize from binary numbers to binary numbers such that,
for any binary number b, converting to a natural and then back
to binary yields
(normalize b). Prove it. (Warning: This
part is tricky!)
Again, feel free to change your earlier definitions if this helps
here.
☐
Formal vs. Informal Proof (Optional)
"Informal proofs are algorithms; formal proofs are code."
The question of what constitutes a proof of a mathematical
claim has challenged philosophers for millennia, but a rough and
ready definition could be this: A proof of a mathematical
proposition
P is a written (or spoken) text that instills in the
reader or hearer the certainty that
P is true. That is, a proof
is an act of communication.
Acts of communication may involve different sorts of readers. On
one hand, the "reader" can be a program like Coq, in which case
the "belief" that is instilled is that
P can be mechanically
derived from a certain set of formal logical rules, and the proof
is a recipe that guides the program in checking this fact. Such
recipes are
formal proofs.
Alternatively, the reader can be a human being, in which case the
proof will be written in English or some other natural language,
and will thus necessarily be
informal. Here, the criteria for
success are less clearly specified. A "valid" proof is one that
makes the reader believe
P. But the same proof may be read by
many different readers, some of whom may be convinced by a
particular way of phrasing the argument, while others may not be.
Some readers may be particularly pedantic, inexperienced, or just
plain thickheaded; the only way to convince them will be to make
the argument in painstaking detail. But other readers, more
familiar in the area, may find all this detail so overwhelming
that they lose the overall thread; all they want is to be told the
main ideas, since it is easier for them to fill in the details for
themselves than to wade through a written presentation of them.
Ultimately, there is no universal standard, because there is no
single way of writing an informal proof that is guaranteed to
convince every conceivable reader.
In practice, however, mathematicians have developed a rich set of
conventions and idioms for writing about complex mathematical
objects that — at least within a certain community — make
communication fairly reliable. The conventions of this stylized
form of communication give a fairly clear standard for judging
proofs good or bad.
Because we are using Coq in this course, we will be working
heavily with formal proofs. But this doesn't mean we can
completely forget about informal ones! Formal proofs are useful
in many ways, but they are
not very efficient ways of
communicating ideas between human beings.
For example, here is a proof that addition is associative:
Theorem plus_assoc' :
∀n m p :
nat,
n + (
m +
p) = (
n +
m) +
p.
Proof.
intros n m p.
induction n as [
n' IHn'].
reflexivity.
simpl.
rewrite → IHn'.
reflexivity.
Qed.
Coq is perfectly happy with this. For a human, however, it
is difficult to make much sense of it. We can use comments and
bullets to show the structure a little more clearly...
Theorem plus_assoc'' :
∀n m p :
nat,
n + (
m +
p) = (
n +
m) +
p.
Proof.
intros n m p.
induction n as [
n' IHn'].

reflexivity.

simpl.
rewrite → IHn'.
reflexivity.
Qed.
... and if you're used to Coq you may be able to step
through the tactics one after the other in your mind and imagine
the state of the context and goal stack at each point, but if the
proof were even a little bit more complicated this would be next
to impossible.
A (pedantic) mathematician might write the proof something like
this:
 Theorem: For any n, m and p,
n + (
m +
p) = (
n +
m) +
p.
Proof: By induction on n.
 First, suppose n = 0. We must show
0 + (
m +
p) = (0 +
m) +
p.
This follows directly from the definition of +.
 Next, suppose n = S n', where
n' + (
m +
p) = (
n' +
m) +
p.
We must show
(
S n') + (
m +
p) = ((
S n') +
m) +
p.
By the definition of +, this follows from
S (
n' + (
m +
p)) =
S ((
n' +
m) +
p),
which is immediate from the induction hypothesis. Qed.
The overall form of the proof is basically similar, and of
course this is no accident: Coq has been designed so that its
induction tactic generates the same subgoals, in the same
order, as the bullet points that a mathematician would write. But
there are significant differences of detail: the formal proof is
much more explicit in some ways (e.g., the use of
reflexivity)
but much less explicit in others (in particular, the "proof state"
at any given point in the Coq proof is completely implicit,
whereas the informal proof reminds the reader several times where
things stand).
Exercise: 2 stars, advanced, recommended (plus_comm_informal)
Translate your solution for
plus_comm into an informal proof:
Theorem: Addition is commutative.
Proof:
☐
Exercise: 2 stars, optional (beq_nat_refl_informal)
Write an informal proof of the following theorem, using the
informal proof of
plus_assoc as a model. Don't just
paraphrase the Coq tactics into English!
Theorem:
true = beq_nat n n for any
n.
Proof:
☐
Require Export Induction.
Module NatList.
Pairs of Numbers
In an
Inductive type definition, each constructor can take
any number of arguments — none (as with
true and
O), one (as
with
S), or more than one, as here:
This declaration can be read: "There is one way to construct
a pair of numbers: by applying the constructor pair to two
arguments of type nat."
Here are two simple functions for extracting the first and
second components of a pair. The definitions also illustrate how
to do pattern matching on twoargument constructors.
Since pairs are used quite a bit, it is nice to be able to
write them with the standard mathematical notation (x,y) instead
of pair x y. We can tell Coq to allow this with a Notation
declaration.
Notation "( x , y )" := (
pair x y).
The new notation can be used both in expressions and in
pattern matches (indeed, we've seen it already in the previous
chapter — this works because the pair notation is actually
provided as part of the standard library):
Let's try to prove a few simple facts about pairs.
If we state things in a particular (and slightly peculiar) way, we
can complete proofs with just reflexivity (and its builtin
simplification):
But reflexivity is not enough if we state the lemma in a more
natural way:
We have to expose the structure of p so that simpl can
perform the pattern match in fst and snd. We can do this with
destruct.
Notice that, unlike its behavior with
nats,
destruct
doesn't generate an extra subgoal here. That's because
natprods
can only be constructed in one way.
Exercise: 1 star (snd_fst_is_swap)
☐
Exercise: 1 star, optional (fst_swap_is_snd)
☐
Lists of Numbers
Generalizing the definition of pairs, we can describe the
type of
lists of numbers like this: "A list is either the empty
list or else a pair of a number and another list."
For example, here is a threeelement list:
As with pairs, it is more convenient to write lists in
familiar programming notation. The following declarations
allow us to use :: as an infix cons operator and square
brackets as an "outfix" notation for constructing lists.
Notation "x :: l" := (
cons x l)
(
at level 60,
right associativity).
Notation "[ ]" :=
nil.
Notation "[ x ; .. ; y ]" := (
cons x .. (
cons y nil) ..).
It is not necessary to understand the details of these
declarations, but in case you are interested, here is roughly
what's going on. The right associativity annotation tells Coq
how to parenthesize expressions involving several uses of :: so
that, for example, the next three declarations mean exactly the
same thing:
The
at level 60 part tells Coq how to parenthesize
expressions that involve both
:: and some other infix operator.
For example, since we defined
+ as infix notation for the
plus
function at level 50,
Notation "x + y" := (
plus x y)
(
at level 50,
left associativity).
the
+ operator will bind tighter than
::, so
1 + 2 :: [3]
will be parsed, as we'd expect, as
(1 + 2) :: [3] rather than
1
+ (2 :: [3]).
(Expressions like "
1 + 2 :: [3]" can be a little confusing when
you read them in a .v file. The inner brackets, around 3, indicate
a list, but the outer brackets, which are invisible in the HTML
rendering, are there to instruct the "coqdoc" tool that the bracketed
part should be displayed as Coq code rather than running text.)
The second and third
Notation declarations above introduce the
standard squarebracket notation for lists; the righthand side of
the third one illustrates Coq's syntax for declaring nary
notations and translating them to nested sequences of binary
constructors.
Repeat
A number of functions are useful for manipulating lists.
For example, the
repeat function takes a number
n and a
count and returns a list of length
count where every element
is
n.
Length
The
length function calculates the length of a list.
Append
The
app function concatenates (appends) two lists.
Actually, app will be used a lot in some parts of what
follows, so it is convenient to have an infix operator for it.
Notation "x ++ y" := (
app x y)
(
right associativity,
at level 60).
Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof.
reflexivity.
Qed.
Example test_app2:
nil ++ [4;5] = [4;5].
Proof.
reflexivity.
Qed.
Example test_app3: [1;2;3] ++
nil = [1;2;3].
Proof.
reflexivity.
Qed.
Head (with default) and Tail
Here are two smaller examples of programming with lists.
The
hd function returns the first element (the "head") of the
list, while
tl returns everything but the first
element (the "tail").
Of course, the empty list has no first element, so we
must pass a default value to be returned in that case.
Exercises
Exercise: 2 stars, recommended (list_funs)
Complete the definitions of
nonzeros,
oddmembers and
countoddmembers below. Have a look at the tests to understand
what these functions should do.
☐
Exercise: 3 stars, advanced (alternate)
Complete the definition of
alternate, which "zips up" two lists
into one, alternating between elements taken from the first list
and elements from the second. See the tests below for more
specific examples.
Note: one natural and elegant way of writing
alternate will fail
to satisfy Coq's requirement that all
Fixpoint definitions be
"obviously terminating." If you find yourself in this rut, look
for a slightly more verbose solution that considers elements of
both lists at the same time. (One possible solution requires
defining a new kind of pairs, but this is not the only way.)
☐
Bags via Lists
A
bag (or
multiset) is like a set, except that each element
can appear multiple times rather than just once. One possible
implementation is to represent a bag of numbers as a list.
Exercise: 3 stars, recommended (bag_functions)
Complete the following definitions for the functions
count,
sum,
add, and
member for bags.
All these proofs can be done just by reflexivity.
Multiset sum is similar to set union: sum a b contains
all the elements of a and of b. (Mathematicians usually
define union on multisets a little bit differently, which
is why we don't use that name for this operation.)
For sum we're giving you a header that does not give explicit
names to the arguments. Moreover, it uses the keyword
Definition instead of Fixpoint, so even if you had names for
the arguments, you wouldn't be able to process them recursively.
The point of stating the question this way is to encourage you to
think about whether sum can be implemented in another way —
perhaps by using functions that have already been defined.
☐
Exercise: 3 stars, optional (bag_more_functions)
Here are some more bag functions for you to practice with.
When remove_one is applied to a bag without the number to remove,
it should return the same bag unchanged.
☐
Exercise: 3 stars, recommended (bag_theorem)
Write down an interesting theorem
bag_theorem about bags
involving the functions
count and
add, and prove it. Note
that, since this problem is somewhat openended, it's possible
that you may come up with a theorem which is true, but whose proof
requires techniques you haven't learned yet. Feel free to ask for
help if you get stuck!
☐
Reasoning About Lists
As with numbers, simple facts about listprocessing
functions can sometimes be proved entirely by simplification. For
example, the simplification performed by
reflexivity is enough
for this theorem...
... because the
[] is substituted into the match
"scrutinee" in the definition of
app, allowing the match itself
to be simplified.
Also, as with numbers, it is sometimes helpful to perform case
analysis on the possible shapes (empty or nonempty) of an unknown
list.
Here, the
nil case works because we've chosen to define
tl nil = nil. Notice that the
as annotation on the
destruct
tactic here introduces two names,
n and
l', corresponding to
the fact that the
cons constructor for lists takes two
arguments (the head and tail of the list it is constructing).
Usually, though, interesting theorems about lists require
induction for their proofs.
MicroSermon
Simply reading example proof scripts will not get you very far!
It is important to work through the details of each one, using Coq
and thinking about what each step achieves. Otherwise it is more
or less guaranteed that the exercises will make no sense when you
get to them. 'Nuff said.
Induction on Lists
Proofs by induction over datatypes like
natlist are a
little less familiar than standard natural number induction, but
the idea is equally simple. Each
Inductive declaration defines
a set of data values that can be built up using the declared
constructors: a boolean can be either
true or
false; a number
can be either
O or
S applied to another number; a list can be
either
nil or
cons applied to a number and a list.
Moreover, applications of the declared constructors to one another
are the
only possible shapes that elements of an inductively
defined set can have, and this fact directly gives rise to a way
of reasoning about inductively defined sets: a number is either
O or else it is
S applied to some
smaller number; a list is
either
nil or else it is
cons applied to some number and some
smaller list; etc. So, if we have in mind some proposition
P
that mentions a list
l and we want to argue that
P holds for
all lists, we can reason as follows:
 First, show that P is true of l when l is nil.
 Then show that P is true of l when l is cons n l' for
some number n and some smaller list l', assuming that P
is true for l'.
Since larger lists can only be built up from smaller ones,
eventually reaching
nil, these two arguments together establish
the truth of
P for all lists
l. Here's a concrete example:
Theorem app_assoc :
∀l_{1} l_{2} l_{3} :
natlist,
(
l_{1} ++
l_{2}) ++
l_{3} =
l_{1} ++ (
l_{2} ++
l_{3}).
Proof.
intros l_{1} l_{2} l_{3}.
induction l_{1} as [
n l_{1}' IHl1'].

reflexivity.

simpl.
rewrite → IHl1'.
reflexivity.
Qed.
Notice that, as when doing induction on natural numbers, the
as... clause provided to the
induction tactic gives a name to
the induction hypothesis corresponding to the smaller list
l_{1}'
in the
cons case. Once again, this Coq proof is not especially
illuminating as a static written document — it is easy to see
what's going on if you are reading the proof in an interactive Coq
session and you can see the current goal and context at each
point, but this state is not visible in the writtendown parts of
the Coq proof. So a naturallanguage proof — one written for
human readers — will need to include more explicit signposts; in
particular, it will help the reader stay oriented if we remind
them exactly what the induction hypothesis is in the second
case.
For comparison, here is an informal proof of the same theorem.
Theorem: For all lists
l_{1},
l_{2}, and
l_{3},
(l_{1} ++ l_{2}) ++ l_{3} = l_{1} ++ (l_{2} ++ l_{3}).
Proof: By induction on
l_{1}.
 First, suppose l_{1} = []. We must show
([] ++
l_{2}) ++
l_{3} = [] ++ (
l_{2} ++
l_{3}),
which follows directly from the definition of ++.
 Next, suppose l_{1} = n::l_{1}', with
(
l_{1}' ++
l_{2}) ++
l_{3} =
l_{1}' ++ (
l_{2} ++
l_{3})
(the induction hypothesis). We must show
((
n ::
l_{1}') ++
l_{2}) ++
l_{3} = (
n ::
l_{1}') ++ (
l_{2} ++
l_{3}).
By the definition of ++, this follows from
n :: ((
l_{1}' ++
l_{2}) ++
l_{3}) =
n :: (
l_{1}' ++ (
l_{2} ++
l_{3})),
which is immediate from the induction hypothesis. ☐
Reversing a list
For a slightly more involved example of inductive proof over
lists, suppose we use
app to define a listreversing function
rev:
Proofs about reverse
Now let's prove some theorems about our newly defined
rev.
For something a bit more challenging than what we've seen, let's
prove that reversing a list does not change its length. Our first
attempt gets stuck in the successor case...
So let's take the equation relating ++ and length that
would have enabled us to make progress and prove it as a separate
lemma.
Note that, to make the lemma as general as possible, we
quantify over
all natlists, not just those that result from an
application of
rev. This should seem natural, because the truth
of the goal clearly doesn't depend on the list having been
reversed. Moreover, it is easier to prove the more general
property.
Now we can complete the original proof.
For comparison, here are informal proofs of these two theorems:
Theorem: For all lists
l_{1} and
l_{2},
length (l_{1} ++ l_{2}) = length l_{1} + length l_{2}.
Proof: By induction on
l_{1}.
 First, suppose l_{1} = []. We must show
length ([] ++
l_{2}) =
length [] +
length l_{2},
which follows directly from the definitions of
length and ++.
 Next, suppose l_{1} = n::l_{1}', with
length (
l_{1}' ++
l_{2}) =
length l_{1}' +
length l_{2}.
We must show
length ((
n::
l_{1}') ++
l_{2}) =
length (
n::
l_{1}') +
length l_{2}).
This follows directly from the definitions of length and ++
together with the induction hypothesis. ☐
Theorem: For all lists
l,
length (rev l) = length l.
Proof: By induction on
l.
 First, suppose l = []. We must show
length (
rev []) =
length [],
which follows directly from the definitions of length
and rev.
 Next, suppose l = n::l', with
length (
rev l') =
length l'.
We must show
length (
rev (
n ::
l')) =
length (
n ::
l').
By the definition of rev, this follows from
length ((
rev l') ++ [
n]) =
S (
length l')
which, by the previous lemma, is the same as
length (
rev l') +
length [
n] =
S (
length l').
This follows directly from the induction hypothesis and the
definition of length. ☐
The style of these proofs is rather longwinded and pedantic.
After the first few, we might find it easier to follow proofs that
give fewer details (which can easily work out in our own minds or
on scratch paper if necessary) and just highlight the nonobvious
steps. In this more compressed style, the above proof might look
like this:
Theorem:
For all lists
l,
length (rev l) = length l.
Proof: First, observe that
length (l ++ [n]) = S (length l)
for any
l (this follows by a straightforward induction on
l).
The main property again follows by induction on
l, using the
observation together with the induction hypothesis in the case
where
l = n'::l'.
☐
Which style is preferable in a given situation depends on
the sophistication of the expected audience and how similar the
proof at hand is to ones that the audience will already be
familiar with. The more pedantic style is a good default for our
present purposes.
SearchAbout
We've seen that proofs can make use of other theorems we've
already proved, e.g., using
rewrite. But in order to refer to a
theorem, we need to know its name! Indeed, it is often hard even
to remember what theorems have been proven, much less what they
are called.
Coq's
SearchAbout command is quite helpful with this. Typing
SearchAbout foo will cause Coq to display a list of all theorems
involving
foo. For example, try uncommenting the following line
to see a list of theorems that we have proved about
rev:
Keep
SearchAbout in mind as you do the following exercises and
throughout the rest of the book; it can save you a lot of time!
If you are using ProofGeneral, you can run
SearchAbout with
Cc
Ca Ca. Pasting its response into your buffer can be
accomplished with
Cc C;.
List Exercises, Part 1
Exercise: 3 stars (list_exercises)
More practice with lists:
There is a short solution to the next one. If you find yourself
getting tangled up, step back and try to look for a simpler
way.
An exercise about your implementation of nonzeros:
☐
Exercise: 2 stars (beq_natlist)
Fill in the definition of
beq_natlist, which compares
lists of numbers for equality. Prove that
beq_natlist l l
yields
true for every list
l.
☐
List Exercises, Part 2
Exercise: 3 stars, advanced (bag_proofs)
Here are a couple of little theorems to prove about your
definitions about bags earlier in the file.
The following lemma about leb might help you in the next proof.
☐
Exercise: 3 stars, optional (bag_count_sum)
Write down an interesting theorem
bag_count_sum about bags
involving the functions
count and
sum, and prove it.
☐
Exercise: 4 stars, advanced (rev_injective)
Prove that the
rev function is injective — that is,
∀(
l_{1} l_{2} :
natlist),
rev l_{1} =
rev l_{2} → l_{1} =
l_{2}.
(There is a hard way and an easy way to do this.)
☐
Options
Suppose we want to write a function that returns the
nth
element of some list. If we give it type
nat → natlist → nat,
then we'll have to choose some number to return when the list is
too short...
This solution is not so good: If nth_bad returns 42, we
can't tell whether that value actually appears on the input
without further processing. A better alternative is to change the
return type of nth_bad to include an error value as a possible
outcome. We call this type natoption.
We can then change the above definition of nth_bad to
return None when the list is too short and Some a when the
list has enough members and a appears at position n. We call
this new function nth_error to indicate that it may result in an
error.
(In the HTML version, the boilerplate proofs of these
examples are elided. Click on a box if you want to see one.)
This example is also an opportunity to introduce one more small
feature of Coq's programming language: conditional
expressions...
Coq's conditionals are exactly like those found in any other
language, with one small generalization. Since the boolean type
is not built in, Coq actually allows conditional expressions over
any inductively defined type with exactly two constructors. The
guard is considered true if it evaluates to the first constructor
in the
Inductive definition and false if it evaluates to the
second.
The function below pulls the
nat out of a
natoption, returning
a supplied default in the
None case.
Exercise: 2 stars (hd_error)
Using the same idea, fix the
hd function from earlier so we don't
have to pass a default element for the
nil case.
☐
Exercise: 1 star, optional (option_elim_hd)
This exercise relates your new
hd_error to the old
hd.
☐
Partial Maps
As a final illustration of how data structures can be defined in
Coq, here is a simple
partial map data type, analogous to the
map or dictionary data structures found in most programming
languages.
First, we define a new inductive datatype
id to serve as the
"keys" of our partial maps.
Internally, an
id is just a number. Introducing a separate type
by wrapping each nat with the tag
Id makes definitions more
readable and gives us the flexibility to change representations
later if we wish.
We'll also need an equality test for
ids:
Exercise: 1 star (beq_id_refl)
☐
Now we define the type of partial maps:
This declaration can be read: "There are two ways to construct a
partial_map: either using the constructor
empty to represent an
empty partial map, or by applying the constructor
record to
a key, a value, and an existing
partial_map to construct a
partial_map with an additional keytovalue mapping."
The
update function overrides the entry for a given key in a
partial map (or adds a new entry if the given key is not already
present).
Last, the find function searches a partial_map for a given
key. It returns None if the key was not found and Some val if
the key was associated with val. If the same key is mapped to
multiple values, find will return the first one it
encounters.
Exercise: 1 star (update_eq)
☐
Exercise: 1 star (update_neq)
☐
Exercise: 2 stars (baz_num_elts)
Consider the following inductive definition:
How
many elements does the type
baz have? (Answer in English
or the natural language of your choice.)
☐