(* More On Induction; Logic in Coq
Version of 2/2/2009
NOTE: This is a preliminary version of Logic.v. Do not submit it.
A full, revised version will be released on Wednesday the 4th.
You'll need to compile the previous files in order to use this one.
*)
Require Export Polysol.
(* Administrivia...
* Save the date: Midterm I, Wednesday Feb 18
* New convention for "exercise stars"...
- one star: very easy exercises that should be
considered as REQUIRED (ideally they should be
done while reading the lecture notes), but that
are NOT TO BE HANDED IN (and will not be graded)
- two, three, or four stars: real homework problems
that (unless explicitly marked "optional") should
be done and handed in for grading
The 30,000 foot view...
What we've seen so far:
- inductive definitions of datatypes
- Fixpoints over inductive datatypes
- higher-order functions (map, fold, filter, etc.)
- polymorphism
- basic Coq
-- inductive proofs
-- several fundamental tactics
Still to come (before Midterm I):
- more on induction: generalizing the IH, induction principles
- "programming with propositions"
- logical connectives as inductive propositions
*)
(* ----------------------------------------------------- *)
(* Programming with Propositions *)
(* A PROPOSITION is a factual claim. In Coq, propositions
are written as expressions of type Prop. *)
Check (plus 2 2 = 4).
Check (ble_nat 3 2 = false).
(* Both provable and unprovable claims are perfectly good
propositions. Simply BEING a proposition is one thing;
being PROVABLE is something else! *)
Check (plus 2 2 = 4).
Check (plus 2 2 = 5).
(* We've seen one way that propositions can be used in
Coq: in [Theorem] declarations. *)
Theorem plus_2_2_is_4 :
plus 2 2 = 4.
Proof. reflexivity. Qed.
(* Coq allows us to do many other things with
propositions. For example, we can give a name to a
proposition using a [Definition]. *)
Definition plus_fact : Prop := plus 2 2 = 4.
Check plus_fact.
Theorem plus_fact_is_true :
plus_fact.
Proof. unfold plus_fact. reflexivity. Qed.
(* Note that we need an [unfold] in the proof because
[plus_fact] was introduced as a [Definition]. *)
(* So far, all the propositions we have seen are equality
propositions. But we can build on equality
propositions to make other sorts of claims. For
example, what does it mean to claim that "a number n is
even"? We have a function that (we believe) tests
evenness, so one possible definition is "n is even
iff (evenb n = true)." *)
Definition even (n:nat) :=
evenb n = true.
(* [even] is a PARAMETERIZED PROPOSITION. Think of it as a
FUNCTION that, when applied to a number n, yields a
proposition asserting that n is even. *)
Check even.
Check (even 4).
(* The type of [even], [nat->Prop], can be pronounced in
two ways: either simply "[even] is a function from
numbers to propositions" or, perhaps more helpfully,
"[even] is a FAMILY of propositions, indexed by a
number [n]." *)
(* Functions returning propositions are 100% first-class
citizens in Coq. We can use them in other
definitions: *)
Definition even_n__even_SSn (n:nat) :=
(even n) -> (even (S (S n))).
(* We can define them to take multiple arguments... *)
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 pass propositions -- and even parameterized
propositions -- as arguments to functions: *)
Definition true_for_zero (P:nat->Prop) : Prop :=
P 0.
Definition true_for_n__true_for_Sn (P:nat->Prop) (n:nat) : Prop :=
P n -> P (S n).
Definition preserved_by_S (P:nat->Prop) : Prop :=
forall n', P n' -> P (S n').
Definition true_for_all_numbers (P:nat->Prop) : Prop :=
forall n, P n.
Definition nat_induction (P:nat->Prop) : Prop :=
(true_for_zero P)
-> (preserved_by_S P)
-> (true_for_all_numbers P).
(* Let's unravel what this means in concrete terms: *)
Example nat_induction_example : forall (P:nat->Prop),
nat_induction P
= ( (P 0)
-> (forall n', P n' -> P (S n'))
-> (forall n, P n)).
Proof.
unfold nat_induction, true_for_zero, preserved_by_S, true_for_all_numbers.
reflexivity.
Qed.
Theorem our_nat_induction_works : forall (P:nat->Prop),
nat_induction P.
Proof.
intros P.
unfold nat_induction.
intros TFZ PPS.
unfold true_for_all_numbers. intros n.
induction n as [| n'].
Case "n = O". apply TFZ.
Case "n = S n'". apply PPS. apply IHn'.
Qed.
(* ----------------------------------------------------- *)
(* Induction axioms *)
(* You may be puzzled by the last proof because it seems
like we're using a built-in reasoning principle of
induction over natural numbers to prove a theorem that
basically just says the same thing. Indeed, this is
exactly what we just did.
In general, every time we declare a new datatype with
[Inductive], Coq automatically generates an induction
principle as an axiom (a theorem that we do not need to
prove).
The induction principle for a type [t] is called
[t_ind]. Here is the one for natural numbers: *)
Check nat_ind.
(* The ":" here can be pronounced "...is a theorem proving
the proposition..." *)
(* Here's a more direct proof that our induction principle
is valid, using the [nat_ind] axiom directly (with [apply]
instead of [induction]). *)
Theorem our_nat_induction_works' :
forall P, nat_induction P.
Proof.
intros P.
unfold nat_induction, true_for_zero,
preserved_by_S, true_for_all_numbers.
apply nat_ind. Qed.
(* Indeed, we can apply [nat_ind] (instead of using
[induction]) in ANY inductive proof. *)
Theorem mult_0_r' : forall n:nat,
mult n 0 = 0.
Proof.
apply nat_ind.
Case "O". reflexivity.
Case "S". simpl. intros n IHn. rewrite -> IHn.
simpl. reflexivity. Qed.
(* Some things to note:
- In the induction step of the proof we have to do a
little manual bookkeeping (the [intros])
- We do not introduce [n] into the context before
applying [nat_ind]
- The [apply] tactic automatically chooses variable
names for us (in the second subgoal, here), whereas
[induction] gives us a way to specify what names
should be used. The automatic choice is suboptimal.
All this makes [inductive] nicer in practice than using
induction principles directly. *)
Theorem plus_one_r' : forall n:nat,
plus n 1 = S n.
Proof.
(* Complete this proof without using the [induction] tactic. *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Our formulation of induction (the [nat_induction]
proposition and the theorem stating that it works) can
also be used directly to carry out proofs by
induction. *)
Theorem plus_one_r'' : forall n:nat,
plus n 1 = S n.
Proof.
(* Prove the same theorem again without [induction] or
[apply nat_ind]. *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* Induction principles for other datatypes *)
(* We've looked in depth now at the induction principle
for natural numbers. The induction principles that Coq
generates for other datatypes defined with [Inductive]
follow a very similar pattern. If we define a type [t]
with constructors [c1] ... [cn], Coq generates an
induction principle with this shape:
t_ind :
forall P : t -> Prop,
... case for c1 ...
-> ... case for c2 ...
-> ...
-> ... case for cn ...
-> forall 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.
*)
Inductive yesno : Set :=
| yes : yesno
| no : yesno.
Check yesno_ind.
(* Yields:
yesno_ind
: forall P : yesno -> Prop,
P yes
-> P no
-> forall y : yesno, P y
*)
(* EXERCISE (one star): Write out the induction principle
that Coq will generate for the following datatype.
Write down your answer on paper, and then compare it
with what Coq prints. *)
Inductive rgb : Set :=
| red : rgb
| green : rgb
| blue : rgb.
Check rgb_ind.
Inductive natlist : Set :=
| nnil : natlist
| ncons : nat -> natlist -> natlist.
Check natlist_ind.
(* Yields (modulo a little tidying):
natlist_ind :
forall P : natlist -> Prop,
P nnil
-> (forall (n : nat) (l : natlist), P l -> P (ncons n l))
-> forall n : natlist, P n
*)
(* EXERCISE (one star): Suppose we had written the above
definition a little differently: *)
Inductive natlist1 : Set :=
| nnil1 : natlist1
| nsnoc1 : natlist1 -> nat -> natlist1.
(* Now what will the induction principle look like? *)
(* From these examples, we can extract this general rule:
- 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 xs of type t,
then P holds for (c x1 ... xn)"
*)
(* EXERCISE (one star): Here is an induction principle for
an inductively defined set s.
ExSet_ind :
forall P : ExSet -> Prop,
(forall b : bool, P (con1 b))
-> (forall (n : nat) (e : ExSet), P e -> P (con2 n e))
-> forall e : ExSet, P e
Give an [Inductive] definition of ExSet:
Inductive ExSet : Set :=
FILL IN HERE
*)
(* Now, what about polymorphic datatypes?
The inductive definition of polymorphic lists
Inductive list (X:Set) : Set :=
| nil : list X
| cons : X -> list X -> list X.
is very similar. The main difference is that, here, the
whole definition is PARAMTERIZED on a set [X] -- i.e., 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 :
forall (X : Set) (P : list X -> Prop),
P []
-> (forall (x : X) (l : list X), P l -> P (x :: l))
-> forall 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 set
[X], gives us back an induction principle specialized to
[list X]. *)
(* EXERCISE (one star): Write out the induction principle
that Coq will generate for the following datatype.
Compare your answer with what Coq prints. *)
Inductive tree (X:Set) : Set :=
| leaf : X -> tree X
| node : tree X -> tree X -> tree X.
Check tree_ind.
(* THOUGHT EXERCISE (not to be handed in): Find an inductive
definition that gives rise to the following induction
principle:
mytype_ind :
forall (X : Set) (P : mytype X -> Prop),
(forall x : X, P (constr1 X x))
-> (forall n : nat, P (constr2 X n))
-> (forall m : mytype X, P m -> forall n : nat,
P (constr3 X m n))
-> forall m : mytype X, P m *)
(* THOUGHT EXERCISE (not to be handed in): Find an inductive
definition that gives rise to the following induction
principle:
foo_ind :
forall (X Y : Set) (P : foo X Y -> Prop),
(forall x : X, P (bar X Y x))
-> (forall y : Y, P (baz X Y y))
-> (forall f1 : nat -> foo X Y,
(forall n : nat, P (f1 n)) -> P (quux X Y f1))
-> forall f2 : foo X Y, P f2 *)
(* EXERCISE (one star): Consider the following inductive
definition:
Inductive foo (X:Set) : Set :=
| 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 :
forall (X : Set) (P : foo X -> Prop),
(forall (l : list X) (f : foo X),
______________________ -> _______________________)
-> _________________________________________________
-> forall f : foo X, _______________________________
*)
(* ----------------------------------------------------- *)
(* Induction hypotheses *)
(* The induction principle for numbers
forall P : nat -> Prop,
P 0
-> (forall n : nat, P n -> P (S n))
-> forall 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. *)
Definition P_m0r (n:nat) : Prop :=
mult n 0 = 0.
(* ... or equivalently... *)
Definition P_m0r' : nat->Prop :=
fun n => mult n 0 = 0.
Theorem mult_0_r'' : forall n:nat,
P_m0r n.
Proof.
apply nat_ind.
Case "n = O". unfold P_m0r. reflexivity.
Case "n = S n'".
(* Note the proof state at this point! *)
unfold P_m0r. simpl. intros n IHn.
rewrite -> IHn. reflexivity.
Qed.
(* ----------------------------------------------------- *)
(* A closer look at the [induction] tactic *)
(* The [induction] tactic actually does quite a bit of
low-level bookkeeping for us.
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' : forall n m p : nat,
plus n (plus m p) = plus (plus n m) p.
Proof.
(* ...we first introduce all 3 variables into the context,
which amounts to saying "Consider an arbitrary [n], [m], and
[p]..." *)
intros n m p.
(* ...We now use the [induction] tactic to prove [P
n] (that is, [plus n (plus m p) = plus (plus n m) p])
for ALL [n], and hence also for the particular [n] that
is in the context at the moment. *)
induction n as [| n'].
Case "n = O". reflexivity.
Case "n = S n'".
(* In the second subgoal generated by [induction] --
the "inductive step" -- we must prove that [P n']
implies [P (S n')] for all [n']. The [induction]
tactic automatically introduces [n'] and [P n'] into
the context for us, leaving just [P (S n')] as the
goal. *)
simpl. rewrite -> IHn'. reflexivity.
Qed.
(* It also works to apply [induction] to a variable that is
quantified in the goal. *)
Theorem plus_comm' : forall n m : nat,
plus n m = plus 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 [forall m]. *)
(* If we do [induction] on a variable that is quantified in
the goal AFTER some other quantifiers, the [induction]
tactic will automatically introduce these quantifiers
into the context. *)
Theorem plus_comm'' : forall n m : nat,
plus n m = plus m n.
Proof.
(* Let's do induction on [m] this time, instead of
[n]... *)
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 (one star): Rewrite the previous two theorems
and their proofs in the same style as [mult_0_r'']
above -- i.e., give, for each, an explicit [Definition]
of the proposition being proved by induction and state
the theorem and proof in terms of this defined
proposition. *)
(* ---------------------------------------------------------- *)
(* Generalizing induction hypotheses *)
(* Last week's homework included a proof that the [double]
function is injective. The way we START this proof is
a little bit delicate: if we begin it with [intros
n. induction n.], all is well. But if we begin it with
[intros n m. induction n.], we get stuck in the middle
of the inductive case... *)
Theorem double_injective_FAILED : forall n m,
double n = double m
-> n = m.
Proof.
intros n m. induction n as [| n'].
Case "n = O". simpl. intros eq. destruct m as [| m'].
SCase "m = O". reflexivity.
SCase "m = S m'". inversion eq.
Case "n = S n'". intros eq. destruct m as [| m'].
SCase "m = O". inversion eq.
SCase "m = S m'".
assert (n' = m') as H.
SSCase "Proof of assertion".
(* Here we are stuck. We need the assertion in
order to rewrite the final goal (subgoal 2 at
this point) to an identity. But the induction
hypothesis, [IHn'], does not give us [n' = m'] --
there is an extra [S] in the way -- so the
assertion is not provable. *)
Admitted.
(* What went wrong here?
The problem is that, at the point we invoke the induction
hypothesis, we have already introduced [m] into the
context -- intuitively, we have told Coq, "Let's consider
some particular [n] and [m]..." and we now have to prove
that, if [double n = double m] for this *this particular*
[n] and [m], then [n = m].
The next tactic, [induction n] says to Coq: We are going
to show the goal by induction on [n]. That is, we are
going to prove that
P n = "if double n = double m, then n = m"
holds for all [n] by showing
- P O (i.e., "if double O =
double m then O = m")
- P n -> P (S n) (i.e., "if double n =
double m then n = m"
implies "if double (S n) =
double m then S n = m").
If we look closely at the second statement, it is saying
something rather strange: it says that, for any
*particular* [m], if we know
"if double n = double m then n = m"
then we can prove
"if double (S n) = double m then S n = m".
To see why this is strange, let's think of a particular
[m] -- say, [5]. The statement is then saying that, if
we can prove
Q = "if double n = 10 then n = 5"
then we can prove
R = "if double (S n) = 10 then S n = 5".
But knowing Q doesn't give us any help with proving
R! (If we tried to prove R from Q, we would say
something like "Suppose [double (S n) = 10]..." but then
we'd be stuck: knowing that [double (S n)] is [10] tells
us nothing about whether [double n] is [10], so Q is
useless at this point.)
To summarize: Trying to carry out this proof by induction
on [n] when [m] is already in the context doesn't work
because we are trying to prove a relation involving
*every* [n] but just a *single* [m]. *)
(* The good proof of [double_injective] leaves [m] in the
goal statement at the point where the [induction] tactic
is invoked on [n]: *)
Theorem double_injective' : forall n m,
double n = double m
-> n = m.
Proof.
intros n. induction n as [| n'].
Case "n = O". simpl. intros m eq. destruct m as [| m'].
SCase "m = O". reflexivity.
SCase "m = S m'". inversion eq.
Case "n = S n'".
(* Notice that both the goal and the induction
hypothesis have changed: the goal asks us to prove
something more general (i.e., to prove the
statement for *every* [m]), but the IH is
correspondingly more flexible, allowing us to
choose any [m] we like when we apply the IH. *)
intros m eq.
(* Now we choose a particular [m] and introduce the
assumption that [double n = double m]. Since we
are doing a case analysis on [n], we need a case
analysis on [m] to keep the two "in sync". *)
destruct m as [| m'].
SCase "m = O". inversion eq. (* The 0 case is trivial *)
SCase "m = S m'".
(* At this point, since we are in the second
branch of the [destruct m], the [m'] mentioned
in the context at this point is actually the
predecessor of the one we started out talking
about. Since we are also in the [S] branch of
the induction, this is perfect: if we
instantiate the generic [m] in the IH with the
[m'] that we are talking about right now (this
instantiation is performed automatically by
[apply]), then [IHn'] gives us exactly what we
need to finish the proof. *)
assert (n' = m') as H.
SSCase "Proof of assertion". apply IHn'.
inversion eq. reflexivity.
rewrite -> H. reflexivity.
Qed.
(* So what we've learned is that we need to be careful about
using induction to try to prove something too specific:
If we're proving a property of [n] and [m] by induction
on [n], we may need to leave [m] generic.
However, this strategy doesn't always apply directly;
sometimes a little rearrangement is needed. Suppose,
for example, that we had decided we wanted to prove
[double_injective] by induction on [m] instead of
[n]. *)
Theorem double_injective_take2_FAILED : forall n m,
double n = double m
-> n = m.
Proof.
intros n m. induction m as [| m'].
Case "m = O". simpl. intros eq. destruct n as [| n'].
SCase "n = O". reflexivity.
SCase "n = S n'". inversion eq.
Case "m = S m'". intros eq. destruct n as [| n'].
SCase "n = O". inversion eq.
SCase "n = S n'".
assert (n' = m') as H.
SSCase "Proof of assertion".
(* Here we are stuck again, just like before. *)
Admitted.
(* The problem is that, to do induction on [m], we must
first introduce [n]. (If we simply say [induction m]
without introducing anything first, Coq will
automatically introduce [n] for us!) What can we do
about this?
One possibility is to rewrite the statement of the lemma
so that [m] is quantified before [n]. This will work,
but it's not nice: We don't want to have to mangle the
statements of lemmas to fit the needs of a particular
strategy for proving them -- we want to state them in the
most clear and natural way.
What we can do instead is to first introduce all the
quantified variables and then RE-GENERALIZE one or more
of them, taking them out of the context and putting them
back at the beginning of the goal. The [generalize
dependent] tactic does this. *)
Theorem double_injective_take2 : forall n m,
double n = double m
-> n = m.
Proof.
intros n m.
(* [n] and [m] are both in the context *)
generalize dependent n.
(* Now [n] is back in the goal and we can do induction on
[m] and get a sufficiently general IH. *)
induction m as [| m'].
Case "m = O". simpl. intros n eq. destruct n as [| n'].
SCase "n = O". reflexivity.
SCase "n = S n'". inversion eq.
Case "m = S m'". intros n eq. destruct n as [| n'].
SCase "n = O". inversion eq.
SCase "n = S n'".
assert (n' = m') as H.
SSCase "Proof of assertion".
apply IHm'. inversion eq. reflexivity.
rewrite -> H. reflexivity.
Qed.
Theorem plus_n_n_injective_take2 : forall n m,
plus n n = plus m m
-> n = m.
Proof.
(* Carry out this proof by induction on [m]. *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem index_after_last : forall (n : nat) (X : Set)
(l : list X),
length l = n
-> index (S n) l = None.
Proof.
(* Prove this by induction on [l] *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* EXERCISE: Write an informal proof corresponding to your
coq proof of [index_after_last]:
Theorem: For any nat n and list l, if length l = n then
index (S n) l = None.
Proof:
(* FILL IN HERE *)
*)
Theorem length_snoc''' : forall (n : nat) (X : Set)
(v : X) (l : list X),
length l = n
-> length (snoc l v) = S n.
Proof.
(* Prove this by induction on [l]. *)
(* OPTIONAL EXERCISE *) Admitted.
Theorem eqnat_false_S : forall n m,
beq_nat n m = false -> beq_nat (S n) (S m) = false.
Proof.
(* Prove this by induction on [m]. *)
(* OPTIONAL EXERCISE *) Admitted.
Theorem length_append_cons : forall (X : Set) (l1 l2 : list X)
(x : X) (n : nat),
length (l1 ++ (x :: l2)) = n
-> S (length (l1 ++ l2)) = n.
Proof.
(* Prove this by induction on [l1], without using [length_append]. *)
(* OPTIONAL EXERCISE *) Admitted.
Theorem length_appendtwice : forall (X:Set) (n:nat)
(l:list X),
length l = n
-> length (l ++ l) = plus n n.
Proof.
(* Prove this by induction on [l], without using length_append. *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ----------------------------------------------------- *)
(* A quick digression, for adventurous souls... If we can
define parameterized propositions using [Definition],
then can we also use [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. *)
(** <<
(* Define a recursive function [true_upto_n_implies_true_everywhere]
that makes [true_upto_n_example] work. *)
Fixpoint true_upto_n___true_everywhere
(* OPTEXERCISE...*)
(n:nat) (P:nat->Prop) {struct n} : Prop :=
match n with
| 0 => (forall m, P m)
| S n' => (P (S n') -> true_upto_n___true_everywhere n' P)
end.
Example true_upto_n_example :
(true_upto_n___true_everywhere 3 (fun n => even n))
= (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity. Qed.
>> *)