IndPrinciplesInduction Principles
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.
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 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.
Inductive time : Type :=
| day
| night.
Check time_ind :
∀ P : time → Prop,
P day →
P night →
∀ t : time, P t.
| 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.
| 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 x_{1}:a_{1} ... xn:an, that case is:
"For all x_{1}:a_{1} ... xn:an, if [P] holds of each of the arguments of type [t], then [P] holds of [c x_{1} ... xn]" But that oversimplifies a little. An assumption about P holding of an argument x of type t actually occurs immediately after the quantification of x.
Now the induction principle case for nsnoc 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.
∀ P : natlist' → Prop,
P nnil' →
(∀ l : natlist', P l → ∀ n : nat, P (nsnoc l n)) →
∀ n : natlist', P n.
Exercise: 2 stars, standard (booltree_ind)
Here is a type for trees that contain a boolean value at each leaf and branch.
Inductive booltree : Type :=
| bt_empty
| bt_leaf (b : bool)
| bt_branch (b : bool) (t_{1} t_{2} : booltree).
(* What is the induction principle for booltree? Of course you could
ask Coq, but try not to do that. Instead, write it down yourself on
paper. Then look at the definition of booltree_ind_type, below.
It has three missing pieces, which are provided by the definitions
in between here and there. Fill in those definitions based on what
you wrote on paper. *)
Definition booltree_property_type : Type := booltree → Prop.
Definition base_case (P : booltree_property_type) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition leaf_case (P : booltree_property_type) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition branch_case (P : booltree_property_type) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition booltree_ind_type :=
∀ (P : booltree_property_type),
base_case P →
leaf_case P →
branch_case P →
∀ (b : booltree), P b.
| bt_empty
| bt_leaf (b : bool)
| bt_branch (b : bool) (t_{1} t_{2} : booltree).
(* What is the induction principle for booltree? Of course you could
ask Coq, but try not to do that. Instead, write it down yourself on
paper. Then look at the definition of booltree_ind_type, below.
It has three missing pieces, which are provided by the definitions
in between here and there. Fill in those definitions based on what
you wrote on paper. *)
Definition booltree_property_type : Type := booltree → Prop.
Definition base_case (P : booltree_property_type) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition leaf_case (P : booltree_property_type) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition branch_case (P : booltree_property_type) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition booltree_ind_type :=
∀ (P : booltree_property_type),
base_case P →
leaf_case P →
branch_case P →
∀ (b : booltree), P b.
Now check the correctness of your answers by proving the following
theorem. If you have them right, you can complete the proof with
just one tactic: exact booltree_ind. That will work because the
automatically generated induction principle booltree_ind has the
same type as what you just defined.
Exercise: 2 stars, 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 Give an Inductive definition of Toy, such that the induction principle Coq generates is that given above:
Show that your definition is correct by proving the following theorem.
You should be able to instantiate f and g with your two constructors,
then immediately finish the proof with exact Toy_ind. As in the previous
exercise, that will work because the automatically generated induction
principle Toy_ind will have the same type.
Theorem Toy_correct : ∃ f g,
∀ P : Toy → Prop,
(∀ b : bool, P (f b)) →
(∀ (n : nat) (t : Toy), P t → P (g n t)) →
∀ t : Toy, P t.
Proof. (* FILL IN HERE *) Admitted.
☐
∀ P : Toy → Prop,
(∀ b : bool, P (f b)) →
(∀ (n : nat) (t : Toy), P t → P (g n t)) →
∀ t : Toy, P t.
Proof. (* FILL IN HERE *) Admitted.
☐
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.)
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.
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)) →
(∀ 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, 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 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.
... 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.
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.
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.
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.
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
Print ev.
(* ===>
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall 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.
(* ===>
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall 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 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.
| 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 le_{1} : nat → nat → Prop :=
| le1_n : ∀ n, le_{1} n n
| le1_S : ∀ n m, (le_{1} n m) → (le_{1} n (S m)).
Notation "m <=1 n" := (le_{1} m n) (at level 70).
| le1_n : ∀ n, le_{1} n n
| le1_S : ∀ n m, (le_{1} n m) → (le_{1} n (S m)).
Notation "m <=1 n" := (le_{1} 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 le_{2} (n:nat) : nat → Prop :=
| le2_n : le_{2} n n
| le2_S m (H : le_{2} n m) : le_{2} n (S m).
Notation "m <=2 n" := (le_{2} m n) (at level 70).
| le2_n : le_{2} n n
| le2_S m (H : le_{2} n m) : le_{2} n (S m).
Notation "m <=2 n" := (le_{2} 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 n_{0} : nat, n <=1 n_{0} → P n n_{0}.
Check le2_ind :
∀ (n : nat) (P : nat → Prop),
P n →
(∀ m : nat, n <=2 m → P m → P (S m)) →
∀ n_{0} : nat, n <=2 n_{0} → P n_{0}.
∀ P : nat → nat → Prop,
(∀ n : nat, P n n) →
(∀ n m : nat, n <=1 m → P n m → P n (S m)) →
∀ n n_{0} : nat, n <=1 n_{0} → P n n_{0}.
Check le2_ind :
∀ (n : nat) (P : nat → Prop),
P n →
(∀ m : nat, n <=2 m → P m → P (S m)) →
∀ n_{0} : nat, n <=2 n_{0} → P n_{0}.
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 That is why Coq actually generates the induction principle ev_ind that we saw before.
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 that
index (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.
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.
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 P_{0} ⇒ fun P_{1} ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P_{0}
| 1 ⇒ P_{1}
| S (S n') ⇒ PSS n' (f n')
end.
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n : nat, P n → P (S(S n))) →
∀ n : nat , P n :=
fun P ⇒ fun P_{0} ⇒ fun P_{1} ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P_{0}
| 1 ⇒ P_{1}
| 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.
Lemma even_ev : ∀ n, even n = true → ev n.
Proof.
intros.
induction n as [ | |n'] using nat_ind2.
- apply ev_0.
- simpl in H.
inversion H.
- simpl in H.
apply ev_SS.
apply IHn'.
apply H.
Qed.
Proof.
intros.
induction n as [ | |n'] using nat_ind2.
- apply ev_0.
- simpl in H.
inversion H.
- simpl in H.
apply ev_SS.
apply IHn'.
apply H.
Qed.
Exercise: 4 stars, standard, optional (t_tree)
What if we wanted to define binary trees as follows, using a constructor that bundles the children and value at a node into a tuple?
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Inductive t_tree (X : Type) : Type :=
| t_leaf
| t_branch : (t_tree X × X × t_tree X) → t_tree X.
Arguments t_leaf {X}.
Arguments t_branch {X}.
Inductive t_tree (X : Type) : Type :=
| t_leaf
| t_branch : (t_tree X × X × t_tree X) → t_tree X.
Arguments t_leaf {X}.
Arguments t_branch {X}.
Unfortunately, the automatically-generated induction principle is
not as strong as we need. It doesn't introduce induction hypotheses
for the subtrees.
That will get us in trouble if we want to prove something by
induction, such as that reflect is an involution.
Fixpoint reflect {X : Type} (t : t_tree X) : t_tree X :=
match t with
| t_leaf ⇒ t_leaf
| t_branch (l, v, r) ⇒ t_branch (reflect r, v, reflect l)
end.
Theorem reflect_involution : ∀ (X : Type) (t : t_tree X),
reflect (reflect t) = t.
Proof.
intros X t. induction t.
- reflexivity.
- destruct p as [[l v] r]. simpl. Abort.
match t with
| t_leaf ⇒ t_leaf
| t_branch (l, v, r) ⇒ t_branch (reflect r, v, reflect l)
end.
Theorem reflect_involution : ∀ (X : Type) (t : t_tree X),
reflect (reflect t) = t.
Proof.
intros X t. induction t.
- reflexivity.
- destruct p as [[l v] r]. simpl. Abort.
We get stuck, because we have no inductive hypothesis for l or
r. So, we need to define our own custom induction principle, and
use it to complete the proof.
First, define the type of the induction principle that you want to
use. There are many possible answers. Recall that you can use
match as part of the definition.
Definition better_t_tree_ind_type : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Second, define the induction principle by giving a term of that
type. Use the examples about nat, above, as models.
Definition better_t_tree_ind : better_t_tree_ind_type
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Finally, prove the theorem. If induction...using gives you an
error about "Cannot recognize an induction scheme", don't worry
about it. The induction tactic is picky about the shape of the
theorem you pass to it, but it doesn't give you much information
to debug what is wrong about that shape. You can use apply
instead, as we saw at the beginning of this file.
Theorem reflect_involution : ∀ (X : Type) (t : t_tree X),
reflect (reflect t) = t.
Proof. (* FILL IN HERE *) Admitted.
☐
reflect (reflect t) = t.
Proof. (* FILL IN HERE *) Admitted.
☐
(* 2023-11-27 14:50 *)