MorePropMore about Propositions and Evidence
Require Export "Prop".
Programming with Propositions
A
proposition is a statement expressing a factual claim,
like "two plus two equals four." In Coq, propositions are written
as expressions of type
Prop. Although we haven't mentioned it
explicitly, we have already seen numerous examples.
Check (2 + 2 = 4).
Check (ble_nat 3 2 = false).
Check (beautiful 8).
Both provable and unprovable claims are perfectly good
propositions. Simply being a proposition is one thing; being
provable is something else!
Check (2 + 2 = 5).
Check (beautiful 4).
Both
2 + 2 = 4 and
2 + 2 = 5 are legal expressions
of type
Prop.
We've seen one place that propositions can appear in Coq: in
Theorem (and
Lemma and
Example) declarations.
Theorem plus_2_2_is_4 :
2 + 2 = 4.
Proof. reflexivity. Qed.
But they can be used in many other ways. For example, we can give
a name to a proposition using a Definition, just as we have
given names to expressions of other sorts.
Definition plus_fact : Prop := 2 + 2 = 4.
Check plus_fact.
We can later use this name in any situation where a proposition is
expected — for example, as the claim in a Theorem declaration.
Theorem plus_fact_is_true :
plus_fact.
Proof. reflexivity. Qed.
We've seen several ways of constructing propositions.
- We can define a new proposition primitively using Inductive.
- Given two expressions e1 and e2 of the same type, we can
form the proposition e1 = e2, which states that their
values are equal.
- We can combine propositions using implication and
quantification.
We have also seen
parameterized propositions, such as
even and
beautiful.
Check (even 4).
Check (even 3).
Check even.
The type of
even, i.e.,
nat→Prop, can be pronounced in
three equivalent ways: (1) "
even is a
function from numbers to
propositions," (2) "
even is a
family of propositions, indexed
by a number
n," or (3) "
even is a
property of numbers."
Propositions — including parameterized propositions — are
first-class citizens in Coq. For example, we can define functions
from numbers to propositions...
Definition between (n m o: nat) : Prop :=
andb (ble_nat n o) (ble_nat o m) = true.
... and then partially apply them:
Definition teen : nat→Prop := between 13 19.
We can even pass propositions — including parameterized
propositions — as arguments to functions:
Definition true_for_zero (P:nat→Prop) : Prop :=
P 0.
Here are two more examples of passing parameterized propositions
as arguments to a function.
The first function,
true_for_all_numbers, takes a proposition
P as argument and builds the proposition that
P is true for
all natural numbers.
Definition true_for_all_numbers (P:nat→Prop) : Prop :=
∀n, P n.
The second, preserved_by_S, takes P and builds the proposition
that, if P is true for some natural number n', then it is also
true by the successor of n' — i.e. that P is preserved by
successor:
Definition preserved_by_S (P:nat→Prop) : Prop :=
∀n', P n' → P (S n').
If we have these as building blocks, we can use them to build up other functions
Definition induction_on_nat (P:nat→Prop)
(P0 : true_for_zero P)
(PnSn : preserved_by_S P) : true_for_all_numbers P :=
fix do_inductive_step (n : nat) : P n :=
match n with
| 0 => P0
| S n' => PnSn n' (do_inductive_step n')
end.
Check induction_on_nat.
In other words, induction isn't magic -- it's recursion!
Exercise: 3 stars (combine_odd_even)
Complete the definition of the
combine_odd_even function
below. It takes as arguments two properties of numbers
Podd and
Peven. As its result, it should return a new property
P such
that
P n is equivalent to
Podd n when
n is odd, and
equivalent to
Peven n otherwise.
Definition combine_odd_even (Podd Peven : nat → Prop) : nat → Prop :=
admit.
To test your definition, see whether you can prove the following
facts:
Theorem combine_odd_even_intro :
∀(Podd Peven : nat → Prop) (n : nat),
(oddb n = true → Podd n) →
(oddb n = false → Peven n) →
combine_odd_even Podd Peven n.
Proof.
Admitted.
Theorem combine_odd_even_elim_odd :
∀(Podd Peven : nat → Prop) (n : nat),
combine_odd_even Podd Peven n →
oddb n = true →
Podd n.
Proof.
Admitted.
Theorem combine_odd_even_elim_even :
∀(Podd Peven : nat → Prop) (n : nat),
combine_odd_even Podd Peven n →
oddb n = false →
Peven n.
Proof.
Admitted.
☐
One more quick digression, for adventurous souls: if we can define
parameterized propositions using
Definition, then can we also
define them using
Fixpoint? Of course we can! However, this
kind of "recursive parameterization" doesn't correspond to
anything very familiar from everyday mathematics. The following
exercise gives a slightly contrived example.
Exercise: 4 stars, optional (true_upto_n__true_everywhere)
Define a recursive function
true_upto_n__true_everywhere that makes
true_upto_n_example work.
☐
Induction Principles
This is a good point to pause and take a deeper look at induction
principles.
Every time we declare a new
Inductive datatype, Coq
automatically generates an
induction principle for this type.
The induction principle for a type
t is called
t_ind. Here is
the one for natural numbers:
Check nat_ind.
The induction tactic is a straightforward wrapper that, at
its core, simply performs apply t_ind. To see this more
clearly, let's experiment a little with using apply nat_ind
directly, instead of the induction tactic, to carry out some
proofs. Here, for example, is an alternate proof of a theorem
that we saw in the Basics chapter.
Theorem mult_0_r' : ∀n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
Case "O". reflexivity.
Case "S". simpl. intros n IHn. rewrite → IHn.
reflexivity. Qed.
This proof is basically the same as the earlier one, but a
few minor differences are worth noting. First, in the induction
step of the proof (the
"S" case), we have to do a little
bookkeeping manually (the
intros) that
induction does
automatically.
Second, we do not introduce
n into the context before applying
nat_ind — the conclusion of
nat_ind is a quantified formula,
and
apply needs this conclusion to exactly match the shape of
the goal state, including the quantifier. The
induction tactic
works either with a variable in the context or a quantified
variable in the goal.
Third, the
apply tactic automatically chooses variable names for
us (in the second subgoal, here), whereas
induction lets us
specify (with the
as... clause) what names should be used. The
automatic choice is actually a little unfortunate, since it
re-uses the name
n for a variable that is different from the
n
in the original theorem. This is why the
Case annotation is
just
S — if we tried to write it out in the more explicit form
that we've been using for most proofs, we'd have to write
n = S
n, which doesn't make a lot of sense! All of these conveniences
make
induction nicer to use in practice than applying induction
principles like
nat_ind directly. But it is important to
realize that, modulo this little bit of bookkeeping, applying
nat_ind is what we are really doing.
Exercise: 2 stars, optional (plus_one_r')
Complete this proof as we did
mult_0_r' above, without using
the
induction tactic.
Theorem plus_one_r' : ∀n:nat,
n + 1 = S n.
Proof.
Admitted.
☐
The induction principles that Coq generates for other datatypes
defined with
Inductive follow a similar pattern. If we define a
type
t with constructors
c1 ...
cn, Coq generates a theorem
with this shape:
t_ind :
∀P :
t → Prop,
...
case for c1 ...
→
...
case for c2 ...
→
...
...
case for cn ...
→
∀n :
t,
P n
The specific shape of each case depends on the arguments to the
corresponding constructor. Before trying to write down a general
rule, let's look at some more examples. First, an example where
the constructors take no arguments:
Inductive yesno : Type :=
| yes : yesno
| no : yesno.
Check yesno_ind.
Exercise: 1 star (rgb)
Write out the induction principle that Coq will generate for the
following datatype. Write down your answer on paper or type it
into a comment, and then compare it with what Coq prints.
Inductive rgb : Type :=
| red : rgb
| green : rgb
| blue : rgb.
Check rgb_ind.
☐
Here's another example, this time with one of the constructors
taking some arguments.
Inductive natlist : Type :=
| nnil : natlist
| ncons : nat → natlist → natlist.
Check natlist_ind.
Exercise: 1 star (natlist1)
Suppose we had written the above definition a little
differently:
Inductive natlist1 : Type :=
| nnil1 : natlist1
| nsnoc1 : natlist1 → nat → natlist1.
Now what will the induction principle look like?
☐
From these examples, we can extract this general rule:
- The type declaration gives several constructors; each
corresponds to one clause of the induction principle.
- Each constructor c takes argument types a1...an.
- Each ai can be either t (the datatype we are defining) or
some other type s.
- The corresponding case of the induction principle
says (in English):
- "for all values x1...xn of types a1...an, if P
holds for each of the inductive arguments (each xi of
type t), then P holds for c x1 ... xn".
Exercise: 1 star (ex_set)
Here is an induction principle for an inductively defined
set.
ExSet_ind :
∀P :
ExSet → Prop,
(
∀b :
bool,
P (
con1 b))
→
(
∀(
n :
nat) (
e :
ExSet),
P e → P (
con2 n e))
→
∀e :
ExSet,
P e
Give an
Inductive definition of
ExSet:
Inductive ExSet : Type :=
.
☐
What about polymorphic datatypes?
The inductive definition of polymorphic lists
Inductive list (
X:
Type) :
Type :=
|
nil :
list X
|
cons :
X → list X → list X.
is very similar to that of
natlist. The main difference is
that, here, the whole definition is
parameterized on a set
X:
that is, we are defining a
family of inductive types
list X,
one for each
X. (Note that, wherever
list appears in the body
of the declaration, it is always applied to the parameter
X.)
The induction principle is likewise parameterized on
X:
list_ind :
∀(
X :
Type) (
P :
list X → Prop),
P []
→
(
∀(
x :
X) (
l :
list X),
P l → P (
x ::
l))
→
∀l :
list X,
P l
Note the wording here (and, accordingly, the form of
list_ind):
The
whole induction principle is parameterized on
X. That is,
list_ind can be thought of as a polymorphic function that, when
applied to a type
X, gives us back an induction principle
specialized to the type
list X.
Exercise: 1 star (tree)
Write out the induction principle that Coq will generate for
the following datatype. Compare your answer with what Coq
prints.
Inductive tree (X:Type) : Type :=
| leaf : X → tree X
| node : tree X → tree X → tree X.
Check tree_ind.
☐
Exercise: 1 star (mytype)
Find an inductive definition that gives rise to the
following induction principle:
mytype_ind :
∀(
X :
Type) (
P :
mytype X → Prop),
(
∀x :
X,
P (
constr1 X x))
→
(
∀n :
nat,
P (
constr2 X n))
→
(
∀m :
mytype X,
P m →
∀n :
nat,
P (
constr3 X m n))
→
∀m :
mytype X,
P m
☐
Exercise: 1 star, optional (foo)
Find an inductive definition that gives rise to the
following induction principle:
foo_ind :
∀(
X Y :
Type) (
P :
foo X Y → Prop),
(
∀x :
X,
P (
bar X Y x))
→
(
∀y :
Y,
P (
baz X Y y))
→
(
∀f1 :
nat → foo X Y,
(
∀n :
nat,
P (
f1 n))
→ P (
quux X Y f1))
→
∀f2 :
foo X Y,
P f2
☐
Exercise: 1 star, optional (foo')
Consider the following inductive definition:
Inductive foo' (X:Type) : Type :=
| C1 : list X → foo' X → foo' X
| C2 : foo' X.
What induction principle will Coq generate for
foo'? Fill
in the blanks, then check your answer with Coq.)
foo'_ind :
∀(
X :
Type) (
P :
foo' X → Prop),
(
∀(
l :
list X) (
f :
foo' X),
_______________________ →
_______________________ )
→
___________________________________________ →
∀f :
foo' X,
________________________
☐
Induction Hypotheses
Where does the phrase "induction hypothesis" fit into this story?
The induction principle for numbers
∀P :
nat → Prop,
P 0
→
(
∀n :
nat,
P n → P (
S n))
→
∀n :
nat,
P n
is a generic statement that holds for all propositions
P (strictly speaking, for all families of propositions
P
indexed by a number
n). Each time we use this principle, we
are choosing
P to be a particular expression of type
nat→Prop.
We can make the proof more explicit by giving this expression a
name. For example, instead of stating the theorem
mult_0_r as
"
∀ n, n * 0 = 0," we can write it as "
∀ n, P_m0r
n", where
P_m0r is defined as...
Definition P_m0r (n:nat) : Prop :=
n * 0 = 0.
... or equivalently...
Definition P_m0r' : nat→Prop :=
fun n => n * 0 = 0.
Now when we do the proof it is easier to see where P_m0r
appears.
Theorem mult_0_r'' : ∀n:nat,
P_m0r n.
Proof.
apply nat_ind.
Case "n = O". reflexivity.
Case "n = S n'".
unfold P_m0r. simpl. intros n' IHn'.
apply IHn'. Qed.
This extra naming step isn't something that we'll do in
normal proofs, but it is useful to do it explicitly for an example
or two, because it allows us to see exactly what the induction
hypothesis is. If we prove ∀ n, P_m0r n by induction on
n (using either induction or apply nat_ind), we see that the
first subgoal requires us to prove P_m0r 0 ("P holds for
zero"), while the second subgoal requires us to prove ∀ n',
P_m0r n' → P_m0r n' (S n') (that is "P holds of S n' if it
holds of n'" or, more elegantly, "P is preserved by S").
The induction hypothesis is the premise of this latter
implication — the assumption that P holds of n', which we are
allowed to use in proving that P holds for S n'.
Optional Material
This section offers some additional details on how induction works
in Coq and the process of building proof trees. It can safely be
skimmed on a first reading. (We recommend skimming rather than
skipping over it outright: it answers some questions that occur to
many Coq users at some point, so it is useful to have a rough idea
of what's here.)
Induction Principles in Prop
Earlier, we looked in detail at the induction principles that Coq
generates for inductively defined
sets. The induction
principles for inductively defined
propositions like
gorgeous
are a tiny bit more complicated. As with all induction
principles, we want to use the induction principle on
gorgeous
to prove things by inductively considering the possible shapes
that something in
gorgeous can have — either it is evidence
that
0 is gorgeous, or it is evidence that, for some
n,
3+n
is gorgeous, or it is evidence that, for some
n,
5+n is
gorgeous and it includes evidence that
n itself is. Intuitively
speaking, however, what we want to prove are not statements about
evidence but statements about
numbers. So we want an
induction principle that lets us prove properties of numbers by
induction on evidence.
For example, from what we've said so far, you might expect the
inductive definition of
gorgeous...
Inductive gorgeous :
nat → Prop :=
g_0 :
gorgeous 0
|
g_plus3 :
∀n,
gorgeous n → gorgeous (3+
m)
|
g_plus5 :
∀n,
gorgeous n → gorgeous (5+
m).
...to give rise to an induction principle that looks like this...
gorgeous_ind_max :
∀P : (
∀n :
nat,
gorgeous n → Prop),
P O g_0 →
(
∀(
m :
nat) (
e :
gorgeous m),
P m e → P (3+
m) (
g_plus3 m e)
→
(
∀(
m :
nat) (
e :
gorgeous m),
P m e → P (5+
m) (
g_plus5 m e)
→
∀(
n :
nat) (
e :
gorgeous n),
P n e
... because:
- Since gorgeous is indexed by a number n (every gorgeous
object e is a piece of evidence that some particular number
n is gorgeous), the proposition P is parameterized by both
n and e — that is, the induction principle can be used to
prove assertions involving both a gorgeous number and the
evidence that it is gorgeous.
- Since there are three ways of giving evidence of gorgeousness
(gorgeous has three constructors), applying the induction
principle generates three subgoals:
- We must prove that P holds for O and b_0.
- We must prove that, whenever n is a gorgeous
number and e is an evidence of its gorgeousness,
if P holds of n and e,
then it also holds of 3+m and g_plus3 n e.
- We must prove that, whenever n is a gorgeous
number and e is an evidence of its gorgeousness,
if P holds of n and e,
then it also holds of 5+m and g_plus5 n e.
- If these subgoals can be proved, then the induction principle
tells us that P is true for all gorgeous numbers n and
evidence e of their gorgeousness.
But this is a little more flexibility than we actually need or
want: it is giving us a way to prove logical assertions where the
assertion involves properties of some piece of
evidence of
gorgeousness, while all we really care about is proving
properties of
numbers that are gorgeous — we are interested in
assertions about numbers, not about evidence. It would therefore
be more convenient to have an induction principle for proving
propositions
P that are parameterized just by
n and whose
conclusion establishes
P for all gorgeous numbers
n:
∀P :
nat → Prop,
...
→
∀n :
nat,
gorgeous n → P n
For this reason, Coq actually generates the following simplified
induction principle for
gorgeous:
Check gorgeous_ind.
In particular, Coq has dropped the evidence term
e as a
parameter of the the proposition
P, and consequently has
rewritten the assumption
∀ (n : nat) (e: gorgeous n), ...
to be
∀ (n : nat), gorgeous n → ...; i.e., we no longer
require explicit evidence of the provability of
gorgeous n.
In English,
gorgeous_ind says:
- Suppose, P is a property of natural numbers (that is, P n is
a Prop for every n). To show that P n holds whenever n
is gorgeous, it suffices to show:
- P holds for 0,
- for any n, if n is gorgeous and P holds for
n, then P holds for 3+n,
- for any n, if n is gorgeous and P holds for
n, then P holds for 5+n.
We can apply
gorgeous_ind directly instead of using
induction.
Theorem gorgeous__beautiful' : ∀n, gorgeous n → beautiful n.
Proof.
intros.
apply gorgeous_ind.
Case "g_0".
apply b_0.
Case "g_plus3".
intros.
apply b_sum. apply b_3.
apply H1.
Case "g_plus5".
intros.
apply b_sum. apply b_5.
apply H1.
apply H.
Qed.
Module P.
Exercise: 3 stars, optional (p_provability)
Consider the following inductively defined proposition:
Inductive p : (tree nat) → nat → Prop :=
| c1 : ∀n, p (leaf _ n) 1
| c2 : ∀t1 t2 n1 n2,
p t1 n1 → p t2 n2 → p (node _ t1 t2) (n1 + n2)
| c3 : ∀t n, p t n → p t (S n).
Describe, in English, the conditions under which the
proposition
p t n is provable.
☐
End P.
More on the induction Tactic
The
induction tactic actually does even more low-level
bookkeeping for us than we discussed above.
Recall the informal statement of the induction principle for
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, if P n' holds, then so does P (S n')
- conclude that P n holds for all n.
So, when we begin a proof with
intros n and then
induction n,
we are first telling Coq to consider a
particular n (by
introducing it into the context) and then telling it to prove
something about
all numbers (by using induction).
What Coq actually does in this situation, internally, is to
"re-generalize" the variable we perform induction on. For
example, in the proof above that
plus is associative...
Theorem plus_assoc' : ∀n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p.
induction n as [| n'].
Case "n = O". reflexivity.
Case "n = S n'".
simpl. rewrite → IHn'. reflexivity. Qed.
It also works to apply induction to a variable that is
quantified in the goal.
Theorem plus_comm' : ∀n m : nat,
n + m = m + n.
Proof.
induction n as [| n'].
Case "n = O". intros m. rewrite → plus_0_r. reflexivity.
Case "n = S n'". intros m. simpl. rewrite → IHn'.
rewrite ← plus_n_Sm. reflexivity. Qed.
Note that
induction n leaves
m still bound in the goal —
i.e., what we are proving inductively is a statement beginning
with
∀ m.
If we do
induction on a variable that is quantified in the goal
after some other quantifiers, the
induction tactic will
automatically introduce the variables bound by these quantifiers
into the context.
Theorem plus_comm'' : ∀n m : nat,
n + m = m + n.
Proof.
induction m as [| m'].
Case "m = O". simpl. rewrite → plus_0_r. reflexivity.
Case "m = S m'". simpl. rewrite ← IHm'.
rewrite ← plus_n_Sm. reflexivity. Qed.
Exercise: 1 star, optional (plus_explicit_prop)
Rewrite both
plus_assoc' and
plus_comm' and their proofs in
the same style as
mult_0_r'' above — that is, for each theorem,
give an explicit
Definition of the proposition being proved by
induction, and state the theorem and proof in terms of this
defined proposition.
☐
Additional Exercises
Exercise: 2 stars, optional (foo_ind_principle)
Suppose we make the following inductive definition:
Inductive foo (
X :
Set) (
Y :
Set) :
Set :=
|
foo1 :
X → foo X Y
|
foo2 :
Y → foo X Y
|
foo3 :
foo X Y → foo X Y.
Fill in the blanks to complete the induction principle that will be
generated by Coq.
foo_ind
:
∀(
X Y :
Set) (
P :
foo X Y → Prop),
(
∀x :
X,
__________________________________)
→
(
∀y :
Y,
__________________________________)
→
(
________________________________________________)
→
________________________________________________
☐
Exercise: 2 stars, optional (bar_ind_principle)
Consider the following induction principle:
bar_ind
:
∀P :
bar → Prop,
(
∀n :
nat,
P (
bar1 n))
→
(
∀b :
bar,
P b → P (
bar2 b))
→
(
∀(
b :
bool) (
b0 :
bar),
P b0 → P (
bar3 b b0))
→
∀b :
bar,
P b
Write out the corresponding inductive set definition.
Inductive bar :
Set :=
|
bar1 :
________________________________________
|
bar2 :
________________________________________
|
bar3 :
________________________________________.
☐
Exercise: 2 stars, optional (no_longer_than_ind)
Given the following inductively defined proposition:
Inductive no_longer_than (
X :
Set) : (
list X)
→ nat → Prop :=
|
nlt_nil :
∀n,
no_longer_than X []
n
|
nlt_cons :
∀x l n,
no_longer_than X l n →
no_longer_than X (
x::
l) (
S n)
|
nlt_succ :
∀l n,
no_longer_than X l n →
no_longer_than X l (
S n).
write the induction principle generated by Coq.
no_longer_than_ind
:
∀(
X :
Set) (
P :
list X → nat → Prop),
(
∀n :
nat,
____________________)
→
(
∀(
x :
X) (
l :
list X) (
n :
nat),
no_longer_than X l n → ____________________ →
_____________________________ →
(
∀(
l :
list X) (
n :
nat),
no_longer_than X l n → ____________________ →
_____________________________ →
∀(
l :
list X) (
n :
nat),
no_longer_than X l n →
____________________
☐