Library Stdlib.FSets.FMapInterface


Finite map library

This file proposes interfaces for finite maps

From Stdlib Require Export Bool DecidableType OrderedType.
Set Implicit Arguments.

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

Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.

Weak signature for maps

No requirements for an ordering on keys nor elements, only decidability of equality on keys. First, a functorial signature:

Module Type WSfun (E : DecidableType).

  Definition key := E.t.
  #[global]
  Hint Transparent key : core.

  Parameter t : Type -> Type.
the abstract type of maps

  Section Types.

    Variable elt:Type.

    Parameter empty : t elt.
The empty map.

    Parameter is_empty : t elt -> bool.
Test whether a map is empty or not.

    Parameter add : key -> elt -> t elt -> t elt.
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.

    Parameter find : key -> t elt -> option elt.
find x m returns the current binding of x in m, or None if no such binding exists.

    Parameter remove : key -> t elt -> t elt.
remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.

    Parameter mem : key -> t elt -> bool.
mem x m returns true if m contains a binding for x, and false otherwise.

    Variable elt' elt'' : Type.

    Parameter map : (elt -> elt') -> t elt -> t elt'.
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.

    Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
Same as map, but the function receives as arguments both the key and the associated value for each binding of the map.

    Parameter map2 :
     (option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''.
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'.

    Parameter elements : t elt -> list (key*elt).
elements m returns an assoc list corresponding to the bindings of m, in any order.

    Parameter cardinal : t elt -> nat.
cardinal m returns the number of bindings in m.

    Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
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.

    Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
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.

    Section Spec.

      Variable m m' m'' : t elt.
      Variable x y z : key.
      Variable e e' : elt.

      Parameter MapsTo : key -> elt -> t elt -> Prop.

      Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.

      Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.

      Definition eq_key (p p':key*elt) := E.eq (fst p) (fst p').

      Definition eq_key_elt (p p':key*elt) :=
          E.eq (fst p) (fst p') /\ (snd p) = (snd p').

Specification of MapsTo
      Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.

Specification of mem
      Parameter