1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
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 ?
*)
|
