Library stdpp.gmultiset

From stdpp Require Export countable.
From stdpp Require Import gmap.
From stdpp Require ssreflect. From stdpp Require Import options.

Multisets gmultiset A are represented as maps from A to natural numbers, which represent the multiplicity. To ensure we have canonical representations, the multiplicity is a positive. Therefore, gmultiset_car !! x = None means x has multiplicity 0 and gmultiset_car !! x = Some 1 means x has multiplicity 1.

Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A positive }.
Global Arguments GMultiSet {_ _ _} _ : assert.
Global Arguments gmultiset_car {_ _ _} _ : assert.

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

Global Program Instance gmultiset_countable `{Countable A} :
    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 ⇒ Pos.to_nat n | None ⇒ 0 end.
  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
    0 < multiplicity x X.
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x,
    multiplicity x X ≤ multiplicity x Y.
  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, ∀ x,
    multiplicity x X = multiplicity x Y.

  Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
    let (X) := X in '(x,n) ← map_to_list X; replicate (Pos.to_nat n) x.
  Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.

  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
  Global Instance gmultiset_singleton : SingletonMS A (gmultiset A) := λ x,
    GMultiSet {[ x := 1%positive ]}.
  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (x `max` y)%positive) 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)%positive) X Y.
Often called the "sum"
  Global Instance gmultiset_disj_union : DisjUnion (gmultiset A) := λ X Y,
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (x + y)%positive) X Y.
  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
    let (X) := X in let (Y) := Y in
    GMultiSet $ difference_with (λ x y,
      guard (y < x)%positive;; Some (x - y)%positive) X Y.
  Global Instance gmultiset_scalar_mul : ScalarMul nat (gmultiset A) := λ n X,
    let (X) := X in GMultiSet $
      match n with 0 ⇒ ∅ | _ ⇒ fmap (λ m, m × Pos.of_nat n)%positive X end.

  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
    let (X) := X in dom X.

  Definition gmultiset_map `{Countable B} (f : A → B)
      (X : gmultiset A) : gmultiset B :=
    GMultiSet $ map_fold
      (λ x n, partial_alter (Some ∘ from_option (Pos.add n) n) (f x))
      ∅
      (gmultiset_car X).
End definitions.

Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom gmultiset_map.

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

  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.
  Lemma multiplicity_scalar_mul n X x :
    multiplicity x (n *: X) = n × multiplicity x X.
  Proof.
    destruct X as [X]; unfold multiplicity; simpl. destruct n as [|n]; [done|].
    rewrite lookup_fmap. destruct (X !! _); simpl; lia.
  Qed.

  Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
  Proof. done. Qed.
  Lemma gmultiset_elem_of_empty x : x ∈@{gmultiset A} ∅ ↔ False.
  Proof. rewrite elem_of_multiplicity, multiplicity_empty. lia. Qed.
  Lemma gmultiset_elem_of_singleton x y : x ∈@{gmultiset A} {[+ y +]} ↔ x = y.
  Proof.
    rewrite elem_of_multiplicity, multiplicity_singleton'.
    case_decide; naive_solver lia.
  Qed.
  Lemma gmultiset_elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
  Proof. rewrite !elem_of_multiplicity, multiplicity_union. lia. Qed.
  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.
  Lemma gmultiset_elem_of_intersection X Y x : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y.
  Proof. rewrite !elem_of_multiplicity, multiplicity_intersection. lia. Qed.
  Lemma gmultiset_elem_of_scalar_mul n X x : x ∈ n *: X ↔ n ≠ 0 ∧ x ∈ X.
  Proof. rewrite !elem_of_multiplicity, multiplicity_scalar_mul. lia. Qed.

  Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
  Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
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. Turn all equalities (=), equivalences (≡), inclusions (⊆ and ⊂), and set membership relations (∈) into arithmetic (in)equalities involving multiplicity. The multiplicities of ∅, ∪, ∩, ⊎ and ∖ are turned into 0, max, min, +, and -, respectively. 2. Decompose the goal into smaller subgoals through intuitionistic reasoning. 3. Instantiate universally quantified hypotheses in hypotheses to obtain a goal that can be solved using lia. 4. Simplify multiplicities of singletons {[ x ]}.
Step (1) and (2) are implemented using the set_solver tactic, which internally calls naive_solver for step (2). Step (1) is implemented by extending the SetUnfold mechanism with a class MultisetUnfold.
Step (3) is implemented using the tactic multiset_instantiate, which instantiates universally quantified hypotheses H : ∀ x : A, P x in two ways:
  • If the goal or some hypothesis contains multiplicity y X it adds the hypothesis H y.
  • If P contains a multiset singleton {[ y ]} it adds the hypothesis H y. This is needed, for example, to prove ¬ ({[ x ]} ⊆ ∅), which is turned into hypothesis H : ∀ y, multiplicity y {[ x ]} ≤ 0 and goal False. The only way to make progress is to instantiate H with the singleton appearing in H, so variable x.
