From c7f474c5f60248624f7bd89a6fb84bfce3f727ec Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Nov 2020 19:33:38 +0100
Subject: [PATCH] add _singletons lemmas for big_opMS and big_opS

---
 theories/algebra/gmultiset.v | 11 ++++++++++-
 theories/algebra/gset.v      | 11 ++++++++++-
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 701bb9d5a..b4b6f91ba 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -1,6 +1,6 @@
 From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
 (* The multiset union CMRA *)
@@ -81,6 +81,15 @@ Section gmultiset.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
     lia.
   Qed.
+
+  Lemma big_opMS_singletons X :
+    ([^op mset] x ∈ X, {[ x ]}) = X.
+  Proof.
+    induction X as [|x X IH] using gmultiset_ind.
+    - rewrite big_opMS_empty. done.
+    - unfold_leibniz. rewrite big_opMS_disj_union // big_opMS_singleton IH //.
+  Qed.
+
 End gmultiset.
 
 Arguments gmultisetO _ {_ _}.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index b3a5d578c..0807e7238 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,6 +1,6 @@
 From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
 (* The union CMRA *)
@@ -55,6 +55,15 @@ Section gset.
 
   Global Instance gset_core_id X : CoreId X.
   Proof. by apply core_id_total; rewrite gset_core_self. Qed.
+
+  Lemma big_opS_singletons X :
+    ([^op set] x ∈ X, {[ x ]}) = X.
+  Proof.
+    induction X as [|x X Hx IH] using set_ind_L.
+    - rewrite big_opS_empty. done.
+    - unfold_leibniz. rewrite big_opS_insert // IH //.
+  Qed.
+
 End gset.
 
 Arguments gsetO _ {_ _}.
-- 
GitLab