The Coq mailing list

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

Understood.  Thank you.

The high-level implications of this are that I can not use define 
relations (ala Relations_N modules) over FSetLists to form a partial 
order and reuse those theorems to build up my proof.   I can not define 
a complete definition of Antisymmetry.

Scott Doerrie

Stéphane Lescuyer wrote:
> Well, it's not a theoretical limit, just the way it's done in the
> library. As Georges explained, sortedness is decidable as soon as
> comparison is, but the proofs are not done along those lines in FSet,
> and the lemmas add_sort/union_sort/remove_sort/.... are opaque so even
> if they were creating the exact same object under the hood (which they
> arent), the results still wouldn't be equal because Coq couldnt' check
> that they are convertible to one another.
>
> 2009/3/18 M. Scott Doerrie 
> <mdoerri AT cs.jhu.edu>:
>   
> > I suppose I have assumed that since everything is complete, decidable,
> > deterministic, and finite, that the result of union_sort and add_sort would
> > be identical structures when union and add produced identical structures.
> >  Why can I talk about having identical resulting structures over union and
> > add and not union_sort and add_sort?
> >
> > Scott Doerrie
> >
> > Stéphane Lescuyer wrote:
> >     
> > > 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
> > > > > >
> > > > > >
> > > > > >
> > > > > >             
> > > > >
> > > > >           
> > > >         
> > >
> > >
> > >       
> >     
>
>
>
>