Step (4) is implemented using the tactic multiset_simplify_singletons, which simplifies occurrences of multiplicity x {[ y ]} as follows:
  • First, we try to turn these occurencess into 1 or 0 if either x = y or x ≠ y can be proved using done, respectively.
  • Second, we try to turn these occurrences into a fresh z ≤ 1 if y does not occur elsewhere in the hypotheses or goal.
  • Finally, we make a case distinction between x = y or x ≠ y. This step is done last so as to avoid needless exponential blow-ups.
The tests test_big_X in tests/multiset_solver.v show the second step reduces the running time significantly (from >10 seconds to <1 second).

Class MultisetUnfold `{Countable A} (x : A) (X : gmultiset A) (n : nat) :=
  { multiset_unfold : multiplicity x X = n }.
Global Arguments multiset_unfold {_ _ _} _ _ _ {_} : assert.
Global 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 :
    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 multiset_unfold_scalar_mul x m X n :
    MultisetUnfold x X n →
    MultisetUnfold x (m *: X) (m × n).
  Proof. intros [HX]; constructor. by rewrite multiplicity_scalar_mul, HX. 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) | 0.
  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) | 0.
  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) | 0.
  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_subset X Y f g :
    (∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
    SetUnfold (X ⊂ Y) ((∀ x, f x ≤ g x) ∧ (¬∀ x, g x ≤ f x)) | 0.
  Proof.
    constructor. unfold strict. f_equiv.
    - by apply set_unfold_multiset_subseteq.
    - f_equiv. by apply set_unfold_multiset_subseteq.
  Qed.

  Global Instance set_unfold_multiset_elem_of X x n :
    MultisetUnfold x X n → SetUnfoldElemOf x X (0 < n) | 100.
  Proof. constructor. by rewrite <-(multiset_unfold x X n). Qed.

  Global Instance set_unfold_gmultiset_empty x :
    SetUnfoldElemOf x (∅ : gmultiset A) False.
  Proof. constructor. apply gmultiset_elem_of_empty. Qed.
  Global Instance set_unfold_gmultiset_singleton x y :
    SetUnfoldElemOf x ({[+ y +]} : gmultiset A) (x = y).
  Proof. constructor; apply gmultiset_elem_of_singleton. Qed.
  Global Instance set_unfold_gmultiset_union x X Y P Q :
    SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
    SetUnfoldElemOf x (X ∪ Y) (P ∨ Q).
  Proof.
    intros ??; constructor. by rewrite gmultiset_elem_of_union,
      (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
  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.
  Global Instance set_unfold_gmultiset_intersection 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_intersection.
    by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
  Qed.
End multiset_unfold.

Step 3: instantiate hypotheses For these tactics we want to use ssreflect rewrite. ssreflect matching interacts better with canonical structures (see <https://gitlab.mpi-sws.org/iris/stdpp/-/issues/195>).
Module Export tactics.
Import ssreflect.

Ltac multiset_instantiate :=
  repeat match goal with
  | H : (∀ x : ?A, @?P x) |- _ ⇒
     let e := mk_evar A in
     lazymatch constr:(P e) with
     | context [ {[+ ?y +]} ] ⇒ unify y e; learn_hyp (H y)
     end
  | H : (∀ x : ?A, _), _ : context [multiplicity ?y _] |- _ ⇒ learn_hyp (H y)
  | H : (∀ x : ?A, _) |- context [multiplicity ?y _] ⇒ learn_hyp (H y)
  end.

Step 4: simplify singletons This lemma results in information loss if there are other occurrences of y in the goal. In the tactic multiset_simplify_singletons we use clear y to ensure we do not use the lemma if it leads to information loss.
Local Lemma multiplicity_singleton_forget `{Countable A} x y :
  ∃ n, multiplicity (A:=A) x {[+ y +]} = n ∧ n ≤ 1.
