From b11b0f04502d273a7fdc16d6d9086e9a8c27d59a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Aug 2019 19:54:18 +0200
Subject: [PATCH] Refactor proofs for `|={E}=>` commuting with bigops, and make
 names consistent.

---
 theories/base_logic/lib/boxes.v |  4 ++--
 theories/bi/updates.v           | 29 ++++++++++++++---------------
 2 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 9d71aab4d..7de868396 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -210,7 +210,7 @@ Proof.
   iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
   iDestruct ("HeqP" with "HP") as "HP".
   iCombine "Hf" "HP" as "Hf".
-  rewrite -big_sepM_sep big_opM_fmap; iApply (fupd_big_sepM _ _ f).
+  rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
   iApply (@big_sepM_impl with "Hf").
   iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]".
@@ -227,7 +227,7 @@ Proof.
   iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
     [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' false) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
-  { rewrite -big_sepM_sep -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
+  { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
     iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.
     iInv N as (b) "[>Hγ HΦ]".
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 1a610b881..7679b2924 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -308,24 +308,23 @@ Section fupd_derived.
 
   Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
-  Lemma fupd_big_sepL {A} E (Φ : nat → A → PROP) (l : list A) :
+
+  Global Instance fupd_homomorphism E :
+    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (fupd (PROP:=PROP) E E).
+  Proof. split; [split|]; try apply _. apply fupd_sep. apply fupd_intro. Qed.
+
+  Lemma big_sepL_fupd {A} E (Φ : nat → A → PROP) l :
     ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ={E}=∗ [∗ list] k↦x ∈ l, Φ k x.
-  Proof.
-    apply (big_opL_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-  Qed.
-  Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → PROP) (m : gmap K A) :
+  Proof. by rewrite (big_opL_commute _). Qed.
+  Lemma big_sepM_fupd `{Countable K} {A} E (Φ : K → A → PROP) m :
     ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x.
-  Proof.
-    apply (big_opM_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-  Qed.
-  Lemma fupd_big_sepS `{Countable A} E (Φ : A → PROP) X :
+  Proof. by rewrite (big_opM_commute _). Qed.
+  Lemma big_sepS_fupd `{Countable A} E (Φ : A → PROP) X :
     ([∗ set] x ∈ X, |={E}=> Φ x) ={E}=∗ [∗ set] x ∈ X, Φ x.
-  Proof.
-    apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-  Qed.
+  Proof. by rewrite (big_opS_commute _). Qed.
+  Lemma big_sepMS_fupd `{Countable A} E (Φ : A → PROP) l :
+    ([∗ mset] x ∈ l, |={E}=> Φ x) ⊢ |={E}=> [∗ mset] x ∈ l, Φ x.
+  Proof. by rewrite (big_opMS_commute _). Qed.
 
   (** Fancy updates that take a step derived rules. *)
   Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2,E3}▷=> Q.
-- 
GitLab