The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Adam Koprowski a écrit :
> On Mon, Mar 16, 2009 at 17:28, dimitrisg7 <dvekris AT hotmail.com 
> <mailto:dvekris AT hotmail.com>> wrote:
>
>     [...] I would be happy if I could have something like:
>
>     Inductive data_prop ...
>     ...
>     ...
>     with Fixpoint func (data_prop).
>
>  That's a very good question indeed.  I was wondering about that 
> myself. In my work I'll also need an inductively defined tree-like 
> data-structure whose component's type depends on the subtree, hence 
> I'd like to compute it with a (mutually recursive) Fixpoint function.
>   Are there any theoretical concerns when combining Inductive and 
> Fixpoint definitions or is it not possible to do that in Coq for 
> technical reasons only? Any neat way to side-step this limitation? The 
> obvious one is to turn the Fixpoint function into a relation and 
> define it inductively, but that makes instantiating and working with 
> such data-types much less pleasent...
>  
This kind of definition is called "inductive-recursive" in the 
literature. This is not a theoretical problem. See for instance 
http://pauillac.inria.fr/coq/mailing-lists/coqclub/200210/msg00025.html 
for some discussion about that.