The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Wed, Nov 07, 2007 at 09:21:28AM +0000, Edsko de Vries wrote:
> Hi,
> 
> Is there an implementation of multisets in Coq which has the property
> that for two multisets M1 and M2, union M1 M2 = union M2 M1 (as in the
> Multiset implementation in the standard library), but is "concrete" in
> the sense that it supports an operation elems :: Multiset A -> List A?
> 
> Thanks,
> 
> Edsko
> 

Hi 

You can have a look at my small experiment of MultiSet based on Finite
Maps: 

https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/*checkout*/trunk/Orsay/FSets/MultiSets.v?rev=634&root=coq-contribs

In order to be efficient, a decidable order is asked on the elements. 
If you wish, this could be relaxed to just a decidable equality (in the
same spirit as FSetWeak / FMapWeak of Coq stdlib).

There is indeed an "elements" functions (that produce a List
(A*positive), the positive part being the multiplicity).  At the same
time, you don't have union M1 M2 = union M2 M1, but only union M1 M2
[=] union M2 M1, with [=] being an equivalence relation based on
point-to-point comparison. The idea is that underlying maps may
perfectly be coded with data representations that don't have canonical
representatives (think of (almost) well-balanced tree for
instance). At the same time, if you choose underlying maps such as
FMapList (sorted lists), it should be possible to prove that = and [=]
are the same  (at least when elements are compared according to 
Coq = and not according to some setoid equality). 

Best regards, 

Pierre Letouzey