The Coq mailing list

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

Indeed, proofs of sorting are not identical for identical lists. They
depend on the way you built the list : consider for instance the set S
= {x, y} where x < y. If you build it by merging {x} and {y}, the
proof of sortedness will be something like "union_sort _ _ (proof that
{x} is sorted) (proof that {y} is sorted)" where union_sort is a lemma
stating that merging two sorted lists yiels a sorted list.
If, on the contrary, you build S by adding x to {y}, the proof of
well-sortedness will be something like "add_sort _ _ (proof that {y}
is sorted)", and there is no relation a priori between add_sort and
union_sort.

S.L.

2009/3/18 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
>>>
>>>
>>
>>
>>
>>
>
>



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