Merge branch 'ralf/big_opM_singletons' into 'master'

add big_opM_singletons

See merge request iris/iris!567

theories/algebra/gmap.v

@@ -598,6 +598,22 @@ Proof.
   intros ??. rewrite !lookup_included=> Hm i.
   rewrite !lookup_fmap. by apply option_fmap_mono.
 Qed.
+
+Lemma big_opM_singletons m :
+  ([^op map] k ↦ x ∈ m, {[ k := x ]}) = m.
+Proof.
+  (* We are breaking the big_opM abstraction here. The reason is that [map_ind]
+     is too weak: we need an induction principle that visits all the keys in the
+     right order, namely the order in which they appear in map_to_list.  Here,
+     we achieve this by unfolding [big_opM] and doing induction over that list
+     instead. *)
+  rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
+  assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
+  revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
+  intros [??]%NoDup_cons. rewrite IH //.
+  rewrite insert_singleton_op ?not_elem_of_list_to_map_1 //.
+Qed.
+
 End properties.
 
 Section unital_properties.

theories/algebra/gmultiset.v

 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 *)
@@ -84,6 +84,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 _ {_ _}.

theories/algebra/gset.v

 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 _ {_ _}.