The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Gerald Macinenti wrote:
> I am searching for a contribution where someone defined an associative
> array datatype
> with usual operations (add, remove, find ...)

        Well, I've done that a few years ago, but it's
a well-kept secret (never had time to write the docs...).
Look for the Rocq/GRAPHS contrib.  It contains a
library allmaps.v which does what you want.  Look at
file map.v for the main constructions : (Map A) is
a type of finite maps from the type ad of addresses
(essentially non-negative numbers in binary) to type A.
You'll find functions MapGet : (A:Set) (Map A) -> ad -> (option A)
[(MapGet A m x) returns (SOME A y) if m maps x to y or (NONE A)
if x is not in the domain], plus similar functions
MapPut (add binding, erasing previous binding for x if any),
MapPutBehind (add binding, doing nothing if x already bound),
MapRemove (remove x from domain of map),
MapMerge (merge two maps; second one wins in case of conflicts),
MapDomRestrTo (domain restriction),
MapDelta (symmetric difference),
and a few of their properties.
        fset.v contains an implementation of finite sets
as elements of type (Map unit).
        mapaxioms.v contains a few useful lemmata with proofs.
        mapiter.v provides iterators over maps.
        mapsubset.v provides a subset test for maps.
        mapcard.v provides MapCard and theorems on cardinalities.
        mapcanon.c shows defines canonical representatives for
maps, and shows that all operations in the library preserve
canonicity.
        You'll notice that elements in the domain of maps
(the index-set) are always of type ad.  There does not seem
to be a way of allowing for more general index-sets, except
by allocating ad's for each object of interest.
        All the best,

        -- Jean.