The Coq mailing list

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

On Wed, Nov 07, 2007 at 11:56:23AM +0000, Edsko de Vries wrote:
> > 
> > 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).
> 
> When I try to compile your library, I get an error on
> 
>   Definition Subset s s' := forall a : elt, multi a s <= multi a s'. 
>  
> Error: In environment
> s : t
> s' : ?22
> a : elt
> The term "multi a s" has type "N" while it is expected to have type "nat"
> 
> which I'm not entirely sure how to get rid of. 
> 

My fault. I forgot to mention that this MultiSets.v only compiles on a
fairly recent svn version of Coq, since it needs some functions and
results about the N datatype that I've added to the theories precisely
during the making of this MultiSets. If you're reluctant to fetch and
compile a development version of Coq, you can probably adapt this
MultiSets.v by replacing any N-related stuff by the corresponding nat
stuff.

> > 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). 
> 
> That sounds great, do you think that would be difficult?
> 

No it's not very hard, i've even tried and done it. See files: 

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

I'm afraid these files also rely on stuff not present in Coq 8.1plX 
(more precisely, recent additions to FSets / FMaps). 


Two more remarks: 

 * Working with setoids and morphisms is often less cumbersome that
   you may think first. For instance, FSets / FMap are usually quite
   usable even if you haven't Leibniz equality between sets and maps
   by default. The experimental MultiSets I've mentionned about could
   be extended in the same way, with the right Add Relation(s) and Add
   Setoid(s) in order to allow the use of "rewrite" in the most common
   situations.  But of course, your mileage may vary, depending on
   your needs about these Multisets.

 * concerning merge sort, there is one hidden in Coq's stdlib, as well 
   as many other functions about sorted lists: see file FSetList.v, 
   and more precisely function "union" in functor Raw.

Best regards, 
Pierre L.