From efe73fee69e3aaac549a6a320f70839fc3703f9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= <leo.lveb@gmail.com>
Date: Fri, 11 Mar 2022 10:05:54 +0100
Subject: [PATCH] Add lemmas elem_of_list_to_set_disj and
 gmultiset_difference_disj_union_{l,r}

---
 theories/gmultiset.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index f6a8a171..a4960ac2 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -397,6 +397,14 @@ Section more_lemmas.
   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 as [|?? IH]; [set_solver|split].
+    - intros [->%gmultiset_elem_of_singleton| Hin]%gmultiset_elem_of_disj_union;
+        [set_solver|by right; apply IH].
+    - intros [-> |]%elem_of_cons; rewrite ?list_to_set_disj_cons; multiset_solver.
+  Qed.
   Global Instance list_to_set_disj_perm :
     Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
   Proof. induction 1; multiset_solver. Qed.
@@ -603,6 +611,12 @@ Section more_lemmas.
   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.
-- 
GitLab