The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Mon, Mar 07, 2005 at 09:02:59PM -0500, 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.

What you are trying to do (as you said yourself) is defining a type
and a predicate on this type mutually inductive; this is called
induction-recursion, and is not supported by the CIC (calculus of
inductive constructions), the type theory behind Coq. AFAIK, the
canonical reference for the notion is:

 Peter Dybjer, A general formulation of simultaneous
 inductive-recursive definitions in type theory, Journal of Symbolic
 Logic, 65(2), June 2000.

Notice the relatively recent date :-) But maybe someone will correct
me and say that the notion was known for longer.

In Coq, you define list, then define notin, then define (e.g.) a
record type holding a list and the uniqueness property; the concept of
"Partial Setoid" may help there. Alternatively, you can have the
uniqueness property as hypothesis in every theorem / lemma :-)

As for induction-recursion, I know of Agda and Lego that support it;
none of these is currently to the stage of practically useful as a
proof assistant, though.

-- 
Lionel