gmultiset.v 21.7 KB
Newer Older
1
(* Copyright (c) 2012-2019, 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
    Countable (gmultiset A) := {|
15
  encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
21
22
23
|}.
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
    multiplicity x X  multiplicity x Y.
28
29
  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y,  x,
    multiplicity x X = multiplicity x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
30

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

35
36
  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
37
    GMultiSet {[ x := 0 ]}.
38
  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
39
40
41
42
43
44
45
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (x `max` y)) X Y.
  Global Instance gmultiset_intersection : Intersection (gmultiset A) := λ X Y,
    let (X) := X in let (Y) := Y in
    GMultiSet $ intersection_with (λ x y, Some (x `min` y)) X Y.
  (** Often called the "sum" *)
  Global Instance gmultiset_disj_union : DisjUnion (gmultiset A) := λ X Y,
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (S (x + y))) X Y.
48
  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
    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.
52

53
  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
54
    let (X) := X in dom _ X.
55
End definitions. 
Robbert Krebbers's avatar
Robbert Krebbers committed
56

57
58
59
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
60
Typeclasses Opaque gmultiset_dom.
61

Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65
66
67
68
69
70
71
72
73
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.
74
75
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
76
Global Instance gmultiset_equiv_equivalence : Equivalence (@{gmultiset A}).
77
Proof. constructor; repeat intro; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79
80
81
82
83
84
85

(* 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.
86
87
88
89
90
91
92
Lemma multiplicity_singleton' x y :
  multiplicity x {[ y ]} = if decide (x = y) then 1 else 0.
Proof.
  destruct (decide _) as [->|].
  - by rewrite multiplicity_singleton.
  - by rewrite multiplicity_singleton_ne.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Lemma multiplicity_union X Y x :
94
95
96
97
98
99
100
101
102
103
104
105
106
  multiplicity x (X  Y) = multiplicity x X `max` multiplicity x Y.
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_intersection X Y x :
  multiplicity x (X  Y) = multiplicity x X `min` multiplicity x Y.
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
  rewrite lookup_intersection_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_disj_union X Y x :
  multiplicity x (X  Y) = multiplicity x X + multiplicity x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
Ralf Jung's avatar
Ralf Jung committed
109
  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
113
114
115
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.
Ralf Jung's avatar
Ralf Jung committed
116
  destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
Qed.

119
(* Set_ *)
120
121
122
Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
Proof. done. Qed.

123
Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
124
125
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
126
  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
127
128
129
  - intros x y.
    rewrite elem_of_multiplicity, multiplicity_singleton'.
    destruct (decide (x = y)); intuition lia.
Ralf Jung's avatar
Ralf Jung committed
130
  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
131
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
133
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
134

135
136
137
Lemma gmultiset_elem_of_disj_union X Y x : x  X  Y  x  X  x  Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.

138
139
140
Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
  SetUnfold (x  X) P  SetUnfold (x  Y) Q  SetUnfold (x  X  Y) (P  Q).
Proof.
141
142
  intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
  by rewrite <-(set_unfold (x  X) P), <-(set_unfold (x  Y) Q).
143
144
Qed.

145
(* Algebraic laws *)
146
147
(** For union *)
Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Proof.
Ralf Jung's avatar
Ralf Jung committed
149
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Qed.
151
Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
Ralf Jung's avatar
Ralf Jung committed
153
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Qed.
155
Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_union, multiplicity_empty.
Qed.
160
Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
161
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
162
163
164
165
Global Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) ().
Proof.
  intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166

167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
(** For intersection *)
Global Instance gmultiset_intersection_comm : Comm (=@{gmultiset A}) ().
Proof.
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
Qed.
Global Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) ().
Proof.
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
Qed.
Global Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A})  ().
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_intersection, multiplicity_empty.
Qed.
Global Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A})  ().
Proof. intros X. by rewrite (comm_L ()), (left_absorb_L _ _). Qed.
Global Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) ().
Proof.
  intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
Qed.

188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
Lemma gmultiset_union_intersection_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
Proof.
  apply gmultiset_eq; intros y.
  rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia.
Qed.
Lemma gmultiset_union_intersection_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_union_intersection_l. Qed.
Lemma gmultiset_intersection_union_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
Proof.
  apply gmultiset_eq; intros y.
  rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia.
Qed.
Lemma gmultiset_intersection_union_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_intersection_union_l. Qed.

203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
(** For disjoint union (aka sum) *)
Global Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) ().
Proof.
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_disj_union; lia.
Qed.
Global Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) ().
Proof.
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_disj_union; lia.
Qed.
Global Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A})  ().
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_disj_union, multiplicity_empty.
Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A})  ().
218
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
219
220

Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ).
Robbert Krebbers's avatar
Robbert Krebbers committed
221
222
Proof.
  intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
