The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

You are correct that I've been assuming FSetLists as my structure.  I 
had not considered the AVL structure, for which this wouldn't hold. 

I do not understand where proof-irrelevance would enter for FSetLists.  
I had thought that with identical representations, the proofs of sorting 
would also be identical.  What did I miss here?

Scott Doerrie

Stéphane Lescuyer wrote:
> 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
> >
> >     
>
>
>
>