The Coq mailing list

[Marino Miculan <miculan AT dimi.uniud.it>]

On 08/mar/05, at 03:02, Robert Dockins wrote:

> I'm trying to define a type which has a uniqueness property.  I thought
> I'd define the type to be mutually inductive with a proposition type
> indicating the uniqueness:
> [...]
> However, coq rejects the definition, complaining,
>
> Error: The reference uniq_list was not found in the current 
> environment.

well, I've raise this problem (with exactly this example) something 
like nine years ago; see
http://coq.inria.fr/pipermail/coq-club/1996/000065.html
for an analysis of the problem.

> 1) Why does this happen?

The short answer is: the CIC/pCIC type theory does not allow to define 
types whose sorts contain the types under definition.
This avoids possible loopholes which could lead to the inconsistency of 
the system.

> 2) Is there a better way to do what I want? Is it possible?
> (I know I could just use ListSet, but I'm actually interested in a more
> complex structure).

As far as I know, there is no way for defining directly this kind of 
types.
Of course, you can use well-formedness predicates, two-level encodings, 
etc., but I suppose that this is not what you (and me) want.

-marino

--
  Marino Miculan - Department of Mathematics and Computing Science
University of Udine  - via delle Scienze 206, 33100 Udine - Italy
vox: +39-043255-8486 - fax: +39-043255-8499 - mob: +39-3292606452
mail:miculan at dimi uniud it  http://www.dimi.uniud.it/~miculan/