1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(* $Id: FMapInterface.v 11699 2008-12-18 11:49:08Z letouzey $ *)
11
(** * Finite map library *)
13
(** This file proposes interfaces for finite maps *)
15
Require Export Bool DecidableType OrderedType.
16
Set Implicit Arguments.
17
Unset Strict Implicit.
19
(** When compared with Ocaml Map, this signature has been split in
22
- The first parts [WSfun] and [WS] propose signatures for weak
23
maps, which are maps with no ordering on the key type nor the
24
data type. [WSfun] and [WS] are almost identical, apart from the
25
fact that [WSfun] is expressed in a functorial way whereas [WS]
26
is self-contained. For obtaining an instance of such signatures,
27
a decidable equality on keys in enough (see for example
28
[FMapWeakList]). These signatures contain the usual operators
29
(add, find, ...). The only function that asks for more is
30
[equal], whose first argument should be a comparison on data.
32
- Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the
33
case where the key type is ordered. The main novelty is that
34
[elements] is required to produce sorted lists.
36
- Finally, [Sord] extends [S] with a complete comparison function. For
37
that, the data type should have a decidable total ordering as well.
39
If unsure, what you're looking for is probably [S]: apart from [Sord],
40
all other signatures are subsets of [S].
42
Some additional differences with Ocaml:
44
- no [iter] function, useless since Coq is purely functional
45
- [option] types are used instead of [Not_found] exceptions
46
- more functions are provided: [elements] and [cardinal] and [map2]
51
Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
53
(** ** Weak signature for maps
55
No requirements for an ordering on keys nor elements, only decidability
56
of equality on keys. First, a functorial signature: *)
58
Module Type WSfun (E : DecidableType).
60
Definition key := E.t.
62
Parameter t : Type -> Type.
63
(** the abstract type of maps *)
69
Parameter empty : t elt.
72
Parameter is_empty : t elt -> bool.
73
(** Test whether a map is empty or not. *)
75
Parameter add : key -> elt -> t elt -> t elt.
76
(** [add x y m] returns a map containing the same bindings as [m],
77
plus a binding of [x] to [y]. If [x] was already bound in [m],
78
its previous binding disappears. *)
80
Parameter find : key -> t elt -> option elt.
81
(** [find x m] returns the current binding of [x] in [m],
82
or [None] if no such binding exists. *)
84
Parameter remove : key -> t elt -> t elt.
85
(** [remove x m] returns a map containing the same bindings as [m],
86
except for [x] which is unbound in the returned map. *)
88
Parameter mem : key -> t elt -> bool.
89
(** [mem x m] returns [true] if [m] contains a binding for [x],
90
and [false] otherwise. *)
92
Variable elt' elt'' : Type.
94
Parameter map : (elt -> elt') -> t elt -> t elt'.
95
(** [map f m] returns a map with same domain as [m], where the associated
96
value a of all bindings of [m] has been replaced by the result of the
97
application of [f] to [a]. Since Coq is purely functional, the order
98
in which the bindings are passed to [f] is irrelevant. *)
100
Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
101
(** Same as [map], but the function receives as arguments both the
102
key and the associated value for each binding of the map. *)
105
(option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''.
106
(** [map2 f m m'] creates a new map whose bindings belong to the ones
107
of either [m] or [m']. The presence and value for a key [k] is
108
determined by [f e e'] where [e] and [e'] are the (optional) bindings
109
of [k] in [m] and [m']. *)
111
Parameter elements : t elt -> list (key*elt).
112
(** [elements m] returns an assoc list corresponding to the bindings
113
of [m], in any order. *)
115
Parameter cardinal : t elt -> nat.
116
(** [cardinal m] returns the number of bindings in [m]. *)
118
Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
119
(** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
120
where [k1] ... [kN] are the keys of all bindings in [m]
121
(in any order), and [d1] ... [dN] are the associated data. *)
123
Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
124
(** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal,
125
that is, contain equal keys and associate them with equal data.
126
[cmp] is the equality predicate used to compare the data associated
131
Variable m m' m'' : t elt.
132
Variable x y z : key.
135
Parameter MapsTo : key -> elt -> t elt -> Prop.
137
Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.
139
Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.
141
Definition eq_key (p p':key*elt) := E.eq (fst p) (fst p').
143
Definition eq_key_elt (p p':key*elt) :=
144
E.eq (fst p) (fst p') /\ (snd p) = (snd p').
146
(** Specification of [MapsTo] *)
147
Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
149
(** Specification of [mem] *)
150
Parameter mem_1 : In x m -> mem x m = true.
151
Parameter mem_2 : mem x m = true -> In x m.
153
(** Specification of [empty] *)
154
Parameter empty_1 : Empty empty.
156
(** Specification of [is_empty] *)
157
Parameter is_empty_1 : Empty m -> is_empty m = true.
158
Parameter is_empty_2 : is_empty m = true -> Empty m.
160
(** Specification of [add] *)
161
Parameter add_1 : E.eq x y -> MapsTo y e (add x e m).
162
Parameter add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
163
Parameter add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
165
(** Specification of [remove] *)
166
Parameter remove_1 : E.eq x y -> ~ In y (remove x m).
167
Parameter remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
168
Parameter remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
170
(** Specification of [find] *)
171
Parameter find_1 : MapsTo x e m -> find x m = Some e.
172
Parameter find_2 : find x m = Some e -> MapsTo x e m.
174
(** Specification of [elements] *)
175
Parameter elements_1 :
176
MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
177
Parameter elements_2 :
178
InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
179
(** When compared with ordered maps, here comes the only
180
property that is really weaker: *)
181
Parameter elements_3w : NoDupA eq_key (elements m).
183
(** Specification of [cardinal] *)
184
Parameter cardinal_1 : cardinal m = length (elements m).
186
(** Specification of [fold] *)
188
forall (A : Type) (i : A) (f : key -> elt -> A -> A),
189
fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
191
(** Equality of maps *)
193
(** Caveat: there are at least three distinct equality predicates on maps.
194
- The simpliest (and maybe most natural) way is to consider keys up to
195
their equivalence [E.eq], but elements up to Leibniz equality, in
196
the spirit of [eq_key_elt] above. This leads to predicate [Equal].
197
- Unfortunately, this [Equal] predicate can't be used to describe
198
the [equal] function, since this function (for compatibility with
199
ocaml) expects a boolean comparison [cmp] that may identify more
200
elements than Leibniz. So logical specification of [equal] is done
201
via another predicate [Equivb]
202
- This predicate [Equivb] is quite ad-hoc with its boolean [cmp],
203
it can be generalized in a [Equiv] expecting a more general
204
(possibly non-decidable) equality predicate on elements *)
206
Definition Equal m m' := forall y, find y m = find y m'.
207
Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
208
(forall k, In k m <-> In k m') /\
209
(forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
210
Definition Equivb (cmp: elt->elt->bool) := Equiv (Cmp cmp).
212
(** Specification of [equal] *)
214
Variable cmp : elt -> elt -> bool.
216
Parameter equal_1 : Equivb cmp m m' -> equal cmp m m' = true.
217
Parameter equal_2 : equal cmp m m' = true -> Equivb cmp m m'.
222
(** Specification of [map] *)
223
Parameter map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
224
MapsTo x e m -> MapsTo x (f e) (map f m).
225
Parameter map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'),
226
In x (map f m) -> In x m.
228
(** Specification of [mapi] *)
229
Parameter mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
230
(f:key->elt->elt'), MapsTo x e m ->
231
exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
232
Parameter mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
233
(f:key->elt->elt'), In x (mapi f m) -> In x m.
235
(** Specification of [map2] *)
236
Parameter map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
237
(x:key)(f:option elt->option elt'->option elt''),
239
find x (map2 f m m') = f (find x m) (find x m').
241
Parameter map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
242
(x:key)(f:option elt->option elt'->option elt''),
243
In x (map2 f m m') -> In x m \/ In x m'.
245
Hint Immediate MapsTo_1 mem_2 is_empty_2
246
map_2 mapi_2 add_3 remove_3 find_2
248
Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
249
remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
255
(** ** Static signature for Weak Maps
257
Similar to [WSfun] but expressed in a self-contained way. *)
260
Declare Module E : DecidableType.
261
Include Type WSfun E.
266
(** ** Maps on ordered keys, functorial signature *)
268
Module Type Sfun (E : OrderedType).
269
Include Type WSfun E.
272
Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
273
(* Additional specification of [elements] *)
274
Parameter elements_3 : forall m, sort lt_key (elements m).
275
(** Remark: since [fold] is specified via [elements], this stronger
276
specification of [elements] has an indirect impact on [fold],
277
which can now be proved to receive elements in increasing order. *)
283
(** ** Maps on ordered keys, self-contained signature *)
286
Declare Module E : OrderedType.
292
(** ** Maps with ordering both on keys and datas *)
296
Declare Module Data : OrderedType.
297
Declare Module MapS : S.
300
Definition t := MapS.t Data.t.
302
Parameter eq : t -> t -> Prop.
303
Parameter lt : t -> t -> Prop.
305
Axiom eq_refl : forall m : t, eq m m.
306
Axiom eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
307
Axiom eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
308
Axiom lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
309
Axiom lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
311
Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end.
313
Parameter eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
314
Parameter eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
316
Parameter compare : forall m1 m2, Compare lt eq m1 m2.
317
(** Total ordering between maps. [Data.compare] is a total ordering
318
used to compare data associated with equal keys in the two maps. *)
added
removed
theories/FSets/FMapInterface.v
