logical-foundations/IndPrinciples.v
2020-06-03 21:46:06 -05:00

714 lines
26 KiB
Coq

(** * IndPrinciples: Induction Principles *)
(** With the Curry-Howard correspondence and its realization in Coq in
mind, we can now take a deeper look at induction principles. *)
Set Warnings "-notation-overridden,-parsing".
From LF Require Export ProofObjects.
(* ################################################################# *)
(** * Basics *)
(** Every time we declare a new [Inductive] datatype, Coq
automatically generates an _induction principle_ for this type.
This induction principle is a theorem like any other: If [t] is
defined inductively, the corresponding induction principle is
called [t_ind]. Here is the one for natural numbers: *)
Check nat_ind.
(* ===> nat_ind :
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n *)
(** The [induction] tactic is a straightforward wrapper that, at its
core, simply performs [apply t_ind]. To see this more clearly,
let's experiment with directly using [apply nat_ind], 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' : forall n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
- (* n = O *) reflexivity.
- (* n = S n' *) 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. By contrast, the
[induction] tactic works either with a variable in the context or
a quantified variable in the goal.
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 these bits of bookkeeping,
applying [nat_ind] is what we are really doing. *)
(** **** Exercise: 2 stars, standard, optional (plus_one_r')
Complete this proof without using the [induction] tactic. *)
Theorem plus_one_r' : forall n:nat,
n + 1 = S n.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** Coq generates induction principles for every datatype defined with
[Inductive], including those that aren't recursive. Although of
course we don't need induction to prove properties of
non-recursive datatypes, the idea of an induction principle still
makes sense for them: it gives a way to prove that a property
holds for all values of the type.
These generated principles follow a similar pattern. If we define
a type [t] with constructors [c1] ... [cn], Coq generates a
theorem 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. First, an example where
the constructors take no arguments: *)
Inductive yesno : Type :=
| yes
| no.
Check yesno_ind.
(* ===> yesno_ind : forall P : yesno -> Prop,
P yes ->
P no ->
forall y : yesno, P y *)
(** **** Exercise: 1 star, standard, optional (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
| green
| blue.
Check rgb_ind.
(** [] *)
(** Here's another example, this time with one of the constructors
taking some arguments. *)
Inductive natlist : Type :=
| nnil
| ncons (n : nat) (l : natlist).
Check natlist_ind.
(* ===> (modulo a little variable renaming)
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: 1 star, standard, optional (natlist1)
Suppose we had written the above definition a little
differently: *)
Inductive natlist1 : Type :=
| nnil1
| nsnoc1 (l : natlist1) (n : nat).
(** 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:
- "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, standard, optional (byntree_ind)
Write out the induction principle that Coq will generate for the
following datatype. (Again, write down your answer on paper or
type it into a comment, and then compare it with what Coq
prints.) *)
Inductive byntree : Type :=
| bempty
| bleaf (yn : yesno)
| nbranch (yn : yesno) (t1 t2 : byntree).
(** [] *)
(** **** Exercise: 1 star, standard, optional (ex_set)
Here is an induction principle for an inductively defined
set.
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 : Type :=
(* FILL IN HERE *)
.
(** [] *)
(* ################################################################# *)
(** * Polymorphism *)
(** Next, 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 :
forall (X : Type) (P : list X -> Prop),
P [] ->
(forall (x : X) (l : list X), P l -> P (x :: l)) ->
forall l : list X, P l
Note that 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, standard, optional (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 : X)
| node (t1 t2 : tree X).
Check tree_ind.
(** [] *)
(** **** Exercise: 1 star, standard, optional (mytype)
Find an inductive definition that gives rise to the
following induction principle:
mytype_ind :
forall (X : Type) (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
*)
(** [] *)
(** **** Exercise: 1 star, standard, optional (foo)
Find an inductive definition that gives rise to the
following induction principle:
foo_ind :
forall (X Y : Type) (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: 1 star, standard, optional (foo')
Consider the following inductive definition: *)
Inductive foo' (X:Type) : Type :=
| C1 (l : list X) (f : foo' X)
| C2.
(** What induction principle will Coq generate for [foo']? Fill
in the blanks, then check your answer with Coq.)
foo'_ind :
forall (X : Type) (P : foo' X -> Prop),
(forall (l : list X) (f : foo' X),
_______________________ ->
_______________________ ) ->
___________________________________________ ->
forall f : foo' X, ________________________
*)
(** [] *)
(* ################################################################# *)
(** * Induction Hypotheses *)
(** Where does the phrase "induction hypothesis" fit into this story?
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] (or rather, 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 proofs by induction more explicit by giving
this expression a name. For example, instead of stating
the theorem [mult_0_r] as "[forall n, n * 0 = 0]," we can
write it as "[forall 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 it is easier to see where [P_m0r] appears in the proof. *)
Theorem mult_0_r'' : forall n:nat,
P_m0r n.
Proof.
apply nat_ind.
- (* n = O *) reflexivity.
- (* n = S n' *)
(* Note the proof state at this point! *)
intros n IHn.
unfold P_m0r in IHn. unfold P_m0r. simpl. apply IHn. Qed.
(** This extra naming step isn't something that we 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 [forall 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 [forall n',
P_m0r n' -> P_m0r (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']. *)
(* ################################################################# *)
(** * 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 our original proof that [plus] is associative... *)
Theorem plus_assoc' : forall n m p : nat,
n + (m + p) = (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, [n + (m + p) = (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'].
- (* n = O *) reflexivity.
- (* 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,
n + m = m + n.
Proof.
induction n as [| n'].
- (* n = O *) intros m. rewrite <- plus_n_O. reflexivity.
- (* 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 the variables bound by these quantifiers
into the context. *)
Theorem plus_comm'' : forall n m : nat,
n + m = m + n.
Proof.
(* Let's do induction on [m] this time, instead of [n]... *)
induction m as [| m'].
- (* m = O *) simpl. rewrite <- plus_n_O. reflexivity.
- (* m = S m' *) simpl. rewrite <- IHm'.
rewrite <- plus_n_Sm. reflexivity. Qed.
(** **** Exercise: 1 star, standard, 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. *)
(* FILL IN 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 [even] are a
tiny bit more complicated. As with all induction principles, we
want to use the induction principle on [even] to prove things by
inductively considering the possible shapes that something in [even]
can have. Intuitively speaking, however, what we want to prove
are not statements about _evidence_ but statements about
_numbers_: accordingly, 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 [even]...
Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS : forall n : nat, even n -> even (S (S n)).
...to give rise to an induction principle that looks like this...
ev_ind_max : forall P : (forall n : nat, even n -> Prop),
P O ev_0 ->
(forall (m : nat) (E : even m),
P m E ->
P (S (S m)) (ev_SS m E)) ->
forall (n : nat) (E : even n),
P n E
... because:
- Since [even] is indexed by a number [n] (every [even] object [E] is
a piece of evidence that some particular number [n] is even),
the proposition [P] is parameterized by both [n] and [E] --
that is, the induction principle can be used to prove
assertions involving both an even number and the evidence that
it is even.
- Since there are two ways of giving evidence of evenness ([even]
has two constructors), applying the induction principle
generates two subgoals:
- We must prove that [P] holds for [O] and [ev_0].
- We must prove that, whenever [n] is an even number and [E]
is an evidence of its evenness, if [P] holds of [n] and
[E], then it also holds of [S (S n)] and [ev_SS n E].
- If these subgoals can be proved, then the induction principle
tells us that [P] is true for _all_ even numbers [n] and
evidence [E] of their evenness.
This is more flexibility than we normally need or want: it is
giving us a way to prove logical assertions where the assertion
involves properties of some piece of _evidence_ of evenness, while
all we really care about is proving properties of _numbers_ that
are even -- 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 even numbers [n]:
forall P : nat -> Prop,
... ->
forall n : nat,
even n -> P n
For this reason, Coq actually generates the following simplified
induction principle for [even]: *)
Check even_ind.
(* ===> ev_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, even n -> P n -> P (S (S n))) ->
forall n : nat,
even n -> P n *)
(** In particular, Coq has dropped the evidence term [E] as a
parameter of the the proposition [P]. *)
(** In English, [ev_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 even, it suffices to show:
- [P] holds for [0],
- for any [n], if [n] is even and [P] holds for [n], then [P]
holds for [S (S n)]. *)
(** As expected, we can apply [ev_ind] directly instead of using
[induction]. For example, we can use it to show that [even'] (the
slightly awkward alternate definition of evenness that we saw in
an exercise in the \chap{IndProp} chapter) is equivalent to the
cleaner inductive definition [even]: *)
Theorem ev_ev' : forall n, even n -> even' n.
Proof.
apply even_ind.
- (* ev_0 *)
apply even'_0.
- (* ev_SS *)
intros m Hm IH.
apply (even'_sum 2 m).
+ apply even'_2.
+ apply IH.
Qed.
(** The precise form of an [Inductive] definition can affect the
induction principle Coq generates.
For example, in chapter [IndProp], we defined [<=] as: *)
(* Inductive le : nat -> nat -> Prop :=
| le_n : forall n, le n n
| le_S : forall n m, (le n m) -> (le n (S m)). *)
(** This definition can be streamlined a little by observing that the
left-hand argument [n] is the same everywhere in the definition,
so we can actually make it a "general parameter" to the whole
definition, rather than an argument to each constructor. *)
Inductive le (n:nat) : nat -> Prop :=
| le_n : le n n
| le_S m (H : le n m) : le n (S m).
Notation "m <= n" := (le m n).
(** The second one is better, even though it looks less symmetric.
Why? Because it gives us a simpler induction principle. *)
Check le_ind.
(* ===> forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall n0 : nat, n <= n0 -> P n0 *)
(* ################################################################# *)
(** * Formal vs. Informal Proofs by Induction *)
(** Question: What is the relation between a formal proof of a
proposition [P] and an informal proof of the same proposition [P]?
Answer: The latter should _teach_ the reader how to produce the
former.
Question: How much detail is needed??
Unfortunately, there is no single right answer; rather, there is a
range of choices.
At one end of the spectrum, we can essentially give the reader the
whole formal proof (i.e., the "informal" proof will amount to just
transcribing the formal one into words). This may give the reader
the ability to reproduce the formal one for themselves, but it
probably doesn't _teach_ them anything much.
At the other end of the spectrum, we can say "The theorem is true
and you can figure out why for yourself if you think about it hard
enough." This is also not a good teaching strategy, because often
writing the proof requires one or more significant insights into
the thing we're proving, and most readers will give up before they
rediscover all the same insights as we did.
In the middle is the golden mean -- a proof that includes all of
the essential insights (saving the reader the hard work that we
went through to find the proof in the first place) plus high-level
suggestions for the more routine parts to save the reader from
spending too much time reconstructing these (e.g., what the IH says
and what must be shown in each case of an inductive proof), but not
so much detail that the main ideas are obscured.
Since we've spent much of this chapter looking "under the hood" at
formal proofs by induction, now is a good moment to talk a little
about _informal_ proofs by induction.
In the real world of mathematical communication, written proofs
range from extremely longwinded and pedantic to extremely brief and
telegraphic. Although the ideal is somewhere in between, while one
is getting used to the style it is better to start out at the
pedantic end. Also, during the learning phase, it is probably
helpful to have a clear standard to compare against. With this in
mind, we offer two templates -- one for proofs by induction over
_data_ (i.e., where the thing we're doing induction on lives in
[Type]) and one for proofs by induction over _evidence_ (i.e.,
where the inductively defined thing lives in [Prop]). *)
(* ================================================================= *)
(** ** Induction Over an Inductively Defined Set *)
(** _Template_:
- _Theorem_: <Universally quantified proposition of the form
"For all [n:S], [P(n)]," where [S] is some inductively defined
set.>
_Proof_: By induction on [n].
<one case for each constructor [c] of [S]...>
- Suppose [n = c a1 ... ak], where <...and here we state
the IH for each of the [a]'s that has type [S], if any>.
We must show <...and here we restate [P(c a1 ... ak)]>.
<go on and prove [P(n)] to finish the case...>
- <other cases similarly...> []
_Example_:
- _Theorem_: For all sets [X], lists [l : list X], and numbers
[n], if [length l = n] then [index (S n) l = None].
_Proof_: By induction on [l].
- Suppose [l = []]. We must show, for all numbers [n],
that, if [length [] = n], then [index (S n) [] =
None].
This follows immediately from the definition of [index].
- Suppose [l = x :: l'] for some [x] and [l'], where
[length l' = n'] implies [index (S n') l' = None], for
any number [n']. We must show, for all [n], that, if
[length (x::l') = n] then [index (S n) (x::l') =
None].
Let [n] be a number with [length l = n]. Since
length l = length (x::l') = S (length l'),
it suffices to show that
index (S (length l')) l' = None.
But this follows directly from the induction hypothesis,
picking [n'] to be [length l']. [] *)
(* ================================================================= *)
(** ** Induction Over an Inductively Defined Proposition *)
(** Since inductively defined proof objects are often called
"derivation trees," this form of proof is also known as _induction
on derivations_.
_Template_:
- _Theorem_: <Proposition of the form "[Q -> P]," where [Q] is
some inductively defined proposition (more generally,
"For all [x] [y] [z], [Q x y z -> P x y z]")>
_Proof_: By induction on a derivation of [Q]. <Or, more
generally, "Suppose we are given [x], [y], and [z]. We
show that [Q x y z] implies [P x y z], by induction on a
derivation of [Q x y z]"...>
<one case for each constructor [c] of [Q]...>
- Suppose the final rule used to show [Q] is [c]. Then
<...and here we state the types of all of the [a]'s
together with any equalities that follow from the
definition of the constructor and the IH for each of
the [a]'s that has type [Q], if there are any>. We must
show <...and here we restate [P]>.
<go on and prove [P] to finish the case...>
- <other cases similarly...> []
_Example_
- _Theorem_: The [<=] relation is transitive -- i.e., for all
numbers [n], [m], and [o], if [n <= m] and [m <= o], then
[n <= o].
_Proof_: By induction on a derivation of [m <= o].
- Suppose the final rule used to show [m <= o] is
[le_n]. Then [m = o] and we must show that [n <= m],
which is immediate by hypothesis.
- Suppose the final rule used to show [m <= o] is
[le_S]. Then [o = S o'] for some [o'] with [m <= o'].
We must show that [n <= S o'].
By induction hypothesis, [n <= o'].
But then, by [le_S], [n <= S o']. [] *)
(* Wed Jan 9 12:02:46 EST 2019 *)