gmultiset.v 14.2 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import gmap.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6

Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
7
8
Arguments GMultiSet {_ _ _} _ : assert.
Arguments gmultiset_car {_ _ _} _ : assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10
Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
Proof. solve_decision. Defined.

13
Program Instance gmultiset_countable `{Countable A} :
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17
18
19
20
21
22
23
    Countable (gmultiset A) := {|
  encode X := encode (gmultiset_car X);  decode p := GMultiSet <$> decode p
|}.
Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.

Section definitions.
  Context `{Countable A}.

  Definition multiplicity (x : A) (X : gmultiset A) : nat :=
    match gmultiset_car X !! x with Some n => S n | None => 0 end.
24
  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    0 < multiplicity x X.
26
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y,  x,
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
    multiplicity x X  multiplicity x Y.

29
  Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
30
    let (X) := X in ''(x,n)  map_to_list X; replicate (S n) x.
31
  Global Instance gmultiset_size : Size (gmultiset A) := length  elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

33
34
  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    GMultiSet {[ x := 0 ]}.
36
  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (S (x + y))) X Y.
39
  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
    let (X) := X in let (Y) := Y in
    GMultiSet $ difference_with (λ x y,
      let z := x - y in guard (0 < z); Some (pred z)) X Y.
43

44
  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
45
    let (X) := X in dom _ X.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
End definitions.

48
49
50
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
51
Typeclasses Opaque gmultiset_dom.
52

Robbert Krebbers's avatar
Robbert Krebbers committed
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
Section lemmas.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.

Lemma gmultiset_eq X Y : X = Y   x, multiplicity x X = multiplicity x Y.
Proof.
  split; [by intros ->|intros HXY].
  destruct X as [X], Y as [Y]; f_equal; apply map_eq; intros x.
  specialize (HXY x); unfold multiplicity in *; simpl in *.
  repeat case_match; naive_solver.
Qed.

(* Multiplicity *)
Lemma multiplicity_empty x : multiplicity x  = 0.
Proof. done. Qed.
Lemma multiplicity_singleton x : multiplicity x {[ x ]} = 1.
Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed.
Lemma multiplicity_singleton_ne x y : x  y  multiplicity x {[ y ]} = 0.
Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
Lemma multiplicity_union X Y x :
  multiplicity x (X  Y) = multiplicity x X + multiplicity x Y.
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; omega.
Qed.
Lemma multiplicity_difference X Y x :
  multiplicity x (X  Y) = multiplicity x X - multiplicity x Y.
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
  rewrite lookup_difference_with.
  destruct (X !! _), (Y !! _); simplify_option_eq; omega.
Qed.

87
(* Collection *)
88
89
90
91
92
93
94
95
96
97
98
99
100
Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
Proof. done. Qed.

Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
Proof.
  split.
  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. omega.
  - intros x y. destruct (decide (x = y)) as [->|].
    + rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia.
    + rewrite elem_of_multiplicity, multiplicity_singleton_ne by done.
      by split; auto with lia.
  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega.
Qed.
101
102
Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
103

104
(* Algebraic laws *)
105
Global Instance gmultiset_comm : Comm (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
Proof.
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega.
Qed.
109
Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
Proof.
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega.
Qed.
113
Global Instance gmultiset_left_id : LeftId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
117
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_union, multiplicity_empty.
Qed.
118
Global Instance gmultiset_right_id : RightId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
121
122
123
124
125
126
127
128
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.

Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ).
Proof.
  intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
  rewrite !multiplicity_union. omega.
