The Coq mailing list

[Ersoy Bayramoglu <ersoy.bayramoglu AT epfl.ch>]

Thanks for the explanation. I managed to prove the theorems. Scheme  
didn't turn out to be as scary as it looked after all. If anyone knows  
any alternative way, it would be interesting to hear it, though.

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