phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/gmap.v *)
Lemma gmap_dep_lookup_partial_alter_eq {A P} (f : option A → option A)
    (mt : gmap_dep A P) i (p : P i) :
  gmap_dep_lookup i (gmap_dep_partial_alter f i p mt) = f (gmap_dep_lookup i mt).
Proof.
  revert i p. induction mt using gmap_dep_ind.
  { intros i p; simpl. destruct (f None); simpl; [|done].
    by rewrite gmap_dep_ne_lookup_singleton_eq. }
  intros [] ?;
    rewrite gmap_dep_partial_alter_GNode, !gmap_dep_lookup_GNode by done;
    done || by destruct (f _).
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_lookup_partial_alter_ne {A P} (f : option A → option A)
    (mt : gmap_dep A P) i (p : P i) j :
  i ≠ j →
  gmap_dep_lookup j (gmap_dep_partial_alter f i p mt) = gmap_dep_lookup j mt.
Proof.
  revert i p j; induction mt using gmap_dep_ind.
  { intros i p j ?; simpl. destruct (f None); simpl; [|done].
    by rewrite gmap_dep_ne_lookup_singleton_ne. }
  intros [] ? [] ?;
    rewrite gmap_dep_partial_alter_GNode, !gmap_dep_lookup_GNode by done;
    auto with lia.
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_lookup_fmap {A B P} (f : A → B) (mt : gmap_dep A P) i :
  gmap_dep_lookup i (gmap_dep_fmap f mt) = f <$> gmap_dep_lookup i mt.
