coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robert Dockins <robdockins AT fastmail.fm>
- To: Coq Mailing List <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] odd termination issue
- Date: Sat, 16 Feb 2008 22:14:46 -0500
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Saturday 16 February 2008 08:17:10 pm Brian Aydemir wrote:
> Robert Dockins wrote:
> > The issue is that I would like to reuse a fancy finite map
> > datastructure in a datatype definition. ...
> >
> > Has anyone else encountered this problem and is there a better
> > solution?
>
> It is possible to avoid reinventing the wheel. There has been some
> previous discussion on this topic:
>
> - Inductive definitions that go through lists:
> http://pauillac.inria.fr/pipermail/coq-club/2007/003224.html
>
> - How Coq checks the well-formedness of recursive calls:
> http://pauillac.inria.fr/pipermail/coq-club/2008/003390.html
>
> Below, I give one take on your example. The code's a bit much at
> first glance, but the first part can go in some library (you could
> instead define the exact version of list_pair_snd_ind that you need)
> and the third part proves a useful induction principle for your
> datatype.
>
> Cheers,
> Brian
[snip code example]
Interesting. It looks like the problem is that I was defining the function
in
question via mutual recursion, when instead I should have defined/used a
generic traversal function for the map. It's pretty counterintuitive to me
that Coq is willing to look "through" a previously defined function to
discover properly formed recursive calls but not through a function defined
by mutual recursion. However, reading the second reference from above, it
looks like using section variables might also affect the outcome...
Anyway, thanks for pointing me in the right direction; I think I can get this
figured out now.
Rob Dockins
- [Coq-Club] odd termination issue, Robert Dockins
- Re: [Coq-Club] odd termination issue,
Brian Aydemir
- Re: [Coq-Club] odd termination issue, Robert Dockins
- Re: [Coq-Club] odd termination issue,
Robin Green
- Re: [Coq-Club] odd termination issue, Yves Bertot
- Re: [Coq-Club] odd termination issue,
Robin Green
- Re: [Coq-Club] odd termination issue, Robert Dockins
- Re: [Coq-Club] odd termination issue,
Brian Aydemir
Archive powered by MhonArc 2.6.16.