The Coq mailing list

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