Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] dealing with mutually-inductive definitions


chronological Thread 
  • From: Noam Zeilberger <noam+ AT cs.cmu.edu>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] dealing with mutually-inductive definitions
  • Date: Wed, 1 Aug 2007 17:01:57 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

Noam





Archive powered by MhonArc 2.6.16.

Top of Page