The Coq mailing list

[Frederic Blanqui <blanqui AT lix.polytechnique.fr>]

On Tue, 22 Oct 2002, Lionel Elie Mamane wrote:

> On Tue, Oct 22, 2002 at 03:51:28PM +0200, Eduardo Gimenez wrote:
> 
> > No, you can not do case analysis on the type you are introducing in the
> > definition of the type itself (I can hardly imagine what the semantics of
> > such construction could be :-).

This is what is called an inductive-recursive type. See:

@Article{dybjer00jsl,
  author =       {P. Dybjer},
  title =        {A general formulation of simultaneous inductive-recursive 
definitions in type theory},
  journal =      jsl,
  year =         2000,
  volume =       65,
  number =       2
}

Such definitions are not allowed in Coq.

A simple example is the type of lists with distinct elements (x#y):

dlist:(A:*)(#:A->A->*)*
fresh:(A:*)(#:A->A->*)A->(dlist A #)->*
nil:(A:*)(#:A->A->*)(dlist A #)
cons:(A:*)(#:A->A->*)(x:A)(l:dlist A #)(fresh A # x l)->(dlist A #)

where fresh is defined by the rules:

fresh A # x (nil A')            ->      True
fresh A # x (cons A' #' y l p)  ->      x#y /\ fresh A # x l

-- 
Frederic Blanqui.

------------------------------------------------------------------------
Laboratoire d'Informatique - Ecole Polytechnique - 91128 Palaiseau Cedex
tel: 01 69 33 46 14 - fax: 01 69 33 30 14 - http://www.lri.fr/~blanqui/