The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Ersoy Bayramoglu wrote:
> The Coq wiki has information on generating mutual induction principles 
> which look quite heavy weight for this sort of thing. Because if I 
> assume one of the lemmas, proving the other one is really trivial. If 
> it's the only way, how can i use the induction principal generated by 
> Scheme - or Combined Scheme - for these proofs?

I think this is the only way to go, up to isomorphism.  That is, you 
could manually build the induction principles that [Scheme] builds, or 
you could write a direct mutual [fix] customized to your theorem, but 
that wouldn't really make things easier.

The best way I know to apply mutual induction principles is to
1) Pick just one of the N theorems that you will prove and declare it as 
a goal.
2) Run [intro] enough to get to the point where...
3) ...you can run [apply (name_of_mutual_ind theorem_statement1 ... 
theorem_statementN)].

That is, your initial theorem will just be proving the version of the 
theorem for one of the mutual datatypes, but in the proof you must state 
abstracted versions of the theorem for each mutual datatype, including 
the one you've already stated.  After the [apply], you should see goals 
that require no special induction machinery.

It's also worth realizing that the mutual induction principles aren't 
magic.  After running a [Scheme] command, each of the principles you 
name is bound to the identifier you gave for it, so you can see the type 
of each with [Check name_of_mutual_ind].  The type completely implies 
the procedure I just suggested.  You've probably held off on doing that 
so far because you're assuming that there's better standard tactic 
support for mutual induction, but, as far as I know, there isn't; and, 
of course, I'd love to be proven wrong by another list participant.