coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/
- [Coq-Club] dealing with mutually-inductive definitions, Noam Zeilberger
- Re: [Coq-Club] dealing with mutually-inductive definitions, Noam Zeilberger
- <Possible follow-ups>
- [Coq-Club] dealing with mutually-inductive definitions,
Noam Zeilberger
- Re: [Coq-Club] dealing with mutually-inductive definitions, Adam Chlipala
- Re: [Coq-Club] dealing with mutually-inductive definitions, Xavier Leroy
- Re: [Coq-Club] dealing with mutually-inductive definitions, Matthieu . Sozeau
- Re: [Coq-Club] dealing with mutually-inductive definitions, Matthieu . Sozeau
Archive powered by MhonArc 2.6.16.