diff options
Diffstat (limited to 'theories/MMaps/MMapInterface.v')
| -rw-r--r-- | theories/MMaps/MMapInterface.v | 292 |
1 files changed, 292 insertions, 0 deletions
diff --git a/theories/MMaps/MMapInterface.v b/theories/MMaps/MMapInterface.v new file mode 100644 index 00000000..05c5e5d8 --- /dev/null +++ b/theories/MMaps/MMapInterface.v @@ -0,0 +1,292 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** * Finite map library *) + +(** This file proposes interfaces for finite maps *) + +Require Export Bool Equalities Orders SetoidList. +Set Implicit Arguments. +Unset Strict Implicit. + +(** 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 + [bindings] 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 + +*) + + +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. + Hint Transparent key. + + Definition eq_key {elt} (p p':key*elt) := E.eq (fst p) (fst p'). + + Definition eq_key_elt {elt} (p p':key*elt) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Parameter t : Type -> Type. + (** the abstract type of maps *) + + Section Ops. + + Parameter empty : forall {elt}, t elt. + (** The empty map. *) + + Variable elt:Type. + + 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. *) + + Parameter bindings : t elt -> list (key*elt). + (** [bindings 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. *) + + 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 merge : (key -> option elt -> option elt' -> option elt'') -> + t elt -> t elt' -> t elt''. + (** [merge 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 k e e'] where [e] and [e'] are the (optional) + bindings of [k] in [m] and [m']. *) + + End Ops. + Section Specs. + + Variable elt:Type. + + Parameter MapsTo : key -> elt -> t elt -> Prop. + + Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m. + + Global Declare Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + + Variable m m' : t elt. + Variable x y : key. + Variable e : elt. + + Parameter find_spec : find x m = Some e <-> MapsTo x e m. + Parameter mem_spec : mem x m = true <-> In x m. + Parameter empty_spec : find x (@empty elt) = None. + Parameter is_empty_spec : is_empty m = true <-> forall x, find x m = None. + Parameter add_spec1 : find x (add x e m) = Some e. + Parameter add_spec2 : ~E.eq x y -> find y (add x e m) = find y m. + Parameter remove_spec1 : find x (remove x m) = None. + Parameter remove_spec2 : ~E.eq x y -> find y (remove x m) = find y m. + + (** Specification of [bindings] *) + Parameter bindings_spec1 : + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + (** When compared with ordered maps, here comes the only + property that is really weaker: *) + Parameter bindings_spec2w : NoDupA eq_key (bindings m). + + (** Specification of [cardinal] *) + Parameter cardinal_spec : cardinal m = length (bindings m). + + (** Specification of [fold] *) + Parameter fold_spec : + forall {A} (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + + (** 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 *) + + Definition Equal (m m':t elt) := forall y, find y m = find y m'. + Definition Equiv (eq_elt:elt->elt->Prop) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). + Definition Equivb (cmp: elt->elt->bool) := Equiv (Cmp cmp). + + (** Specification of [equal] *) + Parameter equal_spec : forall cmp : elt -> elt -> bool, + equal cmp m m' = true <-> Equivb cmp m m'. + + End Specs. + Section SpecMaps. + + Variables elt elt' elt'' : Type. + + Parameter map_spec : forall (f:elt->elt') m x, + find x (map f m) = option_map f (find x m). + + Parameter mapi_spec : forall (f:key->elt->elt') m x, + exists y:key, E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + + Parameter merge_spec1 : + forall (f:key->option elt->option elt'->option elt'') m m' x, + In x m \/ In x m' -> + exists y:key, E.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). + + Parameter merge_spec2 : + forall (f:key -> option elt->option elt'->option elt'') m m' x, + In x (merge f m m') -> In x m \/ In x m'. + + End SpecMaps. +End WSfun. + +(** ** Static signature for Weak Maps + + Similar to [WSfun] but expressed in a self-contained way. *) + +Module Type WS. + Declare Module E : DecidableType. + Include WSfun E. +End WS. + + + +(** ** Maps on ordered keys, functorial signature *) + +Module Type Sfun (E : OrderedType). + Include WSfun E. + + Definition lt_key {elt} (p p':key*elt) := E.lt (fst p) (fst p'). + + (** Additional specification of [bindings] *) + + Parameter bindings_spec2 : forall {elt}(m : t elt), sort lt_key (bindings m). + + (** Remark: since [fold] is specified via [bindings], this stronger + specification of [bindings] has an indirect impact on [fold], + which can now be proved to receive bindings in increasing order. *) + +End Sfun. + + +(** ** Maps on ordered keys, self-contained signature *) + +Module Type S. + Declare Module E : OrderedType. + Include Sfun E. +End S. + + + +(** ** Maps with ordering both on keys and datas *) + +Module Type Sord. + + Declare Module Data : OrderedType. + Declare Module MapS : S. + Import MapS. + + Definition t := MapS.t Data.t. + + Include HasEq <+ HasLt <+ IsEq <+ IsStrOrder. + + Definition cmp e e' := + match Data.compare e e' with Eq => true | _ => false end. + + Parameter eq_spec : forall m m', eq m m' <-> Equivb cmp m m'. + + Parameter compare : t -> t -> comparison. + + Parameter compare_spec : forall m1 m2, CompSpec eq lt m1 m2 (compare m1 m2). + +End Sord. + + +(* TODO: provides filter + partition *) + +(* TODO: provide split + Parameter split : key -> t elt -> t elt * option elt * t elt. + + Parameter split_spec k m : + split k m = (filter (fun x -> E.compare x k) m, find k m, filter ...) + + min_binding, max_binding, choose ? +*) |