Library Coq.FSets.FMapInterface
Finite map library
This file proposes interfaces for finite maps
When compared with Ocaml Map, this signature has been split in
several parts :
- The first parts WSfun and WS propose signatures for weak
maps, which are maps with no ordering on the key type nor the
data type. WSfun and WS are almost identical, apart from the
fact that WSfun is expressed in a functorial way whereas WS
is self-contained. For obtaining an instance of such signatures,
a decidable equality on keys in enough (see for example
FMapWeakList). These signatures contain the usual operators
(add, find, ...). The only function that asks for more is
equal, whose first argument should be a comparison on data.
- Then comes Sfun and S, that extend WSfun and WS to the
case where the key type is ordered. The main novelty is that
elements is required to produce sorted lists.
- Finally, Sord extends S with a complete comparison function. For
that, the data type should have a decidable total ordering as well.
If unsure, what you're looking for is probably
S: apart from
Sord,
all other signatures are subsets of
S.
Some additional differences with Ocaml:
- no iter function, useless since Coq is purely functional
- option types are used instead of Not_found exceptions
- more functions are provided: elements and cardinal and map2
Weak signature for maps
No requirements for an ordering on keys nor elements, only decidability
of equality on keys. First, a functorial signature:
the abstract type of maps
The empty map.
Test whether a map is empty or not.
add x y m returns a map containing the same bindings as m,
plus a binding of x to y. If x was already bound in m,
its previous binding disappears.
find x m returns the current binding of x in m,
or None if no such binding exists.
remove x m returns a map containing the same bindings as m,
except for x which is unbound in the returned map.
mem x m returns true if m contains a binding for x,
and false otherwise.
map f m returns a map with same domain as m, where the associated
value a of all bindings of m has been replaced by the result of the
application of f to a. Since Coq is purely functional, the order
in which the bindings are passed to f is irrelevant.
Same as map, but the function receives as arguments both the
key and the associated value for each binding of the map.
map2 f m m´ creates a new map whose bindings belong to the ones
of either m or m´. The presence and value for a key k is
determined by f e e´ where e and e´ are the (optional) bindings
of k in m and m´.
elements m returns an assoc list corresponding to the bindings
of m, in any order.
cardinal m returns the number of bindings in m.
fold f m a computes (f kN dN ... (f k1 d1 a)...),
where k1 ... kN are the keys of all bindings in m
(in any order), and d1 ... dN are the associated data.
equal cmp m1 m2 tests whether the maps m1 and m2 are equal,
that is, contain equal keys and associate them with equal data.
cmp is the equality predicate used to compare the data associated
with the keys.
Specification of MapsTo
Specification of mem
Specification of empty
Specification of is_empty
Specification of add
Specification of remove
Specification of find
Specification of elements
When compared with ordered maps, here comes the only
property that is really weaker:
Specification of cardinal
Specification of fold
Equality of maps
Caveat: there are at least three distinct equality predicates on maps.
- The simpliest (and maybe most natural) way is to consider keys up to
their equivalence E.eq, but elements up to Leibniz equality, in
the spirit of eq_key_elt above. This leads to predicate Equal.
- Unfortunately, this Equal predicate can't be used to describe
the equal function, since this function (for compatibility with
ocaml) expects a boolean comparison cmp that may identify more
elements than Leibniz. So logical specification of equal is done
via another predicate Equivb
- This predicate Equivb is quite ad-hoc with its boolean cmp,
it can be generalized in a Equiv expecting a more general
(possibly non-decidable) equality predicate on elements
Specification of equal
Specification of map
Specification of mapi
Specification of map2
Static signature for Weak Maps
Similar to
WSfun but expressed in a self-contained way.
Maps on ordered keys, functorial signature
Remark: since fold is specified via elements, this stronger
specification of elements has an indirect impact on fold,
which can now be proved to receive elements in increasing order.
Maps on ordered keys, self-contained signature
Maps with ordering both on keys and datas
Total ordering between maps. Data.compare is a total ordering
used to compare data associated with equal keys in the two maps.