Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] dealing with mutually-inductive definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dealing with mutually-inductive definitions


chronological Thread 
  • From: Adam Chlipala <adamc AT cs.berkeley.edu>
  • To: Noam Zeilberger <noam+coq AT cs.cmu.edu>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] dealing with mutually-inductive definitions
  • Date: Thu, 02 Aug 2007 17:46:46 -0700
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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/





Archive powered by MhonArc 2.6.16.

Top of Page