The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Sunday 11 October 2009 9:53:27 am André Hirschowitz wrote:
> I am not so happy with that example, let me propose a hopefully more
> enlightening one:
> 
> you want to define
> Z/2Z. So you would like to write for instance
> 
> Inductive Ztwo : Type :=
> O :Ztwo
> 
> | S : Ztoo ->Ztwo
> 
> WITH  forall n :Ztwo ,  SSn =n.
> 
> This corresponding  Ztwo_rect (or fixpoint) should generate a proof
> obligation for checking that the recursive formulas are compatible with
> the relations specified under the WITH banner.

This sounds to me like quotient types. Coq is an intensional type theory, 
which means its built-in equality is limited to distinguishing constructors, 
more or less. So, to work with quotients, people use setoids, which is a set 
and an equivalence relation that's supposed to represent equality on the set 
in question.

However, there are extensional theories where you can take a setoid 
(something) like that and tell the language to make a new type where the 
elements are the equivalence classes of such a setoid. It may not be that 
simple, but that's the gist. I don't really have experience with such 
languages, but NuPRL is one, for instance.

I wouldn't get your hopes up on quotient types being added to Coq, though. 
You 
might want to read about them anyway, though, and googling "quotient types" 
seems to generate a lot of hits.

Cheers.

-- Dan