223
  rewrite !multiplicity_disj_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
Qed.
225
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) ( X).
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.

228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
Lemma gmultiset_disj_union_intersection_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
Proof.
  apply gmultiset_eq; intros y.
  rewrite multiplicity_disj_union, !multiplicity_intersection,
    !multiplicity_disj_union. lia.
Qed.
Lemma gmultiset_disj_union_intersection_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_intersection_l. Qed.

Lemma gmultiset_disj_union_union_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
Proof.
  apply gmultiset_eq; intros y.
  rewrite multiplicity_disj_union, !multiplicity_union,
    !multiplicity_disj_union. lia.
Qed.
Lemma gmultiset_disj_union_union_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_union_l. Qed.

246
(** Misc *)
247
Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
Robbert Krebbers's avatar
Robbert Krebbers committed
248
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
250
  rewrite gmultiset_eq. intros Hx; generalize (Hx x).
  by rewrite multiplicity_singleton, multiplicity_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
252
Qed.

253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
(** Conversion from lists *)
Lemma list_to_set_disj_nil : list_to_set_disj [] =@{gmultiset A} .
Proof. done. Qed.
Lemma list_to_set_disj_cons x l :
  list_to_set_disj (x :: l) =@{gmultiset A} {[ x ]}  list_to_set_disj l.
Proof. done. Qed.
Lemma list_to_set_disj_app l1 l2 :
  list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1  list_to_set_disj l2.
Proof.
  induction l1 as [|x l1 IH]; simpl.
  - by rewrite (left_id_L _ _).
  - by rewrite IH, (assoc_L _).
Qed.
Global Instance list_to_set_disj_perm :
  Proper (() ==> (=)) (list_to_set_disj (C:=gmultiset A)).
Proof.
  induction 1 as [|x l l' _ IH|x y l|l l' l'' _ IH1 _ IH2]; simpl; auto.
  - by rewrite IH.
  - by rewrite !(assoc_L _), (comm_L _ {[ x ]}).
  - by rewrite IH1.
Qed.

