Home
Understanding Induction Hypothesis Variation in Coq
After several days of beating my mind against a proof in Coq, I now have a better appreciation for when to generalize an inductive hypothesis so as to be able to apply it within a proof. To help me, and hopefully others, understand it better I walk through the proof below, pointing out where I went wrong and how I used induction hypothesis variation to eventually succeed.
First some background is in order. I was working through the “le_exercises” section of the IndProp chapter of Benjamin Pierce’s Software Foundations book. There are several problem theorems in that section, but the three I struggled with were:
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof. Admitted.
Theorem leb_correct : forall n m, n <= m -> leb n m = true.
Proof. Admitted.
Theorem leb_iff : forall n m, leb n m = true <-> n <= m.
Proof. Admitted.
From a high level it’s easy to see where this is going. We are to prove that the boolean and inductive proposition definitions of “less than or equal to” are equivalent to each other. Theorem leb_complete implies in one direction, theorem leb_correct implies in the other, and theorem leb_iff pulls them together to assert equivalence. To recap, the boolean definition was named leb and was provided in the Basics chapter:
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
while the inductive proposition definition was named le and provided in the IndProp chapter:
Inductive le : nat -> nat -> Prop :=
| le_n : forall n, le n n
| le_S : forall n m, (le n m) -> (le n (S m)).
It’s not difficult to convince oneself that these definitions are equivalent; convincing Coq is another matter.
Theorem leb_complete
This first theorem states that the boolean definition leb implies the inductive proposition definition le for any two numbers n and m. I sensed induction would be needed, so I started by inducting on n:
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof.
intros n m H. induction n as [| n' IHn'].
(* === GOAL STACK =================================================== *)
2 subgoals
m : nat
H : leb 0 m = true
______________________________________(1/2)
0 <= m
______________________________________(2/2)
S n' <= m
Attempting to prove the first subgoal using simple case analysis (i.e., destruct) on m gets us nowhere; once everything is simplified, we have no way to relate the goal with a hypothesis, so we’re stuck:
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof.
intros n m H. induction n as [| n' IHn'].
- destruct m.
+ apply le_n.
+ apply le_S. (* Stuck here *)
(* === GOAL STACK =================================================== *)
1 subgoal
m : nat
H : leb 0 (S m) = true
______________________________________(1/1)
0 <= m
To get around this, we can induct on m instead of simply case analyzing. This gives us an induction hypothesis IHm' that we can use to convert our goal from its inductive proposition into the boolean definition that we want to show implication for.
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof.
intros n m H. induction n as [| n' IHn'].
- induction m as [| m' IHm'].
+ apply le_n.
+ apply le_S. apply IHm'. apply H.
(* === GOAL STACK =================================================== *)
This subproof is complete, but there are some unfocused goals:
______________________________________(1/1)
S n' <= m
Now we need to prove the inductive case for our induction on n. Although we can start off the same way as the base case and induct on m again, it turns out we don’t need an induction hypothesis for m here. Thus we can either induct on m or case analyze it; I’ll choose the latter:
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof.
intros n m H. induction n as [| n' IHn'].
- induction m as [| m' IHm'].
+ apply le_n.
+ apply le_S. apply IHm'. apply H.
- destruct m.
+ simpl. inversion H.
+ simpl. apply n_le_m__Sn_le_Sm.
(* === GOAL STACK =================================================== *)
1 subgoal
n', m : nat
H : leb (S n') (S m) = true
IHn' : leb n' (S m) = true -> n' <= S m
______________________________________(1/1)
n' <= m
Everything goes smoothly right up until it comes time to apply the inductive hypothesis IHn'. We simply can’t do it; our goal is n' <= m, but the inductive hypothesis relates n' <= S m to leb.
The problem here is that the variable m was introduced before the induction step on n. In other words, we fixed a single value for m prior to formulating the induction hypothesis, rather than allowing m to be any arbitrary value. This means that when we case analyze m in the inductive step, the induction hypothesis IHn' is also modified; specifically, all occurrences of m become S m. To be absolutely clear, the over-specific IHn' we have is:
IHn' : leb n' (S m) = true -> n' <= S m
but the IHn' we really want is more general:
IHn' : forall m : nat, leb n' m = true -> n' <= m
How do we get this latter, more general IHn'? By introducing only n prior to inducting over n, and thereby leaving m general. To do so, we return to the beginning of the proof and replace intros n m H with just intros n, then modify each proof step to intros everything else at the last possible moment:
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof.
intros n. induction n as [| n' IHn'].
- induction m as [| m' IHm'].
+ intros H. apply le_n.
+ intros H. apply le_S. apply IHm'. apply H.
- destruct m.
+ simpl. intros H. inversion H.
+ simpl. intros H. apply n_le_m__Sn_le_Sm.
(* === GOAL STACK =================================================== *)
1 subgoal
n' : nat
IHn' : forall m : nat, leb n' m = true -> n' <= m
m : nat
H : leb n' m = true
______________________________________(1/1)
n' <= m
Now we have what we need. By applying IHn' and finally applying H, we can complete this proof:
Theorem leb_complete : forall n m, leb n m = true -> n <= m.
Proof.
intros n. induction n as [| n' IHn'].
- induction m as [| m' IHm'].
+ intros H. apply le_n.
+ intros H. apply le_S. apply IHm'. apply H.
- destruct m.
+ simpl. intros H. inversion H.
+ simpl. intros H. apply n_le_m__Sn_le_Sm. apply IHn'. apply H.
Qed.
Theorem leb_correct
Now the implication is reversed: we’re proving that the inductive proposition definition le implies the boolean definition leb for any two numbers n and m. The book hints that induction on m is easier, so that’s what I started with. Unlike the previous theorem, we don’t need to induct on or even destruct n in the base case; we can see that n must be 0 and thus leb n 0 is trivially true. But like the previous theorem, we need to break up n into its two possible forms in the inductive step. And as was true above, we don’t need a separate induction hypothesis for n, so while either induction or case analysis works equally well here, I chose simple case analysis:
Theorem leb_correct : forall n m, n <= m -> leb n m = true.
Proof.
intros n m H. induction m as [| m' IHm'].
- inversion H. symmetry. apply leb_refl.
- destruct n.
+ reflexivity.
+ simpl. (* Stuck here *)
(* === GOAL STACK =================================================== *)
1 subgoal
n, m' : nat
H : S n <= S m'
IHm' : S n <= m' -> leb (S n) m' = true
______________________________________(1/1)
leb n m' = true
Once again, we’re stuck. We have a goal of leb n m' = true, but our induction hypothesis IHm' relating leb to le requires leb (S n) m' = true. As above, the culprit is our introduction of n before inducting over m. What we really want is:
IHm' : forall n : nat, n <= m' -> leb n m' = true
But for this proof, simply replacing intros with intros m won’t work. Why? Because m is defined after n; if we say intros m, Coq will give the first nat the name m, then proceed to do induction on that first variable rather than the second.
Instead, we must use the generalize dependent tactic. We first use intros to introduce everything, then use generalize dependent n to tell Coq to go back and make n general; it’s as if n (and everything else that references n, in this proof H) was never introduced in the first place. Of course, after doing this, we also have to introduce n and H locally in each inductive case:
Theorem leb_correct : forall n m, n <= m -> leb n m = true.
Proof.
intros. generalize dependent n. induction m as [| m' IHm'].
- intros n H. inversion H. symmetry. apply leb_refl.
- intros n H. destruct n.
+ reflexivity.
+ simpl.
(* === GOAL STACK =================================================== *)
1 subgoal
m' : nat
IHm' : forall n : nat, n <= m' -> leb n m' = true
n : nat
H : S n <= S m'
______________________________________(1/1)
leb n m' = true
We now have what we need. The induction hypothesis IHm' is now usable, allowing us to apply it and continue with the final two steps of the proof:
Theorem leb_correct : forall n m, n <= m -> leb n m = true.
Proof.
intros. generalize dependent n. induction m as [| m' IHm'].
- intros n H. inversion H. symmetry. apply leb_refl.
- intros n H. destruct n.
+ reflexivity.
+ simpl. apply IHm'. apply Sn_le_Sm__n_le_m in H. apply H.
Qed.
Theorem leb_iff
To pull everything together we have theorem leb_iff, which proves leb and le to be equivalent definitions of the “less than or equal to” relation. Equivalence is simply bidirectional implication, and since the hard work has already been done above to show implication in both directions, equivalence follows easily:
Theorem leb_iff : forall n m, leb n m = true <-> n <= m.
Proof.
split.
- apply leb_complete.
- apply leb_correct.
Qed.
Altogether, trying to figure these proofs out was maddeningly difficult; it involved several hours and some table-pounding. But when I finally got them, it drove home the importance of keeping hypotheses as general as possible so as to be able to use them in as many places as possible. This is also the first set of proofs I’ve done in Coq that hits at one of the areas I’m interested in, namely proving that two different definitions of the same “thing” are in fact equivalent.