Proof. rewrite multiplicity_singleton'. case_decide; eauto with lia. Qed.

Ltac multiset_simplify_singletons :=
  repeat match goal with
  | H : context [multiplicity ?x {[+ ?y +]}] |- _ ⇒
     first
       [progress rewrite ?multiplicity_singleton ?multiplicity_singleton_ne in H; [|done..]
       
       |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
       |rewrite multiplicity_singleton' in H; destruct (decide (x = y)); simplify_eq/=]
  | |- context [multiplicity ?x {[+ ?y +]}] ⇒
     first
       [progress rewrite ?multiplicity_singleton ?multiplicity_singleton_ne; [|done..]
       
       |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
       |rewrite multiplicity_singleton'; destruct (decide (x = y)); simplify_eq/=]
  end.
End tactics.

Putting it all together Similar to set_solver and naive_solver, multiset_solver has a by parameter whose default is eauto.
Tactic Notation "multiset_solver" "by" tactic3(tac) :=
  set_solver by (multiset_instantiate;
                 multiset_simplify_singletons;
                 
                 solve [fast_done|lia|tac]).
Tactic Notation "multiset_solver" := multiset_solver by eauto.

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

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.

Element of operation
  Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
  Proof. multiset_solver. Qed.

Misc
  Global Instance gmultiset_singleton_inj : Inj (=) (=@{gmultiset A}) singletonMS.
  Proof.
    intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
    rewrite multiplicity_singleton, multiplicity_singleton' in Hx.
    case_decide; [done|lia].
  Qed.
  Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
  Proof. multiset_solver. Qed.

Scalar
  Lemma gmultiset_scalar_mul_0 X : 0 *: X = ∅.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_S_l n X : S n *: X = X ⊎ (n *: X).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_S_r n X : S n *: X = (n *: X) ⊎ X.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_1 X : 1 *: X = X.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_2 X : 2 *: X = X ⊎ X.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_empty n : n *: ∅ =@{gmultiset A} ∅.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_disj_union n X Y :
    n *: (X ⊎ Y) =@{gmultiset A} (n *: X) ⊎ (n *: Y).
  Proof. multiset_solver. Qed.
  Lemma gmultiset_scalar_mul_union n X Y :
    n *: (X ∪ Y) =@{gmultiset A} (n *: X) ∪ (n *: Y).
  Proof. set_unfold. intros x; by rewrite Nat.mul_max_distr_l. Qed.
  Lemma gmultiset_scalar_mul_intersection n X Y :
    n *: (X ∩ Y) =@{gmultiset A} (n *: X) ∩ (n *: Y).
  Proof. set_unfold. intros x; by rewrite Nat.mul_min_distr_l. Qed.
  Lemma gmultiset_scalar_mul_difference n X Y :
    n *: (X ∖ Y) =@{gmultiset A} (n *: X) ∖ (n *: Y).
  Proof. set_unfold. intros x; by rewrite Nat.mul_sub_distr_l. Qed.

  Lemma gmultiset_scalar_mul_inj_ne_0 n X1 X2 :
    n ≠ 0 → n *: X1 = n *: X2 → X1 = X2.
  Proof. set_unfold. intros ? HX x. apply (Nat.mul_reg_l _ _ n); auto. Qed.
Specialized to S n so that type class search can find it.
  Global Instance gmultiset_scalar_mul_inj_S n :
    Inj (=) (=@{gmultiset A}) (S n *:.).
  Proof. intros x1 x2. apply gmultiset_scalar_mul_inj_ne_0. lia. 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.
  Lemma elem_of_list_to_set_disj x l :
    x ∈@{gmultiset A} list_to_set_disj l ↔ x ∈ l.
  Proof. induction l; set_solver. Qed.
  Global Instance list_to_set_disj_perm :
    Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
  Proof. induction 1; multiset_solver. Qed.
  Lemma list_to_set_disj_replicate n x :
    list_to_set_disj (replicate n x) =@{gmultiset A} n *: {[+ x +]}.
  Proof. induction n; 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_iff X : elements X = [] ↔ X = ∅.
  Proof.
    split; [|intros ->; by rewrite gmultiset_elements_empty].
    destruct X as [X]; unfold elements, gmultiset_elements; simpl.
    intros; apply (f_equal GMultiSet).
    destruct (map_to_list X) as [|[x p]] eqn:?; simpl in ×.
    - by apply map_to_list_empty_iff.
    - pose proof (Pos2Nat.is_pos p). destruct (Pos.to_nat); naive_solver lia.
  Qed.
  Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
  Proof. apply gmultiset_elements_empty_iff. 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 (Pos.to_nat 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_delete Y x n') 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 Pos2Nat.inj_add, replicate_add.
    - 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_elements_scalar_mul n X :
    elements (n *: X) ≡ₚ mjoin (replicate n (elements X)).
  Proof.
    induction n as [|n IH]; simpl.
    - by rewrite gmultiset_scalar_mul_0, gmultiset_elements_empty.
    - by rewrite gmultiset_scalar_mul_S_l, gmultiset_elements_disj_union, 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 (Pos.to_nat 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].
      ∃ (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 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_strong {B} (R : relation B) `{!PreOrder R}
      (f : A → B → B) (b : B) X Y :
    (∀ x, Proper (R ==> R) (f x)) →
    (∀ x1 x2 c, x1 ∈ X ⊎ Y → x2 ∈ X ⊎ Y → R (f x1 (f x2 c)) (f x2 (f x1 c))) →
    R (set_fold f b (X ⊎ Y)) (set_fold f (set_fold f b X) Y).
  Proof.
    intros ? Hf. unfold set_fold; simpl.
    rewrite <-foldr_app. apply (foldr_permutation R f b).
    - intros j1 a1 j2 a2 c ? Ha1%elem_of_list_lookup_2 Ha2%elem_of_list_lookup_2.
      rewrite gmultiset_elem_of_elements in Ha1, Ha2. eauto.
    - rewrite (comm (++)). apply gmultiset_elements_disj_union.
  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 ??; apply gmultiset_set_fold_disj_union_strong; [apply _..|].
    intros x1 x2 ? _ _. by rewrite 2!assoc, (comm f x1 x2).
  Qed.
  Lemma gmultiset_set_fold_scalar_mul (f : A → A → A) (b : A) n X :
    Comm (=) f →
    Assoc (=) f →
    set_fold f b (n *: X) = Nat.iter n (flip (set_fold f) X) b.
  Proof.
    intros Hcomm Hassoc. induction n as [|n IH]; simpl.
    - by rewrite gmultiset_scalar_mul_0, gmultiset_set_fold_empty.
    - rewrite gmultiset_scalar_mul_S_r.
      by rewrite (gmultiset_set_fold_disj_union _ _ _ _ _ _), IH.
  Qed.

  Lemma gmultiset_set_fold_comm_acc_strong {B} (R : relation B) `{!PreOrder R}
      (f : A → B → B) (g : B → B) b X :
    (∀ x, Proper (R ==> R) (f x)) →
    (∀ x (y : B), x ∈ X → R (f x (g y)) (g (f x y))) →
    R (set_fold f (g b) X) (g (set_fold f b X)).
  Proof.
    intros ? Hfg. unfold set_fold; simpl.
    apply foldr_comm_acc_strong; [done|solve_proper|].
    intros. by apply Hfg, gmultiset_elem_of_elements.
  Qed.
  Lemma gmultiset_set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
    (∀ x c, g (f x c) = f x (g c)) →
    set_fold f (g b) X = g (set_fold f b X).
  Proof.
    intros. apply (gmultiset_set_fold_comm_acc_strong _); [solve_proper|done].
  Qed.

Properties of the size operation
  Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.
  Proof. done. Qed.
  Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
  Proof.
    unfold size, gmultiset_size; simpl.
    by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
  Qed.
  Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
  Proof. apply gmultiset_size_empty_iff. 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_iff.
    - ∃ 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, length_app.
  Qed.
  Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n × size X.
  Proof.
    induction n as [|n IH].
    - by rewrite gmultiset_scalar_mul_0, gmultiset_size_empty.
    - rewrite gmultiset_scalar_mul_S_l, gmultiset_size_disj_union, IH. lia.
  Qed.

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

  Local Lemma gmultiset_subseteq_alt X Y :
    X ⊆ Y ↔
    map_relation (λ _, Pos.le) (λ _ _, 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
       (λ _, Pos.le) (λ _ _, 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. multiset_solver. Qed.

  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. multiset_solver. Qed.
  Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
  Proof. multiset_solver. Qed.

  Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
  Proof. multiset_solver. Qed.
  Lemma gmultiset_singleton_subseteq x y :
    {[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
  Proof. multiset_solver. Qed.

  Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
  Proof. multiset_solver. 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. multiset_solver. 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. multiset_solver. 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. multiset_solver. Qed.

  Lemma gmultiset_difference_disj_union_r X Y Z : X ∖ Y = (X ⊎ Z) ∖ (Y ⊎ Z).
  Proof. multiset_solver. Qed.

  Lemma gmultiset_difference_disj_union_l X Y Z : X ∖ Y = (Z ⊎ X) ∖ (Z ⊎ Y).
  Proof. multiset_solver. 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 using gmultiset_subset_subseteq. lia.
  Qed.

Well-foundedness
  Lemma gmultiset_wf : well_founded (⊂@{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; multiset_solver.
  Qed.
End more_lemmas.

Map

Section map.
  Context `{Countable A, Countable B}.
  Context (f : A → B).

  Lemma gmultiset_map_alt X :
    gmultiset_map f X = list_to_set_disj (f <$> elements X).
  Proof.
    destruct X as [m]. unfold elements, gmultiset_map. simpl.
    induction m as [|x n m ?? IH] using map_first_key_ind; [done|].
    rewrite map_to_list_insert_first_key, map_fold_insert_first_key by done.
    csimpl. rewrite fmap_app, fmap_replicate, list_to_set_disj_app, <-IH.
    apply gmultiset_eq; intros y.
    rewrite multiplicity_disj_union, list_to_set_disj_replicate.
    rewrite multiplicity_scalar_mul, multiplicity_singleton'.
    unfold multiplicity; simpl. destruct (decide (y = f x)) as [->|].
    - rewrite lookup_partial_alter; simpl. destruct (_ !! f x); simpl; lia.
    - rewrite lookup_partial_alter_ne by done. lia.
  Qed.

  Lemma gmultiset_map_empty : gmultiset_map f ∅ = ∅.
  Proof. done. Qed.

  Lemma gmultiset_map_disj_union X Y :
    gmultiset_map f (X ⊎ Y) = gmultiset_map f X ⊎ gmultiset_map f Y.
  Proof.
    apply gmultiset_eq; intros x.
    rewrite !gmultiset_map_alt, gmultiset_elements_disj_union, fmap_app.
    by rewrite list_to_set_disj_app.
  Qed.

  Lemma gmultiset_map_singleton x :
    gmultiset_map f {[+ x +]} = {[+ f x +]}.
  Proof.
    rewrite gmultiset_map_alt, gmultiset_elements_singleton.
    multiset_solver.
  Qed.

  Lemma elem_of_gmultiset_map X y :
    y ∈ gmultiset_map f X ↔ ∃ x, y = f x ∧ x ∈ X.
  Proof.
    rewrite gmultiset_map_alt, elem_of_list_to_set_disj, elem_of_list_fmap.
    by setoid_rewrite gmultiset_elem_of_elements.
  Qed.

  Lemma multiplicity_gmultiset_map X x :
    Inj (=) (=) f →
    multiplicity (f x) (gmultiset_map f X) = multiplicity x X.
  Proof.
    intros. induction X as [|y X IH] using gmultiset_ind; [multiset_solver|].
    rewrite gmultiset_map_disj_union, gmultiset_map_singleton,
      !multiplicity_disj_union.
    multiset_solver.
  Qed.

  Global Instance gmultiset_map_inj :
    Inj (=) (=) f → Inj (=) (=) (gmultiset_map f).
  Proof.
    intros ? X Y HXY. apply gmultiset_eq; intros x.
    by rewrite <-!(multiplicity_gmultiset_map _ _ _), HXY.
  Qed.

  Global Instance set_unfold_gmultiset_map X (P : A → Prop) y :
    (∀ x, SetUnfoldElemOf x X (P x)) →
    SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x).
  Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed.

  Global Instance multiset_unfold_map x X n :
    Inj (=) (=) f →
    MultisetUnfold x X n →
    MultisetUnfold (f x) (gmultiset_map f X) n.
  Proof.
    intros ? [HX]; constructor. by rewrite multiplicity_gmultiset_map, HX.
  Qed.
End map.