The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

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