From a42a35707b1a639093d5647b63de4df756b0b845 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 12 Jan 2021 18:49:58 +0100
Subject: [PATCH] add some big_opS lemmas

---
 iris/algebra/big_op.v | 30 +++++++++++++++++++++++++++++-
 iris/bi/big_op.v      |  5 +++++
 2 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 892e13a6e..91571f38b 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -394,7 +394,6 @@ Section gmap.
   Qed.
 End gmap.
 
-
 (** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.
@@ -480,8 +479,37 @@ Section gset.
   Lemma big_opS_op f g X :
     ([^o set] y ∈ X, f y `o` g y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ X, g y).
   Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
+
+  Lemma big_opS_list_to_set f (l : list A) :
+    NoDup l →
+    ([^o set] x ∈ list_to_set l, f x) ≡ [^o list] _ ↦ x ∈ l, f x.
+  Proof.
+    induction l as [|x l]; intros Hnodup.
+    - rewrite big_opS_empty //.
+    - inversion Hnodup; subst; clear Hnodup.
+      rewrite /= big_opS_union; last first.
+      { rewrite disjoint_singleton_l.
+        rewrite elem_of_list_to_set //. }
+      rewrite big_opS_singleton.
+      f_equiv. apply IHl; auto.
+  Qed.
 End gset.
 
+Lemma big_opS_set_map `{Countable A, Countable B} (h : A → B) (X : gset A) (f : B → M) :
+  Inj (=) (=) h →
+  ([^o set] x ∈ set_map h X, f x) ≡ ([^o set] x ∈ X, f (h x)).
+Proof.
+  intros Hinj.
+  induction X as [|x X ? IH] using set_ind_L => //=; [ by rewrite big_opS_eq | ].
+  replace (set_map h ({[x]} ∪ X)) with ({[h x]} ∪ (set_map h X) : gset B) by set_solver.
+  rewrite !big_opS_union.
+  - rewrite !big_opS_singleton IH //.
+  - set_solver.
+  - cut ((h x) ∉ (set_map h X : gset _)); first by set_solver.
+    intros (x'&Heq&Hin)%elem_of_map.
+    apply Hinj in Heq. subst. auto.
+Qed.
+
 Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
   ([^o map] k↦_ ∈ m, f k) ≡ ([^o set] k ∈ dom _ m, f k).
 Proof.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 357ef5d1d..9d8d75198 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1631,6 +1631,11 @@ Section gset.
       (([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) -∗ [∗ set] y ∈ X, Φ y).
   Proof. intros. setoid_rewrite <-decide_emp. by apply big_sepS_filter_acc'. Qed.
 
+  Lemma big_sepS_list_to_set Φ (l : list A) :
+    NoDup l →
+    ([∗ set] x ∈ list_to_set l, Φ x) ⊣⊢ [∗ list] _ ↦ x ∈ l, Φ x.
+  Proof. apply big_opS_list_to_set. Qed.
+
   Lemma big_sepS_sep Φ Ψ X :
     ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y).
   Proof. apply big_opS_op. Qed.
-- 
GitLab