phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
    x ∈ filter P X ↔ P x ∧ x ∈ X.
Proof.
    rewrite !elem_of_multiplicity, multiplicity_filter.
    case_decide; naive_solver lia.
  Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Lemma gmultiset_Forall_dom P X : set_Forall P (dom X) ↔ set_Forall P X.
Proof. apply forall_proper; intros x. by rewrite gmultiset_elem_of_dom. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_Exists_dom P X : set_Exists P (dom X) ↔ set_Exists P X.
Proof. apply exist_proper; intros x. by rewrite gmultiset_elem_of_dom. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_Forall_dec P X :
    (∀ x, Decision (P x)) → Decision (set_Forall P X).
Proof.
    refine (λ _, cast_if (decide (set_Forall P (dom X))));
      by rewrite <-gmultiset_Forall_dom.
  Defined.
(* stdpp/gmultiset.v *)
Instance gmultiset_Exists_dec P X :
    (∀ x, Decision (P x)) → Decision (set_Exists P X).
Proof.
    refine (λ _, cast_if (decide (set_Exists P (dom X))));
      by rewrite <-gmultiset_Exists_dom.
  Defined.
(* stdpp/gmultiset.v *)
(* 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 }.
(* stdpp/gmultiset.v *)
Instance multiset_unfold_default x X :
    MultisetUnfold x X (multiplicity x X) | 1000.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Instance multiset_unfold_empty x : MultisetUnfold x ∅ 0.
Proof. constructor. by rewrite multiplicity_empty. Qed.
(* stdpp/gmultiset.v *)
Instance multiset_unfold_singleton x :
    MultisetUnfold x {[+ x +]} 1.
Proof. constructor. by rewrite multiplicity_singleton_eq. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Instance multiset_unfold_filter (P : A → Prop) `{!∀ x, Decision (P x)} x X n :
    MultisetUnfold x X n →
    MultisetUnfold x (filter P X) (if decide (P x) then n else 0).
Proof. intros [HX]; constructor. by rewrite multiplicity_filter, HX. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Instance set_unfold_gmultiset_empty x :
    SetUnfoldElemOf x (∅ : gmultiset A) False.
Proof. constructor. apply gmultiset_elem_of_empty. Qed.
(* stdpp/gmultiset.v *)
Instance set_unfold_gmultiset_singleton x y :
    SetUnfoldElemOf x ({[+ y +]} : gmultiset A) (x = y).
Proof. constructor; apply gmultiset_elem_of_singleton. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Instance set_unfold_gmultiset_filter (P : A → Prop)
      `{!∀ x, Decision (P x)} x X Q :
    SetUnfoldElemOf x X Q →
    SetUnfoldElemOf x (filter P X) (P x ∧ Q).
Proof.
    intros ?; constructor.
    by rewrite gmultiset_elem_of_filter, (set_unfold_elem_of x X Q).
  Qed.
(* stdpp/gmultiset.v *)
Instance set_unfold_gmultiset_dom x X P :
    SetUnfoldElemOf x X P →
    SetUnfoldElemOf x (dom X) P.
Proof.
    constructor.
    by rewrite gmultiset_elem_of_dom, (set_unfold_elem_of x X P). 
  Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
(* 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. *)
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.
(* stdpp/gmultiset.v *)
Ltac multiset_simplify_singletons
:=
  repeat match goal with
  | H : context [multiplicity ?x {[+ ?y +]}] |- _ =>
     first
       [progress rewrite ?multiplicity_singleton_eq
                         ?multiplicity_singleton_ne in H; [|done..]
       (* This second case does *not* use ssreflect matching (due to [destruct]
       and the [->] pattern). If the default Coq matching goes wrong it will
       fail and fall back to the third case, which is strictly more general,
       just slower. *)
       |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_eq
                         ?multiplicity_singleton_ne; [|done..]
       (* Similar to above, this second case does *not* use ssreflect matching. *)
       |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
       |rewrite multiplicity_singleton; destruct (decide (x = y)); simplify_eq/=]
  end.
