Skip to Content.
Sympa Menu

coq-club - [Coq-Club] A small tutorial (attempt) about "advanced" induction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A small tutorial (attempt) about "advanced" induction


chronological Thread 
  • From: Emmanuel Polonowski <polonowski AT u-pec.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] A small tutorial (attempt) about "advanced" induction
  • Date: Thu, 1 Dec 2011 18:18:40 +0100

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
---------------------------------------------------------------






Archive powered by MhonArc 2.6.16.

Top of Page