IndPrinciples: Induction Principles
Basics
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.
 reflexivity.
 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.
Complete this proof without using the induction tactic.
Exercise: 2 stars, standard, optional (plus_one_r')
☐
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
nonrecursive 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:
Exercise: 1 star, standard, optional (rgb)
☐
Here's another example, this time with one of the constructors
taking some arguments.
Exercise: 1 star, standard, optional (natlist1)
Now what will the induction principle look like?
☐
From these examples, we can extract this general rule:
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.)
 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:
Exercise: 1 star, standard, optional (byntree_ind)
☐
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:
Exercise: 1 star, standard, optional (ex_set)
☐
Polymorphism
Exercise: 1 star, standard, optional (tree)
☐
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
☐
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
☐
Consider the following inductive definition:
Exercise: 1 star, standard, optional (mytype)
Exercise: 1 star, standard, optional (foo)
Exercise: 1 star, standard, optional (foo')
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
... or equivalently:
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.
 reflexivity.

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
 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:
Theorem plus_assoc' : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p.
induction n as [ n'].
 reflexivity.

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'].
 intros m. rewrite < plus_n_O. reflexivity.
 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.
induction m as [ m'].
 simpl. rewrite < plus_n_O. reflexivity.
 simpl. rewrite < IHm'.
rewrite < plus_n_Sm. reflexivity. Qed.
Exercise: 1 star, standard, optional (plus_explicit_prop)
Induction Principles in Prop
 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:
 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.
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 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:
 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:
Theorem ev_ev' : forall n, even n > even' n.
Proof.
apply even_ind.

apply even'_0.

intros m Hm IH.
apply (even'_sum 2 m).
+ apply even'_2.
+ apply IH.
Qed.
Proof.
apply even_ind.

apply even'_0.

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:
This definition can be streamlined a little by observing that the
lefthand 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.
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.>
 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.
 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.