coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
---------------------------------------------------------------
- [Coq-Club] A small tutorial (attempt) about "advanced" induction, Emmanuel Polonowski
Archive powered by MhonArc 2.6.16.