The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

On Mon, Mar 16, 2009 at 17:28, dimitrisg7 <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...

 

On Mon, Mar 16, 2009 at 17:41, Edsko de Vries <devriese AT cs.tcd.ie> wrote:
> It has been my experience that giving such definitions as separate
> hypothesis leads to much simpler proofs; but perhaps others will
> disagree with me completely :)

  I don't understand what you mean by separating hypothesis. How would you separate the definitions if they are mutually recursive??

 
  Cheers,
   Adam

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================