The Coq mailing list

[jd AT sophia.inria.fr (Joelle Despeyroux)]

> In general a double induction is simply solved by an induction on the
> first predicate (using Elim) followed by an Inversion over the second
> hypothesis.

Right.  The problem is that Coq does not perform correct induction on
partially instanciated terms.

Christine is right. However, the "trick" does not solve the problem in
those cases where the induction hypothesis on the second predicate are
needed to perform the proof. This is rather usual in proofs on
semantics such as proofs of correctness of a compiler, for example.

For those cases, a simple "trick" always work: Change your goal to
avoid the instanciation of variables of the second predicate when
performing induction on the first predicate.  For instance:

Change: Goal (n:nat)(even n)->(odd n)->False.
to:     Goal (n:nat)(even n)->(m:nat) (odd m)-> (m=n) -> False.

No doubt this is not the intuitive double induction we have in mind!
Anyway, the implementation is correct.

  Joelle Despeyroux.