coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
- To: Edsko de Vries <devriese AT cs.tcd.ie>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] "Concrete" multiset?
- Date: Wed, 7 Nov 2007 11:08:37 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] "Concrete" multiset?, Edsko de Vries
- Re: [Coq-Club] "Concrete" multiset?,
frederic . blanqui
- Re: [Coq-Club] "Concrete" multiset?,
Edsko de Vries
- Re: [Coq-Club] "Concrete" multiset?,
Pierre Casteran
- Re: [Coq-Club] "Concrete" multiset?,
Edsko de Vries
- Re: [Coq-Club] "Concrete" multiset?,
frederic . blanqui
- Re: [Coq-Club] "Concrete" multiset?, Edsko de Vries
- Re: [Coq-Club] "Concrete" multiset?,
frederic . blanqui
- Re: [Coq-Club] "Concrete" multiset?,
Edsko de Vries
- Re: [Coq-Club] "Concrete" multiset?, frederic . blanqui
- Re: [Coq-Club] "Concrete" multiset?,
Pierre Casteran
- Re: [Coq-Club] "Concrete" multiset?,
Edsko de Vries
- Re: [Coq-Club] "Concrete" multiset?, Pierre Letouzey
- Message not available
- Re: [Coq-Club] "Concrete" multiset?, Pierre Letouzey
- Message not available
- Re: [Coq-Club] "Concrete" multiset?,
frederic . blanqui
Archive powered by MhonArc 2.6.16.