The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  If you have a concrete data type, as you must if you have decidable 
equality, then your order predicate should also be decidable, in which case 
list monotonicity is also decidable, and thus can be stated as an equality on 
bool. Proof irrelevance DOES hold for equalities on bool.
  Of course, in that case your type is also effectively countable, so it is 
also possible to bypass order and sorting altogether, and represent a set by 
the non-trivial initial segment of the graph of its characteristic function 
(e.g., {x1, x3} is represented by the Some [true; false; true]); this factors 
better with functions with finite support.

Georges Gonthier

-----Original Message-----
From: 
coq-club-admin AT pauillac.inria.fr
 
[mailto:coq-club-admin AT pauillac.inria.fr]
 On Behalf Of M. Scott Doerrie
Sent: 18 March 2009 19:05
To: Stéphane Lescuyer
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] FSet Extensionality Not defined

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
>>
>>
>
>
>
>

--------------------------------------------------------
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