gmultiset.v 25.3 KB
Newer Older
1
From stdpp Require Export countable.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From stdpp Require Import gmap.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5

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

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

12
Program Instance gmultiset_countable `{Countable A} :
Robbert Krebbers's avatar
Robbert Krebbers committed
13
    Countable (gmultiset A) := {|
14
  encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17 18 19 20 21 22
|}.
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.
23
  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
Robbert Krebbers's avatar
Robbert Krebbers committed
24
    0 < multiplicity x X.
25
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y,  x,
Robbert Krebbers's avatar
Robbert Krebbers committed
26
    multiplicity x X  multiplicity x Y.
27 28
  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y,  x,
    multiplicity x X = multiplicity x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

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

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

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

56 57 58
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
59
Typeclasses Opaque gmultiset_dom.
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
Section basic_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.
  Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
  Proof. intros X Y. by rewrite gmultiset_eq. Qed.
  Global Instance gmultiset_equiv_equivalence : Equivalence (@{gmultiset A}).
  Proof. constructor; repeat intro; 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_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.
  Lemma multiplicity_union X Y x :
    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.
  Proof.
    destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
    rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
  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; lia.
  Qed.

  (* Set *)
  Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
  Proof. done. Qed.

  Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
  Proof.
    split.
    - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
    - intros x y.
      rewrite elem_of_multiplicity, multiplicity_singleton'.
      destruct (decide (x = y)); intuition lia.
    - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
  Qed.
  Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
  Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.

  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.

  Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
    SetUnfoldElemOf x X P  SetUnfoldElemOf x Y Q 
    SetUnfoldElemOf x (X  Y) (P  Q).
  Proof.
    intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
    by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
  Qed.
End basic_lemmas.

(** * A solver for multisets *)
(** We define a tactic [multiset_solver] that solves goals involving multisets.
The strategy of this tactic is as follows:

1. Unfold all equalities ([=]), equivalences ([≡]), and inclusions ([⊆]) using
   the laws of [multiplicity] for the multiset operations. Note that strict
   inclusion ([⊂]) is not supported.
2. Use [naive_solver] to decompose the goal into smaller subgoals.
3. Instantiate all universally quantified hypotheses in the subgoals generated
   by [naive_solver] to obtain goals that can be solved using [lia].

Step (1) is implemented using a type class [MultisetUnfold] that hooks into
the [SetUnfold] mechanism of [set_solver]. Since [SetUnfold] already propagates
through logical connectives, we obtain the same behavior for our multiset
solver. Note that no [MultisetUnfold] instance is defined for the (non-trivial)
singleton [{[ y ]}] since the singleton receives special treatment in step (3).

Step (3) is achieved using the tactic [multiset_instantiate], which instantiates
universally quantified hypotheses [H : ∀ x : A, P x] in two ways:

166 167 168
- If [P] contains a multiset singleton [{[ y ]}] it adds the hypothesis [H y].
- If the goal or some hypothesis contains [multiplicity y X] it adds the
  hypothesis [H y].
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
*)
Class MultisetUnfold `{Countable A} (x : A) (X : gmultiset A) (n : nat) :=
  { multiset_unfold : multiplicity x X = n }.
Arguments multiset_unfold {_ _ _} _ _ _ {_} : assert.
Hint Mode MultisetUnfold + + + - + - : typeclass_instances.

