The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Sorry for the little explanation I wrote in my former message.
>>But for "canonical" sets/maps (that is which admits only one 
>>representation, that is
>>extensional equality is exactly syntactical equality), yes that can work.
I was referring to those "canonical ones"
>> Note however, that FMap/FSet already provide stuff to establish a
>>link between extensionnal equality and a boolean equality on maps.
And that is exactly where I was "attaccking" when I said
> May be the "right" representation of a finite collection is not the
> collection of the term but the collection of their serialization?

Trying to be more explicit this time:
If it was easy to define serialization and deserialization functions
for any finite datatype,
then a similar FMap/FSet implementation can be working on the
serialized version,
requiring no extra instrumentation of the datatipe itself.
That is, today using the polymorphic list type and proving properties
over such lists is order of magnitude easier than doing the same over
finite sets (with canonical representation)
If it was possible to see every datatype as his syntactical
representation, (that of course defines a total ordering) a simple
ordered list without repetition *is* a set with canonical
representation.