The Coq mailing list

[frederic.blanqui AT loria.fr]

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). alternatively, you could modify adam 
koprowski's multiset module in color by taking a total ordering as argument, 
defining union as the merging of the two (sorted) list arguments (giving a 
sorted list again), and defining meq by eq. this is interesting if you later 
need to use the multiset extension of some element ordering since color 
provides it. please, let us know if you write a new implementation of 
multisets. thanks.