Section multiset_unfold.
  Context `{Countable A}.
  Implicit Types x y : A.
  Implicit Types X Y : gmultiset A.

  Global Instance multiset_unfold_default x X :
    MultisetUnfold x X (multiplicity x X) | 1000.
  Proof. done. Qed.
  Global Instance multiset_unfold_empty x : MultisetUnfold x  0.
  Proof. constructor. by rewrite multiplicity_empty. Qed.
  Global Instance multiset_unfold_singleton x y :
    MultisetUnfold x {[ x ]} 1.
  Proof. constructor. by rewrite multiplicity_singleton. Qed.
  Global Instance multiset_unfold_union x X Y n m :
    MultisetUnfold x X n  MultisetUnfold x Y m 
    MultisetUnfold x (X  Y) (n `max` m).
  Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_union, HX, HY. Qed.
  Global Instance multiset_unfold_intersection x X Y n m :
    MultisetUnfold x X n  MultisetUnfold x Y m 
    MultisetUnfold x (X  Y) (n `min` m).
  Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_intersection, HX, HY. Qed.
  Global Instance multiset_unfold_disj_union x X Y n m :
    MultisetUnfold x X n  MultisetUnfold x Y m 
    MultisetUnfold x (X  Y) (n + m).
  Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_disj_union, HX, HY. Qed.
  Global Instance multiset_unfold_difference x X Y n m :
    MultisetUnfold x X n  MultisetUnfold x Y m 
    MultisetUnfold x (X  Y) (n - m).
  Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_difference, HX, HY. Qed.

  Global Instance set_unfold_multiset_equiv X Y f g :
    ( x, MultisetUnfold x X (f x))  ( x, MultisetUnfold x Y (g x)) 
    SetUnfold (X  Y) ( x, f x = g x).
  Proof.
    constructor. apply forall_proper; intros x.
    by rewrite (multiset_unfold x X (f x)), (multiset_unfold x Y (g x)).
  Qed.
  Global Instance set_unfold_multiset_eq X Y f g :
    ( x, MultisetUnfold x X (f x))  ( x, MultisetUnfold x Y (g x)) 
    SetUnfold (X = Y) ( x, f x = g x).
  Proof. constructor. unfold_leibniz. by apply set_unfold_multiset_equiv. Qed.
  Global Instance set_unfold_multiset_subseteq X Y f g :
    ( x, MultisetUnfold x X (f x))  ( x, MultisetUnfold x Y (g x)) 
    SetUnfold (X  Y) ( x, f x  g x).
  Proof.
    constructor. apply forall_proper; intros x.
    by rewrite (multiset_unfold x X (f x)), (multiset_unfold x Y (g x)).
  Qed.
End multiset_unfold.

Ltac multiset_instantiate :=
  (* Step 3.1: instantiate hypotheses *)
  repeat match goal with
  | H : ( x : ?A, @?P x) |- _ =>
     let e := fresh in evar (e:A);
     let e' := eval unfold e in e in clear e;
     lazymatch constr:(P e') with
     | context [ {[ ?y ]} ] =>
        (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
        already exists. *)
        unify y e'; unless (P y) by assumption; pose proof (H y)
     end
237 238 239 240
  | H : ( x : ?A, @?P x), _ : context [multiplicity ?y _] |- _ =>
     (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
     already exists. *)
     unless (P y) by assumption; pose proof (H y)
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 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 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 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588
  | H : ( x : ?A, @?P x) |- context [multiplicity ?y _] =>
     (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
     already exists. *)
     unless (P y) by assumption; pose proof (H y)
  end;
  (* Step 3.2: simplify singletons. *)
  (* Note that we do not use [repeat case_decide] since that leads to an
  exponential explosion in the number of singletons. *)
  repeat match goal with
  | H : context [multiplicity _ {[ _ ]}] |- _ =>
     progress (rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne in H by done)
  | |- context [multiplicity _ {[ _ ]}] =>
     progress (rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne by done)
  end.

Ltac multiset_solver := set_solver by (multiset_instantiate; lia).

Section more_lemmas.
  Context `{Countable A}.
  Implicit Types x y : A.
  Implicit Types X Y : gmultiset A.

  (* Algebraic laws *)
  (** For union *)
  Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) ().
  Proof. unfold Comm. multiset_solver. Qed.
  Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) ().
  Proof. unfold Assoc. multiset_solver. Qed.
  Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A})  ().
  Proof. unfold LeftId. multiset_solver. Qed.
  Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A})  ().
  Proof. unfold RightId. multiset_solver. Qed.
  Global Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) ().
  Proof. unfold IdemP. multiset_solver. Qed.

  (** For intersection *)
  Global Instance gmultiset_intersection_comm : Comm (=@{gmultiset A}) ().
  Proof. unfold Comm. multiset_solver. Qed.
  Global Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) ().
  Proof. unfold Assoc. multiset_solver. Qed.
  Global Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A})  ().
  Proof. unfold LeftAbsorb. multiset_solver. Qed.
  Global Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A})  ().
  Proof. unfold RightAbsorb. multiset_solver. Qed.
  Global Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) ().
  Proof. unfold IdemP. multiset_solver. Qed.

  Lemma gmultiset_union_intersection_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_union_intersection_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_intersection_union_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_intersection_union_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
  Proof. multiset_solver. Qed.

  (** For disjoint union (aka sum) *)
  Global Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) ().
  Proof. unfold Comm. multiset_solver. Qed.
  Global Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) ().
  Proof. unfold Assoc. multiset_solver. Qed.
  Global Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A})  ().
  Proof. unfold LeftId. multiset_solver. Qed.
  Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A})  ().
  Proof. unfold RightId. multiset_solver. Qed.

  Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X .).
  Proof. unfold Inj. multiset_solver. Qed.
  Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (. X).
  Proof. unfold Inj. multiset_solver. Qed.

  Lemma gmultiset_disj_union_intersection_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_intersection_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
  Proof. multiset_solver. Qed.

  Lemma gmultiset_disj_union_union_l X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_union_r X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
  Proof. multiset_solver. Qed.

  (** Misc *)
  Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
  Proof. multiset_solver. Qed.

  (** 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; multiset_solver. Qed.
  Global Instance list_to_set_disj_perm :
    Proper (() ==> (=)) (list_to_set_disj (C:=gmultiset A)).
  Proof. induction 1; multiset_solver. Qed.

  (** 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.
    intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?.
    - by apply map_to_list_empty_inv.
    - naive_solver.
  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_disj_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.
    { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
    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.
      rewrite (assoc_L _). f_equiv.
      rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
    - 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; [|lia].
      exists (x,n); split; [|by apply elem_of_map_to_list].
      apply elem_of_replicate; auto with lia.
  Qed.
  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 lia.
  Qed.

  (** 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 *)
  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_disj_union X Y : size (X  Y) = size X + size Y.
  Proof.
    unfold size, gmultiset_size; simpl.
    by rewrite gmultiset_elements_disj_union, app_length.
  Qed.

  (** Order stuff *)
  Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
  Proof. repeat split; repeat intro; multiset_solver. Qed.

  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 lia.
  Qed.
  Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
  Proof.
   refine (λ X Y, cast_if (decide (map_relation ()
     (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
     by rewrite gmultiset_subseteq_alt.
  Defined.

  Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
  Proof. apply strict_include. Qed.
  Hint Resolve gmultiset_subset_subseteq : core.

  Lemma gmultiset_empty_subseteq X :   X.
  Proof. multiset_solver. Qed.

  Lemma gmultiset_union_subseteq_l X Y : X  X  Y.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_union_subseteq_r X Y : Y  X  Y.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_union_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_union_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
  Proof. multiset_solver. Qed.

  Lemma gmultiset_disj_union_subseteq_l X Y : X  X  Y.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_subseteq_r X Y : Y  X  Y.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
  Proof. multiset_solver. Qed.

  Lemma gmultiset_subset X Y : X  Y  size X < size Y  X  Y.
  Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
  Lemma gmultiset_disj_union_subset_l X Y : Y    X  X  Y.
  Proof.
    intros HY%gmultiset_size_non_empty_iff.
    apply gmultiset_subset; auto using gmultiset_disj_union_subseteq_l.
    rewrite gmultiset_size_disj_union; lia.
  Qed.
  Lemma gmultiset_union_subset_r X Y : X    Y  X  Y.
  Proof. rewrite (comm_L ()). apply gmultiset_disj_union_subset_l. Qed.

  Lemma gmultiset_elem_of_singleton_subseteq x X : x  X  {[ x ]}  X.
  Proof.
    rewrite elem_of_multiplicity. split.
    - intros Hx y. rewrite multiplicity_singleton'.
      destruct (decide (y = x)); naive_solver lia.
    - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
  Qed.

  Lemma gmultiset_elem_of_subseteq X1 X2 x : x  X1  X1  X2  x  X2.
  Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.

  Lemma gmultiset_disj_union_difference X Y : X  Y  Y = X  Y  X.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_disj_union_difference' x Y : x  Y  Y = {[ x ]}  Y  {[ x ]}.
  Proof.
    intros. by apply gmultiset_disj_union_difference,
      gmultiset_elem_of_singleton_subseteq.
  Qed.

  Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
  Proof.
    intros HX%gmultiset_disj_union_difference.
    rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
  Qed.

  Lemma gmultiset_empty_difference X Y : Y  X  Y  X = .
  Proof. multiset_solver. Qed.

  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; lia.
  Qed.

  Lemma gmultiset_difference_diag X : X  X = .
  Proof. multiset_solver. 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_disj_union_difference X Y).
  Qed.

  (** Mononicity *)
  Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
  Proof.
    intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
    by apply submseteq_inserts_r.
  Qed.

  Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
  Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.

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

  (** Well-foundedness *)
  Lemma gmultiset_wf : wf (@{gmultiset A}).
  Proof.
    apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
  Qed.

  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_disj_union_difference' x X) by done.
    apply Hinsert, IH, gmultiset_difference_subset,
      gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
  Qed.
End more_lemmas.