IndPrinciplesInduction Principles
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export ProofObjects.
From LF Require Export ProofObjects.
Basics
In English: Suppose P is a property of natural numbers (that is,
P n is a Prop for every n). To show that P n holds of all
n, it suffices to show:
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
Induction chapter.
- P holds of 0
- for any n, if P holds of n, then P holds of S n.
Theorem mul_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.
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.
Third, we had to manually supply the name of the induction principle
with apply, but induction figures that out itself.
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 (plus_one_r')
Complete this proof without using the induction tactic.t_ind : ∀ P : t → Prop,
... case for c1 ... →
... case for c2 ... → ...
... case for cn ... →
∀ n : t, P n
Inductive time : Type :=
| day
| night.
Check time_ind :
∀ P : time → Prop,
P day →
P night →
∀ t : time, P t.
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 natlist : Type :=
| nnil
| ncons (n : nat) (l : natlist).
Check natlist_ind :
∀ P : natlist → Prop,
P nnil →
(∀ (n : nat) (l : natlist),
P l → P (ncons n l)) →
∀ l : natlist, P l.
In general, the automatically generated induction principle for
inductive type t is formed as follows:
For example, suppose we had written the definition of natlist a little
differently:
- Each constructor c generates one case of the principle.
- If c takes no arguments, that case is:
"P holds of c" - If c takes arguments x1:a1 ... xn:an, that case is:
"For all x1:a1 ... xn:an, if [P] holds of each of the arguments of type [t], then [P] holds of [c x1 ... xn]"
Now the induction principle case for nsnoc1 is a bit different
than the earlier case for ncons:
Check natlist'_ind :
∀ P : natlist' → Prop,
P nnil' →
(∀ l : natlist', P l → ∀ n : nat, P (nsnoc l n)) →
∀ n : natlist', P n.
Exercise: 1 star, standard (booltree_ind)
In the comment below, write out the induction principle that Coq will generate for the following datatype.Inductive booltree : Type :=
| bt_empty
| bt_leaf (b : bool)
| bt_branch (b : bool) (t1 t2 : booltree).
(* FILL IN HERE:
... *)
(* Do not modify the following line: *)
Definition manual_grade_for_booltree_ind : option (nat×string) := None.
☐
Exercise: 1 star, standard (toy_ind)
Here is an induction principle for a toy type:∀ P : Toy → Prop,
(∀ b : bool, P (con1 b)) →
(∀ (n : nat) (t : Toy), P t → P (con2 n t)) →
∀ t : Toy, P t
Inductive Toy : Type :=
(* FILL IN HERE *)
.
(* Do not modify the following line: *)
Definition manual_grade_for_toy_ind : option (nat×string) := None.
☐
Polymorphism
Inductive list (X:Type) : Type :=
| 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
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.Exercise: 1 star, standard, 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
Exercise: 1 star, standard, 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, standard, optional (foo')
Consider the following inductive definition:
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, ________________________
☐
foo'_ind :
∀ (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
... or equivalently:
Now it is easier to see where P_m0r appears in the proof.
Theorem mul_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.
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 add_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' *)
simpl. rewrite → IHn'. reflexivity. Qed.
It also works to apply induction to a variable that is
quantified in the goal.
Theorem add_comm' : ∀ n m : nat,
n + m = m + n.
Proof.
induction n as [| n'].
- (* n = O *) intros m. rewrite → add_0_r. 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 add_comm'' : ∀ n m : nat,
n + m = m + n.
Proof.
(* Let's do induction on m this time, instead of n... *)
induction m as [| m']. (* n is already introduced into the context *)
- (* m = O *) simpl. rewrite → add_0_r. reflexivity.
- (* m = S m' *) simpl. rewrite <- IHm'.
rewrite <- plus_n_Sm. reflexivity. Qed.
Exercise: 1 star, standard, optional (plus_explicit_prop)
Rewrite both add_assoc' and add_comm' and their proofs in the same style as mul_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 for Propositions
Inductive ev'' : nat → Prop :=
| ev_0 : ev'' 0
| ev_SS (n : nat) : ev'' n → ev'' (S (S n)).
Check ev''_ind :
∀ P : nat → Prop,
P 0 →
(∀ n : nat, ev'' n → P n → P (S (S n))) →
∀ n : nat, ev'' n → P n.
In English, ev''_ind says: Suppose P is a property of natural
numbers. To show that P n holds whenever n is even, it suffices
to show:
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'':
- P holds for 0,
- for any n, if n is even and P holds for n, then P holds for S (S n).
Inductive ev' : nat → Prop :=
| ev'_0 : ev' 0
| ev'_2 : ev' 2
| ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m).
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.
The precise form of an Inductive definition can affect the
induction principle Coq generates.
Inductive le1 : nat → nat → Prop :=
| le1_n : ∀ n, le1 n n
| le1_S : ∀ n m, (le1 n m) → (le1 n (S m)).
Notation "m <=1 n" := (le1 m n) (at level 70).
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 le2 (n:nat) : nat → Prop :=
| le2_n : le2 n n
| le2_S m (H : le2 n m) : le2 n (S m).
Notation "m <=2 n" := (le2 m n) (at level 70).
The second one is better, even though it looks less symmetric.
Why? Because it gives us a simpler induction principle.
Check le1_ind :
∀ P : nat → nat → Prop,
(∀ n : nat, P n n) →
(∀ n m : nat, n <=1 m → P n m → P n (S m)) →
∀ n n0 : nat, n <=1 n0 → P n n0.
Check le2_ind :
∀ (n : nat) (P : nat → Prop),
P n →
(∀ m : nat, n <=2 m → P m → P (S m)) →
∀ n0 : nat, n <=2 n0 → P n0.
Another Form of Induction Principles on Propositions (Optional)
∀ 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
- 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 (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 m is an even number and E
is an evidence of its evenness, if P holds of m and
E, then it also holds of S (S m) and ev_SS m 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
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 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)>.
- <other cases similarly...> ☐
- 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)>.
- 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'),
index (S (length l')) 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.
Explicit Proof Objects for Induction (Optional)
There's nothing magic about this induction lemma: it's just
another Coq lemma that requires a proof. Coq generates the proof
automatically too...
We can rewrite that more tidily as follows:
Fixpoint build_proof
(P : nat → Prop)
(evPO : P 0)
(evPS : ∀ n : nat, P n → P (S n))
(n : nat) : P n :=
match n with
| 0 ⇒ evPO
| S k ⇒ evPS k (build_proof P evPO evPS k)
end.
Definition nat_ind_tidy := build_proof.
(P : nat → Prop)
(evPO : P 0)
(evPS : ∀ n : nat, P n → P (S n))
(n : nat) : P n :=
match n with
| 0 ⇒ evPO
| S k ⇒ evPS k (build_proof P evPO evPS k)
end.
Definition nat_ind_tidy := build_proof.
We can read build_proof as follows: Suppose we have
evidence evPO that P holds on 0, and evidence evPS that ∀
n:nat, P n → P (S n). Then we can prove that P holds of an
arbitrary nat n using recursive function build_proof, which
pattern matches on n:
Recursive function build_proof thus pattern matches against
n, recursing all the way down to 0, and building up a proof
as it returns.
The actual nat_ind that Coq generates uses a recursive
function F defined with fix instead of Fixpoint.
We can adapt this approach to proving nat_ind to help prove
non-standard induction principles too. As a motivating example,
suppose that we want to prove the following lemma, directly
relating the ev predicate we defined in IndProp
to the even function defined in Basics.
- If n is 0, build_proof returns evPO to show that P n
holds.
- If n is S k, build_proof applies itself recursively on k to obtain evidence that P k holds; then it applies evPS on that evidence to show that P (S n) holds.
Lemma even_ev : ∀ n: nat, even n = true → ev'' n.
Proof.
induction n; intros.
- apply ev_0.
- destruct n.
+ simpl in H. inversion H.
+ simpl in H.
apply ev_SS.
Abort.
Attempts to prove this by standard induction on n fail in the case for
S (S n), because the induction hypothesis only tells us something about
S n, which is useless. There are various ways to hack around this problem;
for example, we can use ordinary induction on n to prove this (try it!):
Lemma even_ev' : ∀ n : nat,
(even n = true → ev n) ∧ (even (S n) = true → ev (S n)).
But we can make a much better proof by defining and proving a
non-standard induction principle that goes "by twos":
Definition nat_ind2 :
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n : nat, P n → P (S(S n))) →
∀ n : nat , P n :=
fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P0
| 1 ⇒ P1
| S (S n') ⇒ PSS n' (f n')
end.
Once you get the hang of it, it is entirely straightforward to
give an explicit proof term for induction principles like this.
Proving this as a lemma using tactics is much less intuitive.
The induction ... using tactic variant gives a convenient way to
utilize a non-standard induction principle like this.