IndPrinciplesInduction Principles
Set Warnings "-notation-overridden,-parsing".
From LF Require Export ProofObjects.
From LF Require Export ProofObjects.
Basics
Check nat_ind.
(* ===> nat_ind :
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n *)
(* ===> 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' : ∀ n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
- (* n = O *) reflexivity.
- (* n = S n' *) simpl. intros n' IHn'. rewrite → IHn'.
reflexivity. Qed.
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, optional (plus_one_r')
Complete this proof without using the induction tactic.
Theorem plus_one_r' : ∀ n:nat,
n + 1 = S n.
Proof.
(* FILL IN HERE *) Admitted.
☐
n + 1 = S n.
Proof.
(* FILL IN HERE *) Admitted.
t_ind : ∀ P : t → Prop,
... case for c_{1} ... →
... case for c_{2} ... → ...
... 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:
... case for c_{1} ... →
... case for c_{2} ... → ...
... case for cn ... →
∀ n : t, P n
Inductive yesno : Type :=
| yes : yesno
| no : yesno.
Check yesno_ind.
(* ===> yesno_ind : forall P : yesno -> Prop,
P yes ->
P no ->
forall y : yesno, P y *)
| yes : yesno
| no : yesno.
Check yesno_ind.
(* ===> yesno_ind : forall P : yesno -> Prop,
P yes ->
P no ->
forall y : yesno, P y *)
Exercise: 1 star, 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 : rgb
| green : rgb
| blue : rgb.
Check rgb_ind.
☐
| red : rgb
| green : rgb
| blue : rgb.
Check rgb_ind.
Inductive natlist : Type :=
| nnil : natlist
| ncons : nat → natlist → 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 *)
| nnil : natlist
| ncons : nat → natlist → 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, optional (natlist1)
Suppose we had written the above definition a little differently:
Inductive natlist1 : Type :=
| nnil1 : natlist1
| nsnoc1 : natlist1 → nat → natlist1.
| 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 a_{1} ... 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 x_{1}...xn of types a_{1}...an, if P holds for each of the inductive arguments (each xi of type t), then P holds for c x_{1} ... xn".
Exercise: 1 star, 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 : byntree
| bleaf : yesno → byntree
| nbranch : yesno → byntree → byntree → byntree.
☐
| bempty : byntree
| bleaf : yesno → byntree
| nbranch : yesno → byntree → byntree → byntree.
Exercise: 1 star, optional (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:
∀ P : ExSet → Prop,
(∀ b : bool, P (con1 b)) →
(∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →
∀ e : ExSet, P e
Inductive ExSet : Type :=
(* FILL IN HERE *)
.
☐
(* FILL IN HERE *)
.
Polymorphism
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:
| nil : list X
| cons : X → list X → list 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 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.
∀ (X : Type) (P : list X → Prop),
P [] →
(∀ (x : X) (l : list X), P l → P (x :: l)) →
∀ l : list X, P l
Exercise: 1 star, 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 → tree X
| node : tree X → tree X → tree X.
Check tree_ind.
☐
| leaf : X → tree X
| node : tree X → tree X → tree X.
Check tree_ind.
Exercise: 1 star, optional (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
☐
∀ (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)) →
(∀ f_{1} : nat → foo X Y,
(∀ n : nat, P (f_{1} n)) → P (quux X Y f_{1})) →
∀ f_{2} : foo X Y, P f_{2}
☐
∀ (X Y : Type) (P : foo X Y → Prop),
(∀ x : X, P (bar X Y x)) →
(∀ y : Y, P (baz X Y y)) →
(∀ f_{1} : nat → foo X Y,
(∀ n : nat, P (f_{1} n)) → P (quux X Y f_{1})) →
∀ f_{2} : foo X Y, P f_{2}
Exercise: 1 star, optional (foo')
Consider the following inductive definition:
Inductive foo' (X:Type) : Type :=
| C_{1} : list X → foo' X → foo' X
| C_{2} : foo' X.
| C_{1} : list X → foo' X → foo' X
| C_{2} : 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, ________________________
∀ (X : Type) (P : foo' X → Prop),
(∀ (l : list X) (f : foo' X),
_______________________ →
_______________________ ) →
___________________________________________ →
∀ f : foo' X, ________________________
Induction Hypotheses
∀ 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 (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.
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ n : nat, P n
Definition P_m0r (n:nat) : Prop :=
n * 0 = 0.
n * 0 = 0.
... or equivalently:
Definition P_m0r' : nat→Prop :=
fun n ⇒ n * 0 = 0.
fun n ⇒ n * 0 = 0.
Now it is easier to see where P_m0r appears in the proof.
Theorem mult_0_r'' : ∀ 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.
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 ∀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 (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
- 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.
Theorem plus_assoc' : ∀ 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.
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' : ∀ 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.
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 ∀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.
(* 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.
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, 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
Inductive ev : nat → Prop :=
| ev_0 : ev 0
| ev_SS : ∀ n : nat, ev n → ev (S (S n)).
...to give rise to an induction principle that looks like this...
| ev_0 : ev 0
| ev_SS : ∀ n : nat, ev n → ev (S (S n)).
ev_ind_max : ∀ P : (∀ n : nat, ev n → Prop),
P O ev_0 →
(∀ (m : nat) (E : ev m),
P m E →
P (S (S m)) (ev_SS m E)) →
∀ (n : nat) (E : ev n),
P n E
... because:
P O ev_0 →
(∀ (m : nat) (E : ev m),
P m E →
P (S (S m)) (ev_SS m E)) →
∀ (n : nat) (E : ev n),
P n E
- Since ev is indexed by a number n (every ev 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 (ev
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.
- We must prove that P holds for O and ev_0.
- 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.
∀ P : nat → Prop,
... →
∀ n : nat,
even n → P n
For this reason, Coq actually generates the following simplified
induction principle for ev:
... →
∀ n : nat,
even n → P n
Check ev_ind.
(* ===> ev_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, ev n -> P n -> P (S (S n))) ->
forall n : nat,
ev n -> P n *)
(* ===> ev_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, ev n -> P n -> P (S (S n))) ->
forall n : nat,
ev 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:
As expected, we can apply ev_ind directly instead of using
induction. For example, we can use it to show that ev' (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 ev:
- 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).
- P holds for 0,
Theorem ev_ev' : ∀ n, ev n → ev' n.
Proof.
apply ev_ind.
- (* ev_0 *)
apply ev'_0.
- (* ev_SS *)
intros m Hm IH.
apply (ev'_sum 2 m).
+ apply ev'_2.
+ apply IH.
Qed.
Proof.
apply ev_ind.
- (* ev_0 *)
apply ev'_0.
- (* ev_SS *)
intros m Hm IH.
apply (ev'_sum 2 m).
+ apply ev'_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)). *)
| 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, (le n m) → (le n (S m)).
Notation "m ≤ n" := (le m n).
| le_n : le n n
| le_S : ∀ m, (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 n_{0} : nat, n <= n_{0} -> P n_{0} *)
(* ===> forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall n_{0} : nat, n <= n_{0} -> P n_{0} *)
Formal vs. Informal Proofs by Induction
Induction Over an Inductively Defined Set
- Theorem: <Universally quantified proposition of the form
"For all n:S, P(n)," where S is some inductively defined
set.>
- Suppose n = c a_{1} ... 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 a_{1} ... ak)>.
- <other cases similarly...> ☐
- Suppose n = c a_{1} ... 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 a_{1} ... ak)>.
- Theorem: For all sets X, lists l : list X, and numbers
n, if length l = n then index (S n) l = None.
- Suppose l = []. We must show, for all numbers n,
that, if length [] = n, then index (S n) [] =
None.
- 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.
length l = length (x::l') = S (length l'),it suffices to show thatindex (S (length l')) l' = None.But this follows directly from the induction hypothesis, picking n' to be length l'. ☐
- Suppose l = []. We must show, for all numbers n,
that, if length [] = n, then index (S n) [] =
None.
Induction Over an Inductively Defined Proposition
- 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")>
- 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>.
- <other cases similarly...> ☐
- 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>.
- Theorem: The ≤ relation is transitive — i.e., for all
numbers n, m, and o, if n ≤ m and m ≤ o, then
n ≤ 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'.
- 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.