June 23, 2017

# 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.