The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi, even with an UsualOrderedType, extensionality is not true in
general for FSets since it depends on the actual representation : two
different AVLs can represent the same set for instance. Even with
sorted lists, where you might expect the property to be true, it would
require the proof-irrelevance of the proof that the list is sorted.

S.L.

On Wed, Mar 18, 2009 at 7:20 PM, M. Scott Doerrie 
<mdoerri AT cs.jhu.edu>
 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06