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

Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
7 8
Arguments GMultiSet {_ _ _} _ : assert.
Arguments gmultiset_car {_ _ _} _ : assert.
9

10
Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
11 12
Proof. solve_decision. Defined.

13
Program Instance gmultiset_countable `{Countable A} :
14
    Countable (gmultiset A) := {|
15
  encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
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,
25
    0 < multiplicity x X.
26
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y,  x,
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.
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.
34

35 36
  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
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,
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,
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. 
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

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.
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.
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.
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.
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.
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
Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
139 140
  SetUnfoldElemOf x X P  SetUnfoldElemOf x Y Q 
  SetUnfoldElemOf x (X  Y) (P  Q).
141
Proof.
142
  intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
143
  by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
144 145
Qed.

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

168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
(** 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.

189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
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.

204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
(** 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})  ().
219
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
220 221

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

229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
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.

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

254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
(** 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 *)
277 278 279 280 281 282 283
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.
284 285 286
  intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?.
  - by apply map_to_list_empty_inv.
  - naive_solver.
287 288 289 290 291 292 293 294 295 296
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.
297 298
Lemma gmultiset_elements_disj_union X Y :
  elements (X  Y)  elements X ++ elements Y.
299 300 301 302
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.
303
  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
304 305 306 307 308 309
  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.
310 311
    rewrite (assoc_L _). f_equiv.
    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
312 313 314 315 316 317 318 319 320 321 322
  - 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
323
  - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
324
    exists (x,n); split; [|by apply elem_of_map_to_list].
Ralf Jung's avatar
Ralf Jung committed
325
    apply elem_of_replicate; auto with lia.
326
Qed.
327 328 329 330
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
331
  destruct (X !! x); naive_solver lia.
332
Qed.
333

Dan Frumin's avatar
Dan Frumin committed
334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
(** 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 *)
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 383
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.
384
Lemma gmultiset_size_disj_union X Y : size (X  Y) = size X + size Y.
385 386
Proof.
  unfold size, gmultiset_size; simpl.
387
  by rewrite gmultiset_elements_disj_union, app_length.
388
Qed.
389

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

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

413 414
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
415
Hint Resolve gmultiset_subset_subseteq : core.
416 417

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

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

434 435 436 437 438 439 440 441 442 443 444
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.

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

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

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

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

478 479
Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
Proof.
480 481
  intros HX%gmultiset_disj_union_difference.
  rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
482 483
Qed.

Dan Frumin's avatar
Dan Frumin committed
484 485 486 487 488 489 490
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.

491 492 493 494
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
495
  rewrite multiplicity_difference, multiplicity_empty; lia.
496 497
Qed.

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

501 502 503
Lemma gmultiset_difference_subset X Y : X    X  Y  Y  X  Y.
Proof.
  intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|].
504
  by rewrite <-(gmultiset_disj_union_difference X Y).
505 506
Qed.

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

514
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
515
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
516 517 518 519

Lemma gmultiset_subset_size X Y : X  Y  size X < size Y.
Proof.
  intros HXY. assert (size (Y  X)  0).
520
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
521 522
  rewrite (gmultiset_disj_union_difference X Y),
    gmultiset_size_disj_union by auto. lia.
523 524
Qed.

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

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