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:

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:

while the inductive proposition definition was named `le`

and provided in the **IndProp** chapter:

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`

:

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:

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.

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:

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:Now we have what we need. By applying `IHn'`

and finally applying `H`

, we can complete this proof:

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

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:

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_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:

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.