From 144a07ef95efcaae91c10ab757871319d7d8739d Mon Sep 17 00:00:00 2001
From: Marijn van Wezel <marijn.vanwezel@ru.nl>
Date: Thu, 5 Dec 2024 19:45:15 +0000
Subject: [PATCH] Add `gmultiset_disj_union_list`

---
 CHANGELOG.md      |  6 +++++-
 stdpp/base.v      |  5 +++++
 stdpp/gmultiset.v | 41 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 51 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 795c1cea..1692183f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,11 @@
 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
-## 1.11.0 (2024-10-30)
+## std++ master
+
+- Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel)
+
+## std++ 1.11.0 (2024-10-30)
 
 The highlights of this release include:
 * support for building with dune
diff --git a/stdpp/base.v b/stdpp/base.v
index 2a574119..9542a271 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1122,6 +1122,11 @@ Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
 Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
 Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
+Definition disj_union_list `{Empty A} `{DisjUnion A} : list A → A := fold_right (⊎) ∅.
+Global Arguments disj_union_list _ _ _ !_ / : assert.
+(* There is no "big" version of [⊎] in unicode, we thus use [⋃+]. *)
+Notation "⋃+ l" := (disj_union_list l) (at level 20, format "⋃+  l") : stdpp_scope.
+
 Class SingletonMS A B := singletonMS: A → B.
 Global Hint Mode SingletonMS - ! : typeclass_instances.
 Global Instance: Params (@singletonMS) 3 := {}.
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 365d51cb..2d10fb40 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -862,3 +862,44 @@ Section map.
     intros ? [HX]; constructor. by rewrite multiplicity_gmultiset_map, HX.
   Qed.
 End map.
+
+(** * Big disjoint unions *)
+Section disj_union_list.
+  Context `{Countable A}.
+  Implicit Types X Y : gmultiset A.
+  Implicit Types Xs Ys : list (gmultiset A).
+
+  Lemma gmultiset_disj_union_list_nil :
+    ⋃+ (@nil (gmultiset A)) = ∅.
+  Proof. done. Qed.
+
+  Lemma gmultiset_disj_union_list_cons X Xs :
+    ⋃+ (X :: Xs) = X ⊎ ⋃+ Xs.
+  Proof. done. Qed.
+
+  Lemma gmultiset_disj_union_list_singleton X :
+    ⋃+ [X] = X.
+  Proof. simpl. by rewrite (right_id_L ∅ _). Qed.
+
+  Lemma gmultiset_disj_union_list_app Xs1 Xs2 :
+    ⋃+ (Xs1 ++ Xs2) = ⋃+ Xs1 ⊎ ⋃+ Xs2.
+  Proof.
+    induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id_L ∅ _)|].
+    by rewrite IH, (assoc_L _).
+  Qed.
+
+  Lemma elem_of_gmultiset_disj_union_list Xs x :
+    x ∈ ⋃+ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
+  Proof. induction Xs; multiset_solver. Qed.
+
+  Lemma multiplicity_gmultiset_disj_union_list x Xs :
+    multiplicity x (⋃+ Xs) = sum_list (multiplicity x <$> Xs).
+  Proof.
+    induction Xs as [|X Xs IH]; [done|]; simpl.
+    by rewrite multiplicity_disj_union, IH.
+  Qed.
+
+  Global Instance gmultiset_disj_union_list_proper :
+    Proper ((≡ₚ) ==> (=)) (@disj_union_list (gmultiset A) _ _).
+  Proof. induction 1; multiset_solver. Qed.
+End disj_union_list.
-- 
GitLab