The Coq mailing list

[Emmanuel Polonowski <polonowski AT u-pec.fr>]

Dear Coq-Club readers,

While formalizing the meta-theory of my current work, I wrote a compilation 
of several simple case studies about "advanced" inductive definition and 
proofs (i.e. with nested list, on non-structural argument, etc.). Those 
examples could be useful for beginners with Coq like me that get stuck with 
what seems to be usual difficulties, well-covered by various documents but 
not accessible in a single one (afaik).

The source file and html doc are attached at this email. Any comments and 
improvements are very welcome, as well as any explanations w.r.t. the 3 
questions I left un-answered (for the moment, I hope) :

   QUESTION 1 :
   Why Fixpoint definition over term with nested list works
   with fold_right but not with a user-defined auxiliary function
   that does essentially the same as fold_right ?

   QUESTION 2 :
   Why Function definition is not possible with nested fix
   definition ?

   QUESTION 3 :
   How can Coq build a valid definition on the top of an inductive
   definition that doesn't proceed by structural induction ?

Best regards,
Emmanuel Polonowski

Attachment: Tutorial_Induction_part_1.v
Description: Binary data

--
---------------------------------------------------------------
Emmanuel Polonowski
Université Paris-Est Créteil - LACL - ESIAG
http://lacl.u-pec.fr/polonowski
---------------------------------------------------------------