The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Wed, Nov 07, 2007 at 01:44:26PM +0100, 
frederic.blanqui AT loria.fr
 wrote:
> On Wed, 7 Nov 2007, Edsko de Vries wrote:
> 
> >But that means that I have to prove something for every property P I
> >need to prove stuff about (that P is a "morphism", whatever I that is)
> >-- which I don't want to have to do :) I am looking for an
> >implementation of multisets which has the property that (union M1 M2)
> >really *equals* union M2 M1, so that I can prove this property without
> >any further hypotheses about P (this would be possible if the multiset
> >uses some sort of ordering on the elements, for example).
> 
> proving that P is a morphism may not be so difficult (various morphisms are 
> already proved in color). but i understand your point. then, as said by 
> pierre letouzay, you could re-use pierre's multiset module with maps 
> implemented by sorted lists and try to prove that [=] is = (i think that 
> you need a total ordering on your elements to prove that). 

That would be a good solution, but I'm having trouble getting that
library to work (it is using subtraction on N, for example, which
doesn't seem to be defined in the libraries -- at least, not in 8.1pl1).

But apart from that, is there a lemma that tells me that union L1 L2 =
union L2 L1, for two sorted lists (FSetList) L1 and L2 (with "=" the
"real" Coq equality)? It does not seem to be defined in FSetList -- but
it should be provable, no?

Edsko