From 5db505ac2659dd6f6692874002e70575b2449b40 Mon Sep 17 00:00:00 2001
From: marijnvanwezel <marijnvanwezel@gmail.com>
Date: Wed, 12 Mar 2025 22:40:20 +0100
Subject: [PATCH 1/2] Add `SetUnfoldElemOf` instance of `dom` on `gmultiset`

---
 stdpp/gmultiset.v | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 2d10fb40..3b840459 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -159,6 +159,13 @@ Section basic_lemmas.
 
   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_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.
 End basic_lemmas.
 
 (** * A solver for multisets *)
@@ -299,6 +306,9 @@ Section multiset_unfold.
     intros ??; constructor. rewrite gmultiset_elem_of_intersection.
     by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
   Qed.
+  Global Instance set_unfold_gmultiset_dom x X :
+    SetUnfoldElemOf x (dom X) (x ∈ X).
+  Proof. constructor. apply gmultiset_elem_of_dom. Qed.
 End multiset_unfold.
 
 (** Step 3: instantiate hypotheses *)
@@ -554,12 +564,6 @@ Section more_lemmas.
       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 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) :
-- 
GitLab


From 713ad87c6d53d01912c0a44b87c0553323f895f2 Mon Sep 17 00:00:00 2001
From: marijnvanwezel <marijnvanwezel@gmail.com>
Date: Wed, 12 Mar 2025 23:13:35 +0100
Subject: [PATCH 2/2] Add test and update CHANGELOG

---
 CHANGELOG.md            | 1 +
 tests/multiset_solver.v | 3 +++
 2 files changed, 4 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 516c417e..1d6391d9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,7 @@ API-breaking change is listed.
   `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
   `StronglySorted_app_inv_l` → `StronglySorted_app_1_l`
   `StronglySorted_app_inv_r` → `StronglySorted_app_1_r`. (by Marijn van Wezel)
+- Add `SetUnfoldElemOf` instance for `dom` on `gmultiset`. (by Marijn van Wezel)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 0f0e4bee..2b3db9e0 100644
--- a/tests/multiset_solver.v
+++ b/tests/multiset_solver.v
@@ -58,6 +58,9 @@ Section test.
   Lemma test_elem_of_6 x y X : {[+ x; y +]} ⊆ X → x ∈ X ∧ y ∈ X.
   Proof. multiset_solver. Qed.
 
+  Lemma test_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
+  Proof. multiset_solver. Qed.
+
   (** Tests where the goals do not involve the multiset connectives *)
   Lemma test_goal_1 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → x = y.
   Proof. multiset_solver. Qed.
-- 
GitLab