The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Noam Zeilberger wrote:
> I was wondering if there is some sort of tutorial/FAQ for working with
> mutually-(co)inductive definitions in Coq?  I'm looking for something
> more than just the documentation of the Scheme command.  For example,
> what is the most natural way of taking an ordinary mathematical proof
> of a list of theorems by simultaneous induction, and encoding it in
> the tactic language?  Has anyone done any significant amount of
> theorem-proving using mutually-inductive definitions with more than
> (say) three branches?
>   

Here's an example of a closure conversion correctness proof that uses a 
four-way mutual induction principle (created by Scheme):
http://ltamer.cvs.sourceforge.net/ltamer/ctpc/src/coq/CCify.v?revision=1.38

I don't know if that file uses the best way to begin a mutual induction 
proof in Coq, but it's the most primitive way of doing so: manual 
application of the appropriate mutual induction principle to the IH 
specification for each of the types.

The code for that project overall is available at:
   http://ltamer.sourceforge.net/