(* stdpp/gmultiset.v *)
(* For union *)
Instance gmultiset_union_comm : Comm (=@{gmultiset A}) (∪).
Proof. unfold Comm. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) (∪).
Proof. unfold Assoc. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_union_left_id : LeftId (=@{gmultiset A}) ∅ (∪).
Proof. unfold LeftId. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_union_right_id : RightId (=@{gmultiset A}) ∅ (∪).
Proof. unfold RightId. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) (∪).
Proof. unfold IdemP. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
(* For intersection *)
Instance gmultiset_intersection_comm : Comm (=@{gmultiset A}) (∩).
Proof. unfold Comm. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) (∩).
Proof. unfold Assoc. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A}) ∅ (∩).
Proof. unfold LeftAbsorb. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A}) ∅ (∩).
Proof. unfold RightAbsorb. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) (∩).
Proof. unfold IdemP. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_intersection_l X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_intersection_r X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_intersection_union_l X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_intersection_union_r X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
(* For disjoint union (aka sum) *)
Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) (⊎).
Proof. unfold Comm. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) (⊎).
Proof. unfold Assoc. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A}) ∅ (⊎).
Proof. unfold LeftId. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎).
Proof. unfold RightId. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎.).
Proof. unfold Inj. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
Proof. unfold Inj. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_intersection_r X Y Z : (X ∩ Y) ⊎ Z = (X ⊎ Z) ∩ (Y ⊎ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_union_l X Y Z : X ⊎ (Y ∪ Z) = (X ⊎ Y) ∪ (X ⊎ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_union_r X Y Z : (X ∪ Y) ⊎ Z = (X ⊎ Z) ∪ (Y ⊎ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
(* Element of operation *)
Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
(* Misc *)
Instance gmultiset_singleton_inj : Inj (=) (=@{gmultiset A}) singletonMS.
Proof.
    intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
    rewrite !multiplicity_singleton in Hx. repeat case_decide; done || lia.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma not_elem_of_multiplicity x X : x ∉ X ↔ multiplicity x X = 0.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
(* Scalar *)
Lemma gmultiset_scalar_mul_0 X : 0 *: X = ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_scalar_mul_S_l n X : S n *: X = X ⊎ (n *: X).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_scalar_mul_S_r n X : S n *: X = (n *: X) ⊎ X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_scalar_mul_1 X : 1 *: X = X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_scalar_mul_2 X : 2 *: X = X ⊎ X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_scalar_mul_empty n : n *: ∅ =@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_scalar_mul_disj_union n X Y :
    n *: (X ⊎ Y) =@{gmultiset A} (n *: X) ⊎ (n *: Y).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
(* Specialized to [S n] so that type class search can find it. *)
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.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_empty : filter P ∅ =@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_singleton x :
      filter P {[+ x +]} =@{gmultiset A} if decide (P x) then {[+ x +]} else ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_singleton_True x :
      P x → filter P {[+ x +]} =@{gmultiset A} {[+ x +]}.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_singleton_False x :
      ¬P x → filter P {[+ x +]} =@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_union X Y :
      filter P (X ∪ Y) = filter P X ∪ filter P Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_intersection X Y :
      filter P (X ∩ Y) = filter P X ∩ filter P Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_disj_union X Y :
      filter P (X ⊎ Y) = filter P X ⊎ filter P Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_difference X Y :
      filter P (X ∖ Y) = filter P X ∖ filter P Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_scalar_mul X n :
      filter P (n *: X) = n *: filter P X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_id X :
      (∀ x, x ∈ X → P x) → filter P X = X.
Proof.
      intros. apply gmultiset_eq; intros x.
      rewrite multiplicity_filter. case_decide; [done|].
      symmetry. apply not_elem_of_multiplicity. naive_solver.
    Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_empty_iff X :
      filter P X = ∅ ↔ (∀ x, x ∈ X → ¬ P x).
Proof.
      rewrite gmultiset_eq. apply forall_proper; intros x.
      rewrite multiplicity_filter, multiplicity_empty.
      case_decide; [|done]. rewrite <-not_elem_of_multiplicity. naive_solver.
    Qed.
(* stdpp/gmultiset.v *)
(* Conversion from lists *)
Lemma list_to_set_disj_nil : list_to_set_disj [] =@{gmultiset A} ∅.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Instance list_to_set_disj_perm :
    Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
Proof. induction 1; multiset_solver. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
(* 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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
Proof. apply gmultiset_elements_empty_iff. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
Proof.
    unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
  Qed.
(* stdpp/gmultiset.v *)
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_id 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_eq, ?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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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 list_elem_of_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.
(* stdpp/gmultiset.v *)
(* 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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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%list_elem_of_lookup_2 Ha2%list_elem_of_lookup_2.
      rewrite gmultiset_elem_of_elements in Ha1, Ha2. eauto.
    - rewrite (comm (++)). apply gmultiset_elements_disj_union.
  Qed.
(* stdpp/gmultiset.v *)
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.