Proof.
  destruct mt as [|t]; simpl; [done|].
  revert i. induction t; intros []; by simpl.
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_omap_GNode {A B P} (f : A → option B)
    (ml : gmap_dep A P~0) mx mr :
  GNode_valid ml mx mr →
  gmap_dep_omap f (GNode ml mx mr) =
    GNode (gmap_dep_omap f ml) ('(p,x) ← mx; (p,.) <$> f x) (gmap_dep_omap f mr).
Proof. by destruct ml, mx as [[]|], mr. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_lookup_omap {A B P} (f : A → option B) (mt : gmap_dep A P) i :
  gmap_dep_lookup i (gmap_dep_omap f mt) = gmap_dep_lookup i mt ≫= f.
Proof.
  revert i. induction mt using gmap_dep_ind; [done|].
  intros [];
    rewrite gmap_dep_omap_GNode, !gmap_dep_lookup_GNode by done; [done..|].
  destruct select (option _) as [[]|]; simpl; by try destruct (f _).
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_merge_GNode_GEmpty {P} (ml : gmap_dep A P~0) mx mr :
    GNode_valid ml mx mr →
    gmap_dep_merge f (GNode ml mx mr) GEmpty =
      GNode (gmap_dep_omap (λ x, f (Some x) None) ml) (diag_None' f mx None)
            (gmap_dep_omap (λ x, f (Some x) None) mr).
Proof. by destruct ml, mx as [[]|], mr. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_merge_GEmpty_GNode {P} (ml : gmap_dep B P~0) mx mr :
    GNode_valid ml mx mr →
    gmap_dep_merge f GEmpty (GNode ml mx mr) =
      GNode (gmap_dep_omap (λ x, f None (Some x)) ml) (diag_None' f None mx)
            (gmap_dep_omap (λ x, f None (Some x)) mr).
Proof. by destruct ml, mx as [[]|], mr. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_merge_GNode_GNode {P}
      (ml1 : gmap_dep A P~0) ml2 mx1 mx2 mr1 mr2 :
    GNode_valid ml1 mx1 mr1 → GNode_valid ml2 mx2 mr2 →
    gmap_dep_merge f (GNode ml1 mx1 mr1) (GNode ml2 mx2 mr2) =
      GNode (gmap_dep_merge f ml1 ml2) (diag_None' f mx1 mx2)
            (gmap_dep_merge f mr1 mr2).
Proof. by destruct ml1, mx1 as [[]|], mr1, ml2, mx2 as [[]|], mr2. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_lookup_merge {P} (mt1 : gmap_dep A P) (mt2 : gmap_dep B P) i :
    gmap_dep_lookup i (gmap_dep_merge f mt1 mt2) =
      diag_None f (gmap_dep_lookup i mt1) (gmap_dep_lookup i mt2).
Proof.
    revert mt2 i; induction mt1 using gmap_dep_ind; intros mt2 i.
    { induction mt2 using gmap_dep_ind; [done|].
      rewrite gmap_dep_merge_GEmpty_GNode, gmap_dep_lookup_GNode by done.
      destruct i as [i|i|];
        rewrite ?gmap_dep_lookup_omap, gmap_dep_lookup_GNode; simpl;
        [by destruct (gmap_dep_lookup i _)..|].
      destruct select (option _) as [[]|]; simpl; by try destruct (f _). }
    destruct mt2 using gmap_dep_ind.
    { rewrite gmap_dep_merge_GNode_GEmpty, gmap_dep_lookup_GNode by done.
      destruct i as [i|i|];
        rewrite ?gmap_dep_lookup_omap, gmap_dep_lookup_GNode; simpl;
        [by destruct (gmap_dep_lookup i _)..|].
      destruct select (option _) as [[]|]; simpl; by try destruct (f _). }
    rewrite gmap_dep_merge_GNode_GNode by done.
    destruct i; rewrite ?gmap_dep_lookup_GNode; [done..|].
    repeat destruct select (option _) as [[]|]; simpl; by try destruct (f _).
  Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_fold_GNode {A B} (f : positive → A → B → B)
    {P} i y (ml : gmap_dep A P~0) mx mr :
  gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
    (gmap_dep_fold f i~0
      match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
Proof. by destruct ml, mx as [[]|], mr. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_fold_ind {A} {P} (Q : gmap_dep A P → Prop) :
  Q GEmpty →
  (∀ i p x mt,
    gmap_dep_lookup i mt = None →
    (∀ j A' B (f : positive → A' → B → B) (g : A → A') b x',
      gmap_dep_fold f j b
        (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
      = f (Pos.reverse_go i j) x' (gmap_dep_fold f j b (gmap_dep_fmap g mt))) →
    Q mt → Q (gmap_dep_partial_alter (λ _, Some x) i p mt)) →
  ∀ mt, Q mt.
Proof.
  intros Hemp Hinsert mt. revert Q Hemp Hinsert.
  induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
    intros Q Hemp Hinsert; [done|].
  apply (IHr (λ mt, Q (GNode ml mx mt))).
  { apply (IHl (λ mt, Q (GNode mt mx GEmpty))).
    { destruct mx as [[p x]|]; [|done].
      replace (GNode GEmpty (Some (p,x)) GEmpty) with
        (gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
      by apply Hinsert. }
    intros i p x mt r ? Hfold.
    replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
      with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
      by (by destruct mt, mx as [[]|]).
    apply Hinsert.
    - by rewrite gmap_dep_lookup_GNode.
    - intros j A' B f g b x'.
      replace (gmap_dep_partial_alter (λ _, Some x') (i~0) p
          (gmap_dep_fmap g (GNode mt mx GEmpty)))
        with (GNode (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
          (prod_map id g <$> mx) GEmpty)
        by (by destruct mt, mx as [[]|]).
      replace (gmap_dep_fmap g (GNode mt mx GEmpty))
        with (GNode (gmap_dep_fmap g mt) (prod_map id g <$> mx) GEmpty)
        by (by destruct mt, mx as [[]|]).
      rewrite !gmap_dep_fold_GNode; simpl; auto.
    - done. }
  intros i p x mt r ? Hfold.
  replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
    with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
    by (by destruct ml, mx as [[]|], mt).
  apply Hinsert.
  - by rewrite gmap_dep_lookup_GNode.
  - intros j A' B f g b x'.
    replace (gmap_dep_partial_alter (λ _, Some x') (i~1) p
        (gmap_dep_fmap g (GNode ml mx mt)))
      with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx)
        (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt)))
      by (by destruct ml, mx as [[]|], mt).
    replace (gmap_dep_fmap g (GNode ml mx mt))
      with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx) (gmap_dep_fmap g mt))
      by (by destruct ml, mx as [[]|], mt).
    rewrite !gmap_dep_fold_GNode; simpl; auto.
  - done.
Qed.
(* stdpp/gmap.v *)
(* Instance of the finite map type class *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
Proof.
  split.
  - intros A [mt1] [mt2] Hlookup. f_equal. apply (gmap_dep_eq _ _ _).
    intros i [Hk]. destruct (decode i) as [k|]; simplify_eq/=. apply Hlookup.
  - done.
  - intros A f [mt] i. apply gmap_dep_lookup_partial_alter_eq.
  - intros A f [mt] i j ?. apply gmap_dep_lookup_partial_alter_ne. naive_solver.
  - intros A b f [mt] i. apply gmap_dep_lookup_fmap.
  - intros A B f [mt] i. apply gmap_dep_lookup_omap.
  - intros A B C f [mt1] [mt2] i. apply gmap_dep_lookup_merge.
  - done.
  - intros A P Hemp Hins [mt].
    apply (gmap_dep_fold_ind (λ mt, P (GMap mt))); clear mt; [done|].
    intros i [Hk] x mt ? Hfold. destruct (fmap_Some_1 _ _ _ Hk) as (k&Hk'&->).
    assert (GMapKey Hk = gmap_key_encode k) as Hkk by (apply proof_irrel).
    rewrite Hkk in Hfold |- *. clear Hk Hkk.
    apply (Hins k x (GMap mt)); [done|]. intros A' B f g b x'.
    trans ((match decode (encode k) with Some k => f k x' | None => id end)
      (map_fold f b (g <$> GMap mt))); [apply (Hfold 1)|].
    by rewrite Hk'.
Qed.
(* stdpp/gmap.v *)
Instance gmap_countable
    `{Countable K, Countable A} : Countable (gmap K A) := {
  encode m := encode (map_to_list m : list (K * A));
  decode p := list_to_map <$> decode p
}.
Next Obligation.
  intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
  by rewrite list_to_map_to_list.
Qed.
(* stdpp/gmap.v *)
(* Conversion to/from [Pmap] *)
Definition gmap_dep_ne_to_pmap_ne {A} : ∀ {P}, gmap_dep_ne A P → Pmap_ne A
:=
  fix go {P} t :=
    match t with
    | GNode001 r => PNode001 (go r)
    | GNode010 _ x => PNode010 x
    | GNode011 _ x r => PNode011 x (go r)
    | GNode100 l => PNode100 (go l)
    | GNode101 l r => PNode101 (go l) (go r)
    | GNode110 l _ x => PNode110 (go l) x
    | GNode111 l _ x r => PNode111 (go l) x (go r)
    end.
(* stdpp/gmap.v *)
Definition gmap_dep_to_pmap {A P} (mt : gmap_dep A P) : Pmap A
:=
  match mt with
  | GEmpty => PEmpty
  | GNodes t => PNodes (gmap_dep_ne_to_pmap_ne t)
  end.
(* stdpp/gmap.v *)
Definition gmap_to_pmap {A} (m : gmap positive A) : Pmap A
:=
  let '(GMap mt) := m in gmap_dep_to_pmap mt.
(* stdpp/gmap.v *)
Lemma lookup_gmap_dep_ne_to_pmap_ne {A P} (t : gmap_dep_ne A P) i :
  gmap_dep_ne_to_pmap_ne t !! i = gmap_dep_ne_lookup i t.
Proof. revert i; induction t; intros []; by simpl. Qed.
(* stdpp/gmap.v *)
Lemma lookup_gmap_to_pmap {A} (m : gmap positive A) i :
  gmap_to_pmap m !! i = m !! i.
Proof. destruct m as [[|t]]; [done|]. apply lookup_gmap_dep_ne_to_pmap_ne. Qed.
(* stdpp/gmap.v *)
Definition pmap_ne_to_gmap_dep_ne {A} :
    ∀ {P}, (∀ i, P i) → Pmap_ne A → gmap_dep_ne A P
:=
  fix go {P} (p : ∀ i, P i) t :=
    match t with
    | PNode001 r => GNode001 (go p~1 r)
    | PNode010 x => GNode010 (p 1) x
    | PNode011 x r => GNode011 (p 1) x (go p~1 r)
    | PNode100 l => GNode100 (go p~0 l)
    | PNode101 l r => GNode101 (go p~0 l) (go p~1 r)
    | PNode110 l x => GNode110 (go p~0 l) (p 1) x
    | PNode111 l x r => GNode111 (go p~0 l) (p 1) x (go p~1 r)
    end%function.
(* stdpp/gmap.v *)
Definition pmap_to_gmap_dep {A P}
    (p : ∀ i, P i) (mt : Pmap A) : gmap_dep A P
:=
  match mt with
  | PEmpty => GEmpty
  | PNodes t => GNodes (pmap_ne_to_gmap_dep_ne p t)
  end.
(* stdpp/gmap.v *)
Definition pmap_to_gmap {A} (m : Pmap A) : gmap positive A
:=
  GMap $ pmap_to_gmap_dep gmap_key_encode m.
(* stdpp/gmap.v *)
Lemma lookup_pmap_ne_to_gmap_dep_ne {A P} (p : ∀ i, P i) (t : Pmap_ne A) i :
  gmap_dep_ne_lookup i (pmap_ne_to_gmap_dep_ne p t) = t !! i.
Proof. revert P i p; induction t; intros ? [] ?; by simpl. Qed.
(* stdpp/gmap.v *)
Lemma lookup_pmap_to_gmap {A} (m : Pmap A) i : pmap_to_gmap m !! i = m !! i.
Proof. destruct m as [|t]; [done|]. apply lookup_pmap_ne_to_gmap_dep_ne. Qed.
(* stdpp/gmap.v *)
(* * Finite sets *)
Definition gset K `{Countable K}
:= mapset (gmap K).
(* stdpp/gmap.v *)
(* Lift instances of operational TCs from [mapset] and mark them [simpl never]. *)
Instance gset_elem_of: ElemOf K (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_empty : Empty (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_singleton : Singleton K (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_union: Union (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_intersection: Intersection (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_difference: Difference (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_elements: Elements K (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_eq_dec : EqDecision (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_countable : Countable (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_equiv_dec : RelDecision (≡@{gset K}) | 1
:= _.
(* stdpp/gmap.v *)
Instance gset_elem_of_dec : RelDecision (∈@{gset K}) | 1
:= _.
(* stdpp/gmap.v *)
Instance gset_disjoint_dec : RelDecision (##@{gset K})
:= _.
(* stdpp/gmap.v *)
Instance gset_subseteq_dec : RelDecision (⊆@{gset K})
:= _.
(* stdpp/gmap.v *)
(* We put in an eta expansion to avoid [injection] from unfolding equalities
  like [dom (gset _) m1 = dom (gset _) m2]. *)
Instance gset_dom {A} : Dom (gmap K A) (gset K)
:= λ m,
    let '(GMap mt) := m in mapset_dom (GMap mt).
(* stdpp/gmap.v *)
(* Lift instances of other TCs. *)
Instance gset_leibniz : LeibnizEquiv (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_semi_set : SemiSet K (gset K) | 1
:= _.
(* stdpp/gmap.v *)
Instance gset_set : Set_ K (gset K) | 1
:= _.
(* stdpp/gmap.v *)
Instance gset_fin_set : FinSet K (gset K)
:= _.
(* stdpp/gmap.v *)
Instance gset_dom_spec : FinMapDom K (gmap K) (gset K).
Proof.
    pose proof (mapset_dom_spec (M:=gmap K)) as [?? Hdom]; split; auto.
    intros A m. specialize (Hdom A m). by destruct m.
  Qed.
(* stdpp/gmap.v *)
(* The function [gset_to_gmap x X] converts a set [X] to a map with domain
  [X] where each key has value [x]. Compared to the generic conversion
  [set_to_map], the function [gset_to_gmap] has [O(n)] instead of [O(n log n)]
  complexity and has an easier and better developed theory. *)
Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A
:=
    (λ _, x) <$> mapset_car X.
(* stdpp/gmap.v *)
Lemma lookup_gset_to_gmap {A} (x : A) (X : gset K) i :
    gset_to_gmap x X !! i = (guard (i ∈ X);; Some x).
Proof.
    destruct X as [X].
    unfold gset_to_gmap, gset_elem_of, elem_of, mapset_elem_of; simpl.
    rewrite lookup_fmap.
    case_guard; destruct (X !! i) as [[]|]; naive_solver.
  Qed.
(* stdpp/gmap.v *)
Lemma lookup_gset_to_gmap_Some {A} (x : A) (X : gset K) i y :
    gset_to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
(* stdpp/gmap.v *)
Lemma lookup_gset_to_gmap_None {A} (x : A) (X : gset K) i :
    gset_to_gmap x X !! i = None ↔ i ∉ X.
Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
(* stdpp/gmap.v *)
Lemma gset_to_gmap_empty {A} (x : A) : gset_to_gmap x ∅ = ∅.
Proof. apply fmap_empty. Qed.
(* stdpp/gmap.v *)
Lemma gset_to_gmap_union_singleton {A} (x : A) i Y :
    gset_to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(gset_to_gmap x Y).
Proof.
    apply map_eq; intros j; apply option_eq; intros y.
    rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
      elem_of_singleton; destruct (decide (i = j)); intuition.
  Qed.
(* stdpp/gmap.v *)
Lemma gset_to_gmap_singleton {A} (x : A) i :
    gset_to_gmap x {[ i ]} = {[i:=x]}.
Proof.
    rewrite <-(right_id_L ∅ (∪) {[ i ]}), gset_to_gmap_union_singleton.
    by rewrite gset_to_gmap_empty.
  Qed.
(* stdpp/gmap.v *)
Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y :
    gset_to_gmap x (Y ∖ {[i]}) = delete i (gset_to_gmap x Y).
Proof.
    apply map_eq; intros j; apply option_eq; intros y.
    rewrite lookup_delete_Some, !lookup_gset_to_gmap_Some, elem_of_difference,
      elem_of_singleton; destruct (decide (i = j)); intuition.
  Qed.
(* stdpp/gmap.v *)
Lemma fmap_gset_to_gmap {A B} (f : A → B) (X : gset K) (x : A) :
    f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
Proof.
    apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap.
    by simplify_option_eq.
  Qed.
(* stdpp/gmap.v *)
Lemma gset_to_gmap_dom {A B} (m : gmap K A) (y : B) :
    gset_to_gmap y (dom m) = const y <$> m.
Proof.
    apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap.
    destruct (m !! j) as [x|] eqn:?.
    - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
    - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
  Qed.
(* stdpp/gmap.v *)
Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
    dom (gset_to_gmap x X) = X.
Proof.
    induction X as [| y X not_in IH] using set_ind_L.
    - rewrite gset_to_gmap_empty, dom_empty_L; done.
    - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
  Qed.
(* stdpp/gmap.v *)
Lemma gset_to_gmap_set_to_map {A} (X : gset K) (x : A) :
    gset_to_gmap x X = set_to_map (λ _, x) X.
Proof.
    apply map_eq; intros k. by rewrite lookup_gset_to_gmap, lookup_set_to_map.
  Qed.
(* stdpp/gmap.v *)
Lemma map_to_list_gset_to_gmap {A} (X : gset K) (x : A) :
    map_to_list (gset_to_gmap x X) ≡ₚ (., x) <$> elements X.
Proof.
    induction X as [| y X not_in IH] using set_ind_L.
    - rewrite gset_to_gmap_empty, elements_empty, map_to_list_empty. done.
    - rewrite gset_to_gmap_union_singleton, elements_union_singleton by done.
      rewrite map_to_list_insert.
      2:{ rewrite lookup_gset_to_gmap_None. done. }
      rewrite IH. done.
  Qed.
(* stdpp/gmap.v *)
Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B))
:=
    λ X Y, set_bind (λ e1, set_map (e1,.) Y) X.
(* stdpp/gmap.v *)
Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :
    x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
Proof. unfold cprod, gset_cprod. destruct x. set_solver. Qed.
(* stdpp/gmap.v *)
Instance set_unfold_gset_cprod (X : gset A) (Y : gset B) x (P : Prop) Q :
    SetUnfoldElemOf x.1 X P → SetUnfoldElemOf x.2 Y Q →
    SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
Proof using.
    intros ??; constructor.
    by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 X P),
      (set_unfold_elem_of x.2 Y Q).
  Qed.
(* stdpp/gmultiset.v *)
(* 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 }.
(* stdpp/gmultiset.v *)
Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Proof. solve_decision. Defined.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Definition multiplicity (x : A) (X : gmultiset A) : nat
:=
    match gmultiset_car X !! x with Some n => Pos.to_nat n | None => 0 end.
(* stdpp/gmultiset.v *)
Instance gmultiset_elem_of : ElemOf A (gmultiset A)
:= λ x X,
    0 < multiplicity x X.
(* stdpp/gmultiset.v *)
Instance gmultiset_subseteq : SubsetEq (gmultiset A)
:= λ X Y, ∀ x,
    multiplicity x X ≤ multiplicity x Y.
(* stdpp/gmultiset.v *)
Instance gmultiset_equiv : Equiv (gmultiset A)
:= λ X Y, ∀ x,
    multiplicity x X = multiplicity x Y.
(* stdpp/gmultiset.v *)
Instance gmultiset_elements : Elements A (gmultiset A)
:=
    λ '(GMultiSet X),
      '(x,n) ← map_to_list X; replicate (Pos.to_nat n) x.
(* stdpp/gmultiset.v *)
Instance gmultiset_size : Size (gmultiset A)
:= length ∘ elements.
(* stdpp/gmultiset.v *)
Instance gmultiset_empty : Empty (gmultiset A)
:= GMultiSet ∅.
(* stdpp/gmultiset.v *)
Instance gmultiset_singleton : SingletonMS A (gmultiset A)
:= λ x,
    GMultiSet {[ x := 1%positive ]}.
(* stdpp/gmultiset.v *)
Instance gmultiset_union : Union (gmultiset A)
:=
    λ '(GMultiSet X) '(GMultiSet Y),
      GMultiSet $ union_with (λ x y, Some (x `max` y)%positive) X Y.
(* stdpp/gmultiset.v *)
Instance gmultiset_intersection : Intersection (gmultiset A)
:=
    λ '(GMultiSet X) '(GMultiSet Y),
      GMultiSet $ intersection_with (λ x y, Some (x `min` y)%positive) X Y.
(* stdpp/gmultiset.v *)
(* Often called the "sum" *)
Instance gmultiset_disj_union : DisjUnion (gmultiset A)
:=
    λ '(GMultiSet X) '(GMultiSet Y),
      GMultiSet $ union_with (λ x y, Some (x + y)%positive) X Y.
(* stdpp/gmultiset.v *)
Instance gmultiset_difference : Difference (gmultiset A)
:=
    λ '(GMultiSet X) '(GMultiSet Y),
      GMultiSet $ difference_with (λ x y,
        guard (y < x)%positive;; Some (x - y)%positive) X Y.
(* stdpp/gmultiset.v *)
Instance gmultiset_scalar_mul : ScalarMul nat (gmultiset A)
:=
    λ n '(GMultiSet X), GMultiSet $
      match n with 0 => ∅ | _ => fmap (λ m, m * Pos.of_nat n)%positive X end.
(* stdpp/gmultiset.v *)
Instance gmultiset_dom : Dom (gmultiset A) (gset A)
:=
    λ '(GMultiSet X), dom X.
(* stdpp/gmultiset.v *)
Definition gmultiset_map `{Countable B} (f : A → B) : gmultiset A → gmultiset B
:=
    λ '(GMultiSet X),
      GMultiSet $ map_fold
        (λ x n, partial_alter (Some ∘ from_option (Pos.add n) n) (f x))
        ∅
        X.
(* stdpp/gmultiset.v *)
Instance gmultiset_filter : Filter A (gmultiset A)
:=
    λ P _ '(GMultiSet X), GMultiSet (filter (P ∘ fst) X).
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_equiv_equivalence : Equivalence (≡@{gmultiset A}).
Proof. constructor; repeat intro; naive_solver. Qed.
(* stdpp/gmultiset.v *)
(* Multiplicity *)
Lemma multiplicity_empty x : multiplicity x ∅ = 0.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Lemma multiplicity_singleton_eq x : multiplicity x {[+ x +]} = 1.
Proof. unfold multiplicity; simpl. by rewrite lookup_singleton_eq. Qed.
(* stdpp/gmultiset.v *)
Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[+ y +]} = 0.
Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
(* stdpp/gmultiset.v *)
Lemma multiplicity_singleton x y :
    multiplicity x {[+ y +]} = if decide (x = y) then 1 else 0.
Proof.
    destruct (decide _) as [->|].
    - by rewrite multiplicity_singleton_eq.
    - by rewrite multiplicity_singleton_ne.
  Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Lemma multiplicity_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
    multiplicity x (filter P X) = if decide (P x) then multiplicity x X else 0.
Proof.
    destruct X as [X]. unfold multiplicity; simpl.
    rewrite map_lookup_filter. destruct (X !! x); by simplify_option_eq.
  Qed.
(* stdpp/gmultiset.v *)
(* Set *)
Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elem_of_empty x : x ∈@{gmultiset A} ∅ ↔ False.
Proof. rewrite elem_of_multiplicity, multiplicity_empty. lia. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_union. lia. Qed.
(* stdpp/gmultiset.v *)
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.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elem_of_intersection X Y x : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_intersection. lia. Qed.