Qed.
Global Instance gmultiset_union_inj_2 X : Inj (=) (=) ( X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.

129
Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
132
  rewrite gmultiset_eq. intros Hx; generalize (Hx x).
  by rewrite multiplicity_singleton, multiplicity_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
142
(* Properties of the elements operation *)
Lemma gmultiset_elements_empty : elements ( : gmultiset A) = [].
Proof.
  unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty.
Qed.
Lemma gmultiset_elements_empty_inv X : elements X = []  X = .
Proof.
  destruct X as [X]; unfold elements, gmultiset_elements; simpl.
143
144
145
  intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?.
  - by apply map_to_list_empty_inv.
  - naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
Qed.
Lemma gmultiset_elements_empty' X : elements X = []  X = .
Proof.
  split; intros HX; [by apply gmultiset_elements_empty_inv|].
  by rewrite HX, gmultiset_elements_empty.
Qed.
Lemma gmultiset_elements_singleton x : elements ({[ x ]} : gmultiset A) = [ x ].
Proof.
  unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
Qed.
Lemma gmultiset_elements_union X Y :
  elements (X  Y)  elements X ++ elements Y.
Proof.
  destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements.
  set (f xn := let '(x, n) := xn in replicate (S n) x); simpl.
  revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
162
  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
166
167
168
  destruct (Y !! x) as [n'|] eqn:HY.
  - rewrite <-(insert_id Y x n'), <-(insert_delete Y) by done.
    erewrite <-insert_union_with by done.
    rewrite !map_to_list_insert, !bind_cons
      by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
    rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
169
170
    rewrite (assoc_L _). f_equiv.
    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
  - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
      by (by rewrite ?lookup_union_with, ?HX, ?HY).
    by rewrite <-(assoc_L (++)), <-IH.
Qed.
Lemma gmultiset_elem_of_elements x X : x  elements X  x  X.
Proof.
  destruct X as [X]. unfold elements, gmultiset_elements.
  set (f xn := let '(x, n) := xn in replicate (S n) x); simpl.
  unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
  rewrite elem_of_list_bind. split.
  - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
  - intros. destruct (X !! x) as [n|] eqn:Hx; [|omega].
    exists (x,n); split; [|by apply elem_of_map_to_list].
    apply elem_of_replicate; auto with omega.
Qed.
186
187
188
189
190
191
Lemma gmultiset_elem_of_dom x X : x  dom (gset A) X  x  X.
Proof.
  unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
  destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
  destruct (X !! x); naive_solver omega.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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

(* Properties of the size operation *)
Lemma gmultiset_size_empty : size ( : gmultiset A) = 0.
Proof. done. Qed.
Lemma gmultiset_size_empty_inv X : size X = 0  X = .
Proof.
  unfold size, gmultiset_size; simpl. rewrite length_zero_iff_nil.
  apply gmultiset_elements_empty_inv.
Qed.
Lemma gmultiset_size_empty_iff X : size X = 0  X = .
Proof.
  split; [apply gmultiset_size_empty_inv|].
  by intros ->; rewrite gmultiset_size_empty.
Qed.
Lemma gmultiset_size_non_empty_iff X : size X  0  X  .
Proof. by rewrite gmultiset_size_empty_iff. Qed.

Lemma gmultiset_choose_or_empty X : ( x, x  X)  X = .
Proof.
  destruct (elements X) as [|x l] eqn:HX; [right|left].
  - by apply gmultiset_elements_empty_inv.
  - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left.
Qed.
Lemma gmultiset_choose X : X     x, x  X.
Proof. intros. by destruct (gmultiset_choose_or_empty X). Qed.
Lemma gmultiset_size_pos_elem_of X : 0 < size X   x, x  X.
Proof.
  intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, gmultiset_size_empty; lia.
Qed.

Lemma gmultiset_size_singleton x : size ({[ x ]} : gmultiset A) = 1.
Proof.
  unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton.
Qed.
Lemma gmultiset_size_union X Y : size (X  Y) = size X + size Y.
Proof.
  unfold size, gmultiset_size; simpl.
  by rewrite gmultiset_elements_union, app_length.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
234
235
236
237
238
239
240
241

(* Order stuff *)
Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _).
Proof.
  split; [split|].
  - by intros X x.
  - intros X Y Z HXY HYZ x. by trans (multiplicity x Y).
  - intros X Y HXY HYX; apply gmultiset_eq; intros x. by apply (anti_symm ()).
Qed.

242
243
244
245
246
247
248
Lemma gmultiset_subseteq_alt X Y :
  X  Y 
  map_relation () (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
Proof.
  apply forall_proper; intros x. unfold multiplicity.
  destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver omega.
Qed.
249
Global Instance gmultiset_subseteq_dec : RelDecision (@subseteq (gmultiset A) _).
250
Proof.
251
 refine (λ X Y, cast_if (decide (map_relation ()
252
253
254
255
   (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
   by rewrite gmultiset_subseteq_alt.
Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
258
259
260
261
262
263
264
265
266
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
Hint Resolve gmultiset_subset_subseteq.

Lemma gmultiset_empty_subseteq X :   X.
Proof. intros x. rewrite multiplicity_empty. omega. Qed.

Lemma gmultiset_union_subseteq_l X Y : X  X  Y.
Proof. intros x. rewrite multiplicity_union. omega. Qed.
Lemma gmultiset_union_subseteq_r X Y : Y  X  Y.
Proof. intros x. rewrite multiplicity_union. omega. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
272
Lemma gmultiset_union_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
Proof. intros. by apply gmultiset_union_mono. Qed.
Lemma gmultiset_union_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
Proof. intros. by apply gmultiset_union_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
276
277
278
279
280
281
282
283
284

Lemma gmultiset_subset X Y : X  Y  size X < size Y  X  Y.
Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed.
Lemma gmultiset_union_subset_l X Y : Y    X  X  Y.
Proof.
  intros HY%gmultiset_size_non_empty_iff.
  apply gmultiset_subset; auto using gmultiset_union_subseteq_l.
  rewrite gmultiset_size_union; omega.
Qed.
Lemma gmultiset_union_subset_r X Y : X    Y  X  Y.
Proof. rewrite (comm_L ()). apply gmultiset_union_subset_l. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
285
Lemma gmultiset_elem_of_singleton_subseteq x X : x  X  {[ x ]}  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
289
290
291
  rewrite elem_of_multiplicity. split.
  - intros Hx y; destruct (decide (x = y)) as [->|].
    + rewrite multiplicity_singleton; omega.
    + rewrite multiplicity_singleton_ne by done; omega.
  - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
293
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
296
Lemma gmultiset_elem_of_subseteq X1 X2 x : x  X1  X1  X2  x  X2.
Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
297
298
299
300
301
302
Lemma gmultiset_union_difference X Y : X  Y  Y = X  Y  X.
Proof.
  intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
  rewrite multiplicity_union, multiplicity_difference; omega.
Qed.
Lemma gmultiset_union_difference' x Y : x  Y  Y = {[ x ]}  Y  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
305
306
Proof.
  intros. by apply gmultiset_union_difference,
    gmultiset_elem_of_singleton_subseteq.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
307

Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
310
311
312
313
Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
Proof.
  intros HX%gmultiset_union_difference.
  rewrite HX at 2; rewrite gmultiset_size_union. omega.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
314
315
316
317
318
319
320
321
322
323
324
325
326
Lemma gmultiset_non_empty_difference X Y : X  Y  Y  X  .
Proof.
  intros [_ HXY2] Hdiff; destruct HXY2; intros x.
  generalize (f_equal (multiplicity x) Hdiff).
  rewrite multiplicity_difference, multiplicity_empty; omega.
Qed.

Lemma gmultiset_difference_subset X Y : X    X  Y  Y  X  Y.
Proof.
  intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|].
  by rewrite <-(gmultiset_union_difference X Y).
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
327
(* Mononicity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
330
Proof.
  intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
  by apply submseteq_inserts_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
333
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
334
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
338
339

Lemma gmultiset_subset_size X Y : X  Y  size X < size Y.
Proof.
  intros HXY. assert (size (Y  X)  0).
Robbert Krebbers's avatar
Robbert Krebbers committed
340
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
Robbert Krebbers's avatar
Robbert Krebbers committed
341
342
343
344
345
346
347
348
  rewrite (gmultiset_union_difference X Y), gmultiset_size_union by auto. lia.
Qed.

(* Well-foundedness *)
Lemma gmultiset_wf : wf (strict (@subseteq (gmultiset A) _)).
Proof.
  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
350
351
352
353
354
355

Lemma gmultiset_ind (P : gmultiset A  Prop) :
  P   ( x X, P X  P ({[ x ]}  X))   X, P X.
Proof.
  intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
  destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
  rewrite (gmultiset_union_difference' x X) by done.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
357
  apply Hinsert, IH, gmultiset_difference_subset,
    gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
359
End lemmas.