The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Wed, Mar 18, 2009 at 02:20:36PM -0400, M. Scott Doerrie wrote:
> I would really like to have an axiom-free method of constructing 
> Ensembles from FSets.  However, I can't find any definition for 
> Extensionality_Ensembles in FSetToFiniteSet in any version of the Coq 
> standard library.  I believe this axiom would be derivable if creating 
> FSets from UsualOrderedTypes, yet I can not locate it.  Did I miss 
> something?  Is this not possible?
> 
> Scott Doerrie
> 

No, having Leibniz equality on the elements is not enough to have the
extensionnality of finite sets in all generality. For instance, take a
tree-based implementation (typically AVL): there are many ways to
balance a tree while keeping the same elements in it.

It remains me an old question on this topic, but I can't find back the
precise thread on coq-club. Anyway, to illustre my answer at that
time, I wrote a small file FSetListEq.v, still accessible via:

svn://scm.gforge.inria.fr/svn/coq-contribs/trunk/Orsay/FSets/FSetListEq.v

As said in a comment at the start of the file:

(* For the equality on sets to be the one of Coq, we need:
    - an order on elements, and not just a decidable equality
       (hence an OrdereredType leading to some FSets instead of
        a DecidableType leading to some FSetWeak).
    - the equality on elements must be the one of Coq
       (hence a UsualOrderedType instead of just a OrderedType)
    - an implementation of sets with canonical representation,
       for instance FSetList based on sorted lists.
    - the proof irrelevance axiom, since an implementation such
       as FSetList isn't really canonical: a set comes with
       a well-sortedness certificate.
*)

Best,

Pierre