The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 2 févr. 2011 à 01:09, Aaron Bohannon a écrit :

> Hi,

Hi,

> I just saw this topic, which is something that has also been of
> interest to me.  I am doing a large development with many datatypes,
> some of whose constructors take FSets/FMaps as arguments.  I wanted to
> be able to ensure that I could use the "setoid_rewrite" and such
> tactics, as defined in the "SetoidTactics" module, to rewrite FMaps in
> my datatypes, and that the Setoid equality on my FMaps would be
> automatically derived in the natural way from the Setoid equality on
> the range type of the FMaps.
> 
> I was not really sure whether I could get type-classes and modules
> working together in this way.  Also, all of the Setoid-related code
> seems to be lacking documentation and examples and is therefore very
> confusing.  So it took me quite some time to figure out, but I did
> seem to get it all working.  I also wrote generic code for lifting
> Setoid equivalences over the basic type constructors (sum, prod,
> option, list, etc).  It does seem like all of this should be code that
> belongs in the standard library.
> 
> Unfortunately, I do not have time to polish up my code for mass
> consumption right now (my name choices may not be ideal; my code may
> not be as complete as it shoud be; my code loosely depends on some
> custom tactics; etc).  But if someone is very interested in it, I
> would be willing to send what I have privately...especially if they
> are willing to help me refine and polish it!

  I'd be interested in doing that. Indeed the stdlib lacks many standard 
instances and does not really develop one particular approach to formalize
setoids (for lack of a "best"/generally useful design).

> P.S. One hidden gotcha that has nothing to do with FSets/FMaps is
> that, in order to get setoid rewriting working in the way you expect,
> you have to do this:
> 
> Instance Setoid_DefaultRelation {A: Type} {S: Setoid A}: DefaultRelation 
> equiv.
> 
> I am not sure why the DefaultRelation class exists at all or why this
> instance declaration does appear in the standard library.  After all,
> to declare a type as an instance of Setoid literally means to
> associate it with a default equivalence relation.  Why would I want
> another level of indirection?  As I said, the Setoid code in the
> standard library is confusing.

This class is used to decide which relation to use when using "setoid_replace"
without explicitely giving it. There might be multiple relations to choose
from (there's always eq for example) so this instance declaration allows
to say that if a setoid has been declared on [A] it should be used by default.
This is explained in the reference manual: 
http://coq.inria.fr/refman/Reference-Manual031.html#toc171

-- Matthieu