(** Properties of the elements operation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
276
277
278
279
280
281
282
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.
283
284
285
  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
286
287
288
289
290
291
292
293
294
295
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.
296
297
Lemma gmultiset_elements_disj_union X Y :
  elements (X  Y)  elements X ++ elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
299
300
301
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.
302
  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
305
306
307
308
  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.
309
310
    rewrite (assoc_L _). f_equiv.
    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
312
313
314
315
316
317
318
319
320
321
  - 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.
Ralf Jung's avatar
Ralf Jung committed
322
  - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
Robbert Krebbers's avatar
Robbert Krebbers committed
323
    exists (x,n); split; [|by apply elem_of_map_to_list].
Ralf Jung's avatar
Ralf Jung committed
324
    apply elem_of_replicate; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
Qed.
326
327
328
329
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.
Ralf Jung's avatar
Ralf Jung committed
330
  destruct (X !! x); naive_solver lia.
331
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
332

Dan Frumin's avatar
Dan Frumin committed
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
(** Properties of the set_fold operation *)
Lemma gmultiset_set_fold_empty {B} (f : A  B  B) (b : B) :
  set_fold f b ( : gmultiset A) = b.
Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed.
Lemma gmultiset_set_fold_singleton {B} (f : A  B  B) (b : B) (a : A) :
  set_fold f b ({[a]} : gmultiset A) = f a b.
Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed.
Lemma gmultiset_set_fold_disj_union (f : A  A  A) (b : A) X Y :
  Comm (=) f 
  Assoc (=) f 
  set_fold f b (X  Y) = set_fold f (set_fold f b X) Y.
Proof.
  intros Hcomm Hassoc. unfold set_fold; simpl.
  by rewrite gmultiset_elements_disj_union, <- foldr_app, (comm (++)).
Qed.

(** Properties of the size operation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
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.
383
Lemma gmultiset_size_disj_union X Y : size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
384
385
Proof.
  unfold size, gmultiset_size; simpl.
386
  by rewrite gmultiset_elements_disj_union, app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
388

Dan Frumin's avatar
Dan Frumin committed
389
(** Order stuff *)
390
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
391
392
393
394
395
396
397
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.

398
399
400
401
402
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.
Ralf Jung's avatar
Ralf Jung committed
403
  destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
404
Qed.
405
Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
406
Proof.
407
 refine (λ X Y, cast_if (decide (map_relation ()
408
409
410
411
   (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
   by rewrite gmultiset_subseteq_alt.
Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
412
413
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
Tej Chajed's avatar
Tej Chajed committed
414
Hint Resolve gmultiset_subset_subseteq : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
416

Lemma gmultiset_empty_subseteq X :   X.
Ralf Jung's avatar
Ralf Jung committed
417
Proof. intros x. rewrite multiplicity_empty. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
419

Lemma gmultiset_union_subseteq_l X Y : X  X  Y.
Ralf Jung's avatar
Ralf Jung committed
420
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Lemma gmultiset_union_subseteq_r X Y : Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
422
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
424
425
426
427
Proof.
  intros HX HY x. rewrite !multiplicity_union.
  specialize (HX x); specialize (HY x); lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
428
429
430
431
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
432

433
434
435
436
437
438
439
440
441
442
443
Lemma gmultiset_disj_union_subseteq_l X Y : X  X  Y.
Proof. intros x. rewrite multiplicity_disj_union. lia. Qed.
Lemma gmultiset_disj_union_subseteq_r X Y : Y  X  Y.
Proof. intros x. rewrite multiplicity_disj_union. lia. Qed.
Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
Proof. intros ?? x. rewrite !multiplicity_disj_union. by apply Nat.add_le_mono. Qed.
Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
Proof. intros. by apply gmultiset_disj_union_mono. Qed.
Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
Proof. intros. by apply gmultiset_disj_union_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
444
Lemma gmultiset_subset X Y : X  Y  size X < size Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
445
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
446
Lemma gmultiset_disj_union_subset_l X Y : Y    X  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
448
Proof.
  intros HY%gmultiset_size_non_empty_iff.
449
450
  apply gmultiset_subset; auto using gmultiset_disj_union_subseteq_l.
  rewrite gmultiset_size_disj_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
451
Qed.
452
453
Lemma gmultiset_union_subset_r X Y : X    Y  X  Y.
Proof. rewrite (comm_L ()). apply gmultiset_disj_union_subset_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
454

Robbert Krebbers's avatar
Robbert Krebbers committed
455
Lemma gmultiset_elem_of_singleton_subseteq x X : x  X  {[ x ]}  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
  rewrite elem_of_multiplicity. split.
458
459
  - intros Hx y. rewrite multiplicity_singleton'.
    destruct (decide (y = x)); naive_solver lia.
Ralf Jung's avatar
Ralf Jung committed
460
  - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
461
462
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
Lemma gmultiset_elem_of_subseteq X1 X2 x : x  X1  X1  X2  x  X2.
Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.

466
Lemma gmultiset_disj_union_difference X Y : X  Y  Y = X  Y  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
Proof.
  intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
469
  rewrite multiplicity_disj_union, multiplicity_difference; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
Qed.
471
Lemma gmultiset_disj_union_difference' x Y : x  Y  Y = {[ x ]}  Y  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
472
Proof.
473
  intros. by apply gmultiset_disj_union_difference,
Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
    gmultiset_elem_of_singleton_subseteq.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
476

Robbert Krebbers's avatar
Robbert Krebbers committed
477
478
Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
Proof.
479
480
  intros HX%gmultiset_disj_union_difference.
  rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
481
482
Qed.

Dan Frumin's avatar
Dan Frumin committed
483
484
485
486
487
488
489
Lemma gmultiset_empty_difference X Y : Y  X  Y  X = .
Proof.
  intros HYX. unfold_leibniz. intros x.
  rewrite multiplicity_difference, multiplicity_empty.
  specialize (HYX x). lia.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
490
491
492
493
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).
Ralf Jung's avatar
Ralf Jung committed
494
  rewrite multiplicity_difference, multiplicity_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
495
496
Qed.

Dan Frumin's avatar
Dan Frumin committed
497
498
499
Lemma gmultiset_difference_diag X : X  X = .
Proof. by apply gmultiset_empty_difference. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
500
501
502
Lemma gmultiset_difference_subset X Y : X    X  Y  Y  X  Y.
Proof.
  intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|].
503
  by rewrite <-(gmultiset_disj_union_difference X Y).
Robbert Krebbers's avatar
Robbert Krebbers committed
504
505
Qed.

Dan Frumin's avatar
Dan Frumin committed
506
(** Mononicity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
507
Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
508
Proof.
509
  intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
  by apply submseteq_inserts_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
512
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
513
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
514
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
517
518

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
519
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
520
521
  rewrite (gmultiset_disj_union_difference X Y),
    gmultiset_size_disj_union by auto. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
Qed.

Dan Frumin's avatar
Dan Frumin committed
524
(** Well-foundedness *)
525
Lemma gmultiset_wf : wf (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
526
527
528
Proof.
  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
529
530

Lemma gmultiset_ind (P : gmultiset A  Prop) :
531
  P   ( x X, P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
534
Proof.
  intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
  destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
535
  rewrite (gmultiset_disj_union_difference' x X) by done.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
537
  apply Hinsert, IH, gmultiset_difference_subset,
    gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
539
End lemmas.