Merge branch 'robbert/big_op_commute' into 'master'

Lemmas for big ops commuting with updates

See merge request !305

CHANGELOG.md

@@ -164,6 +164,8 @@ Changes in Coq:
 * Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
   `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`,
   `cmra_morphism_core`.
+* Rename lemmas `fupd_big_sep{L,M,S,MS}` into `big_sep{L,M,S,MS}_fupd` to be
+  consistent with other such big op lemmas. Also add such lemmas for `bupd`.
 * Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
   rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
   `-d>`. The renaming can be automatically done using the following script (on

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Φ]".

theories/bi/big_op.v

 From iris.algebra Require Export big_op.
-From iris.bi Require Import derived_laws_sbi plainly.
+From iris.bi Require Import derived_laws_sbi.
 From stdpp Require Import countable fin_sets functions.
 Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
@@ -1448,46 +1448,6 @@ Section list.
   Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
     TCForall Timeless Ps → Timeless ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
-
-  Section plainly.
-    Context `{!BiPlainly PROP}.
-
-    Lemma big_sepL_plainly `{!BiAffine PROP} Φ l :
-      ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
-    Proof. apply (big_opL_commute _). Qed.
-
-    Global Instance big_sepL_nil_plain `{!BiAffine PROP} Φ :
-      Plain ([∗ list] k↦x ∈ [], Φ k x).
-    Proof. simpl; apply _. Qed.
-
-    Global Instance big_sepL_plain `{!BiAffine PROP} Φ l :
-      (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
-    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-
-    Lemma big_andL_plainly Φ l :
-      ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
-    Proof. apply (big_opL_commute _). Qed.
-
-    Global Instance big_andL_nil_plain Φ :
-      Plain ([∧ list] k↦x ∈ [], Φ k x).
-    Proof. simpl; apply _. Qed.
-
-    Global Instance big_andL_plain Φ l :
-      (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
-    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-
-    Lemma big_orL_plainly `{!BiPlainlyExist PROP} Φ l :
-      ■ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ [∨ list] k↦x ∈ l, ■ (Φ k x).
-    Proof. apply (big_opL_commute _). Qed.
-
-    Global Instance big_orL_nil_plain Φ :
-      Plain ([∨ list] k↦x ∈ [], Φ k x).
-    Proof. simpl; apply _. Qed.
-
-    Global Instance big_orL_plain Φ l :
-      (∀ k x, Plain (Φ k x)) → Plain ([∨ list] k↦x ∈ l, Φ k x).
-    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-  End plainly.
 End list.
 
 Section list2.
@@ -1522,24 +1482,6 @@ Section list2.
     (∀ k x1 x2, Timeless (Φ k x1 x2)) →
     Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
   Proof. rewrite big_sepL2_alt. apply _. Qed.
-
-  Section plainly.
-    Context `{!BiPlainly PROP}.
-
-    Lemma big_sepL2_plainly `{!BiAffine PROP} Φ l1 l2 :
-      ■ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
-      ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■ (Φ k y1 y2).
-    Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed.
-
-    Global Instance big_sepL2_nil_plain `{!BiAffine PROP} Φ :
-      Plain ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
-    Proof. simpl; apply _. Qed.
-
-    Global Instance big_sepL2_plain `{!BiAffine PROP} Φ l1 l2 :
-      (∀ k x1 x2, Plain (Φ k x1 x2)) →
-      Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
-    Proof. rewrite big_sepL2_alt. apply _. Qed.
-  End plainly.
 End list2.
 
 (** ** Big ops over finite maps *)
@@ -1568,21 +1510,6 @@ Section gmap.
   Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
-
-  Section plainly.
-    Context `{!BiPlainly PROP}.
-
-    Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
-      ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
-    Proof. apply (big_opM_commute _). Qed.
-
-    Global Instance big_sepM_empty_plain `{BiAffine PROP} Φ :
-      Plain ([∗ map] k↦x ∈ ∅, Φ k x).
-    Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
-    Global Instance big_sepM_plain `{BiAffine PROP} Φ m :
-      (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x  ∈ m, Φ k x).
-    Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
-  End plainly.
 End gmap.
 
 Section gmap2.
@@ -1621,23 +1548,6 @@ Section gmap2.
     (∀ k x1 x2, Timeless (Φ k x1 x2)) →
     Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
   Proof. intros. rewrite /big_sepM2. apply _. Qed.
-
-  Section plainly.
-    Context `{!BiPlainly PROP}.
-
-    Lemma big_sepM2_plainly `{BiAffine PROP} Φ m1 m2 :
-      ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢
-      [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
-    Proof. by rewrite /big_sepM2 plainly_and plainly_pure big_sepM_plainly. Qed.
-
-    Global Instance big_sepM2_empty_plain `{BiAffine PROP} Φ :
-      Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
-    Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
-    Global Instance big_sepM2_plain `{BiAffine PROP} Φ m1 m2 :
-      (∀ k x1 x2, Plain (Φ k x1 x2)) →
-      Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
-    Proof. intros. rewrite /big_sepM2. apply _. Qed.
-  End plainly.
 End gmap2.
 
 (** ** Big ops over finite sets *)
@@ -1666,20 +1576,6 @@ Section gset.
   Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
-
-  Section plainly.
-    Context `{!BiPlainly PROP}.
-
-    Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
-      ■ ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■ (Φ y).
-    Proof. apply (big_opS_commute _). Qed.
-
-    Global Instance big_sepS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ set] x ∈ ∅, Φ x).
-    Proof. rewrite /big_opS elements_empty. apply _. Qed.
-    Global Instance big_sepS_plain `{BiAffine PROP} Φ X :
-      (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
-    Proof. rewrite /big_opS. apply _. Qed.
-  End plainly.
 End gset.
 
 (** ** Big ops over finite multisets *)
@@ -1708,19 +1604,5 @@ Section gmultiset.
   Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
-
-  Section plainly.
-    Context `{!BiPlainly PROP}.
-
-    Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
-      ■ ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■ (Φ y).
-    Proof. apply (big_opMS_commute _). Qed.
-
-    Global Instance big_sepMS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ mset] x ∈ ∅, Φ x).
-    Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
-    Global Instance big_sepMS_plain `{BiAffine PROP} Φ X :
-      (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
-    Proof. rewrite /big_opMS. apply _. Qed.
-  End plainly.
 End gmultiset.
 End sbi_big_op.

theories/bi/plainly.v

-From iris.bi Require Import derived_laws_sbi.
+From iris.bi Require Import derived_laws_sbi big_op.
 From iris.algebra Require Import monoid.
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
@@ -373,38 +373,61 @@ Proof.
   - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
 Qed.
 
-(* Instances for big operators *)
-Global Instance plainly_and_homomorphism :
-  MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
-Proof.
-  split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
-Qed.
-
-Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
-  MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
-Proof.
-  split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
-Qed.
+Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
+  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
+Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
+(* Instances for big operators *)
 Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
 Proof. split; try apply _. apply plainly_sep. Qed.
-
-Global Instance plainly_sep_homomorphism `{BiAffine PROP} :
-  MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
-Proof. split. apply _. apply plainly_emp. Qed.
-
 Global Instance plainly_sep_entails_weak_homomorphism :
   WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
 Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.
-
 Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
 Proof. split. apply _. simpl. rewrite plainly_emp. done. Qed.
 
-Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
-  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
-Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+Global Instance plainly_sep_homomorphism `{BiAffine PROP} :
+  MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
+Proof. split. apply _. apply plainly_emp. Qed.
+Global Instance plainly_and_homomorphism :
+  MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
+Proof. split; [split|]; try apply _. apply plainly_and. apply plainly_pure. Qed.
+Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
+  MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
+Proof. split; [split|]; try apply _. apply plainly_or. apply plainly_pure. Qed.
+
+Lemma big_sepL_plainly `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
+  ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
+Proof. apply (big_opL_commute _). Qed.
+Lemma big_andL_plainly {A} (Φ : nat → A → PROP) l :
+  ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
+Proof. apply (big_opL_commute _). Qed.
+Lemma big_orL_plainly `{!BiPlainlyExist PROP} {A} (Φ : nat → A → PROP) l :
+  ■ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ [∨ list] k↦x ∈ l, ■ (Φ k x).
+Proof. apply (big_opL_commute _). Qed.
+
+Lemma big_sepL2_plainly `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) l1 l2 :
+  ■ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
+  ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■ (Φ k y1 y2).
+Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed.
+
+Lemma big_sepM_plainly `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
+  ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
+Proof. apply (big_opM_commute _). Qed.
+
+Lemma big_sepM2_plainly `{BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
+  ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢ [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
+Proof. by rewrite /big_sepM2 plainly_and plainly_pure big_sepM_plainly. Qed.
+
+Lemma big_sepS_plainly `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+  ■ ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■ (Φ y).
+Proof. apply (big_opS_commute _). Qed.
+
+Lemma big_sepMS_plainly `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+  ■ ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■ (Φ y).
+Proof. apply (big_opMS_commute _). Qed.
 
 (* Plainness instances *)
 Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
@@ -458,6 +481,64 @@ Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+Global Instance big_sepL_nil_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) :
+  Plain ([∗ list] k↦x ∈ [], Φ k x).
+Proof. simpl; apply _. Qed.
+Global Instance big_sepL_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
+  (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
+Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+Global Instance big_andL_nil_plain {A} (Φ : nat → A → PROP) :
+  Plain ([∧ list] k↦x ∈ [], Φ k x).
+Proof. simpl; apply _. Qed.
+Global Instance big_andL_plain {A} (Φ : nat → A → PROP) l :
+  (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
+Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+Global Instance big_orL_nil_plain {A} (Φ : nat → A → PROP) :
+  Plain ([∨ list] k↦x ∈ [], Φ k x).
+Proof. simpl; apply _. Qed.
+Global Instance big_orL_plain {A} (Φ : nat → A → PROP) l :
+  (∀ k x, Plain (Φ k x)) → Plain ([∨ list] k↦x ∈ l, Φ k x).
+Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
+Global Instance big_sepL2_nil_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) :
+  Plain ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+Proof. simpl; apply _. Qed.
+Global Instance big_sepL2_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) l1 l2 :
+  (∀ k x1 x2, Plain (Φ k x1 x2)) →
+  Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+Proof. rewrite big_sepL2_alt. apply _. Qed.
+
+Global Instance big_sepM_empty_plain `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) :
+  Plain ([∗ map] k↦x ∈ ∅, Φ k x).
+Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+Global Instance big_sepM_plain `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
+  (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x  ∈ m, Φ k x).
+Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
+
+Global Instance big_sepM2_empty_plain `{BiAffine PROP, Countable K}
+    {A B} (Φ : K → A → B → PROP) :
+  Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
+Global Instance big_sepM2_plain `{BiAffine PROP, Countable K}
+    {A B} (Φ : K → A → B → PROP) m1 m2 :
+  (∀ k x1 x2, Plain (Φ k x1 x2)) →
+  Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+Proof. intros. rewrite /big_sepM2. apply _. Qed.
+
+Global Instance big_sepS_empty_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) :
+  Plain ([∗ set] x ∈ ∅, Φ x).
+Proof. rewrite /big_opS elements_empty. apply _. Qed.
+Global Instance big_sepS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+  (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
+Proof. rewrite /big_opS. apply _. Qed.
+
+Global Instance big_sepMS_empty_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) :
+  Plain ([∗ mset] x ∈ ∅, Φ x).
+Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
+Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+  (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
+Proof. rewrite /big_opMS. apply _. Qed.
+
 (* Interaction with equality *)
 Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
 Proof.

theories/bi/updates.v

@@ -163,6 +163,23 @@ Section bupd_derived.
   Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
   Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q.
   Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
+
+  Global Instance bupd_homomorphism :
+    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (bupd (PROP:=PROP)).
+  Proof. split; [split|]; try apply _. apply bupd_sep. apply bupd_intro. Qed.
+
+  Lemma big_sepL_bupd {A} (Φ : nat → A → PROP) l :
+    ([∗ list] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ list] k↦x ∈ l, Φ k x.
+  Proof. by rewrite (big_opL_commute _). Qed.
+  Lemma big_sepM_bupd {A} `{Countable K} (Φ : K → A → PROP) l :
+    ([∗ map] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ map] k↦x ∈ l, Φ k x.
+  Proof. by rewrite (big_opM_commute _). Qed.
+  Lemma big_sepS_bupd `{Countable A} (Φ : A → PROP) l :
+    ([∗ set]  x ∈ l, |==> Φ x) ⊢ |==> [∗ set] x ∈ l, Φ x.
+  Proof. by rewrite (big_opS_commute _). Qed.
+  Lemma big_sepMS_bupd `{Countable A} (Φ : A → PROP) l :
+    ([∗ mset] x ∈ l, |==> Φ x) ⊢ |==> [∗ mset] x ∈ l, Φ x.
+  Proof. by rewrite (big_opMS_commute _). Qed.
 End bupd_derived.
 
 Section bupd_derived_sbi.
@@ -291,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.