The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 9 Nov 2011, Carlos Simpson wrote:

> Dear Russell,
>  Thanks, that's illuminating. I guess the question which can make us
> uneasy about using setoids, is whether it causes too much extra effort to
> prove that all functions are compatible all the time? That kind of fear does
> sometimes prove to be overblown.

The amount of work needed to prove that functions are respectful is 
exactly the amount of work needed to show that a function is well-defined 
using quotients (ie the work needed to satisfy the hypothesis of 
ZornsLemma.Quotients.induced_fuction).  Then some sort of type-class 
mechanism needs to take over to prove that compositions of respectful 
functions are respectful.

> One imagines that all of the CIC operations we can do on types, need to 
> be done by hand for setoids. Is it the case that you actually end up 
> having only a small number of these to do in practice? ---Carlos

There is something to this point.  You need need to write a library to make 
products of setoid, and disjoint unions of setoids, and setoid function 
spaces (*).  However, I never really had a problem with this because we 
have to do this sort of thing all the time anyways.  So, for example, when 
doing my work on metric spaces I needed to define a metric for the product 
of two metric spaces, and a metric for functions between metric spaces, 
etc.  Since I had to all this work anyways, I didn't find it particularly 
burdensome to define these operations on setoids while I was at it.

(*) Actually I did discover some annoyance with setoids and function 
spaces.  You need to put a setoid structure on a sigma-type of functions 
that are respectful.  What I discovered was that everything would probably 
be better if PERs were used instead of setoids.  The PER of functions 
between Setoids is exactly what you expect:

f ~~ g := forall x y, x == y -> f x == g y

And we immediately get that a function f is respectful when f ~~ f.  And 
this definition extends to the PER of functions between PERs

f ~~ g := forall x y, x ~~ y -> f x ~~ g y

I spent a while slogging through this PER stuff and every obstacle I 
encountered eventually yielded to an elegant solution.  I suspect that the 
experts on PERs already knew all this stuff I was discovering. 
Unfortunately at the time (several years ago) I couldn't quite get the 
support out of Mathieu's type class mechanism that I needed to make this 
seamless.  I suspect it would be easier today or one could use Canonical 
Structures instead. I would encourage the development and use of PERs 
instead of setoids.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''