From 85697195e03ad41de8a4080f3b6a423059891e42 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Nov 2016 00:27:21 +0100
Subject: [PATCH] More big_opMS lemmas.

---
 algebra/cmra_big_op.v | 10 ++++++++++
 prelude/gmultiset.v   |  8 ++++++++
 2 files changed, 18 insertions(+)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 993c58ff5..f0aeaf985 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -452,6 +452,16 @@ Section gmultiset.
     intros. by rewrite /big_opMS gmultiset_elements_singleton /= right_id.
   Qed.
 
+  Lemma big_opMS_delete f X x :
+    x ∈ X → ([⋅ mset] y ∈ X, f y) ≡ f x ⋅ [⋅ mset] y ∈ X ∖ {[ x ]}, f y.
+  Proof.
+    intros ?%gmultiset_elem_of_subseteq. rewrite -big_opMS_singleton.
+    by rewrite -big_opMS_union -gmultiset_union_difference.
+  Qed.
+
+  Lemma big_opMS_elem_of f X x : x ∈ X → f x ≼ [⋅ mset] y ∈ X, f y.
+  Proof. intros. rewrite big_opMS_delete //. apply cmra_included_l. Qed.
+
   Lemma big_opMS_opS f g X :
     ([⋅ mset] y ∈ X, f y ⋅ g y) ≡ ([⋅ mset] y ∈ X, f y) ⋅ ([⋅ mset] y ∈ X, g y).
   Proof.
diff --git a/prelude/gmultiset.v b/prelude/gmultiset.v
index 67e2a4aab..9767b9a46 100644
--- a/prelude/gmultiset.v
+++ b/prelude/gmultiset.v
@@ -157,6 +157,14 @@ Proof.
   rewrite multiplicity_difference, multiplicity_empty; omega.
 Qed.
 
+(* Order stuff *)
+Lemma gmultiset_elem_of_subseteq x X : x ∈ X → {[ x ]} ⊆ X.
+Proof.
+  rewrite elem_of_multiplicity. intros Hx y; destruct (decide (x = y)) as [->|].
+  - rewrite multiplicity_singleton; omega.
+  - rewrite multiplicity_singleton_ne by done; omega.
+Qed.
+
 (* Properties of the elements operation *)
 Lemma gmultiset_elements_empty : elements (∅ : gmultiset A) = [].
 Proof.
-- 
GitLab