Generalize commuting lemmas to `algebra.big_op` and add all variants.

iris/algebra/big_op.v

@@ -337,6 +337,12 @@ Section gmap.
            (big_opM o (K:=K) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opM_proper; intros; apply Hf. Qed.
 
+  (* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
+  [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
+  Lemma big_opM_map_to_list f m :
+    ([^o map] k↦x ∈ m, f k x) ≡ [^o list] xk ∈ map_to_list m, f (xk.1) (xk.2).
+  Proof. rewrite big_opM_eq. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
+
   Lemma big_opM_singleton f i x : ([^o map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
   Proof.
     rewrite -insert_empty big_opM_insert/=; last eauto using lookup_empty.
@@ -492,12 +498,14 @@ Section gset.
     Proper (pointwise_relation _ (≡) ==> (=) ==> (≡)) (big_opS o (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opS_proper; intros; apply Hf. Qed.
 
+  (* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
+  [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
   Lemma big_opS_elements f X :
-    ([^o set] x ∈ X, f x) = [^o list] _↦x ∈ elements X, f x.
+    ([^o set] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
   Proof. by rewrite big_opS_eq. Qed.
 
   Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
-  Proof. by rewrite big_opS_elements elements_empty. Qed.
+  Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
 
   Lemma big_opS_insert f X x :
     x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x `o` [^o set] y ∈ X, f y).
@@ -627,6 +635,12 @@ Section gmultiset.
     Proper (pointwise_relation _ (≡) ==> (=) ==> (≡)) (big_opMS o (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opMS_proper; intros; apply Hf. Qed.
 
+  (* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
+  [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
+  Lemma big_opMS_elements f X :
+    ([^o mset] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
+  Proof. by rewrite big_opMS_eq. Qed.
+
   Lemma big_opMS_empty f : ([^o mset] x ∈ ∅, f x) = monoid_unit.
   Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
 
@@ -660,6 +674,71 @@ Section gmultiset.
     ([^o mset] y ∈ X, f y `o` g y) ≡ ([^o mset] y ∈ X, f y) `o` ([^o mset] y ∈ X, g y).
   Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
 End gmultiset.
+
+(** Commuting lemmas *)
+Lemma big_opL_opL {A B} (f : nat → A → nat → B → M) (l1 : list A) (l2 : list B) :
+  ([^o list] k1↦x1 ∈ l1, [^o list] k2↦x2 ∈ l2, f k1 x1 k2 x2) ≡
+  ([^o list] k2↦x2 ∈ l2, [^o list] k1↦x1 ∈ l1, f k1 x1 k2 x2).
+Proof.
+  revert f l2. induction l1 as [|x1 l1 IH]; simpl; intros Φ l2.
+  { by rewrite big_opL_unit. }
+  by rewrite IH big_opL_op.
+Qed.
+Lemma big_opL_opM {A} `{Countable K} {B}
+    (f : nat → A → K → B → M) (l1 : list A) (m2 : gmap K B) :
+  ([^o list] k1↦x1 ∈ l1, [^o map] k2↦x2 ∈ m2, f k1 x1 k2 x2) ≡
+  ([^o map] k2↦x2 ∈ m2, [^o list] k1↦x1 ∈ l1, f k1 x1 k2 x2).
+Proof. repeat setoid_rewrite big_opM_map_to_list. by rewrite big_opL_opL. Qed.
+Lemma big_opL_opS {A} `{Countable B}
+    (f : nat → A → B → M) (l1 : list A) (X2 : gset B) :
+  ([^o list] k1↦x1 ∈ l1, [^o set] x2 ∈ X2, f k1 x1 x2) ≡
+  ([^o set] x2 ∈ X2, [^o list] k1↦x1 ∈ l1, f k1 x1 x2).
+Proof. repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL. Qed.
+Lemma big_opL_opMS {A} `{Countable B}
+    (f : nat → A → B → M) (l1 : list A) (X2 : gmultiset B) :
+  ([^o list] k1↦x1 ∈ l1, [^o mset] x2 ∈ X2, f k1 x1 x2) ≡
+  ([^o mset] x2 ∈ X2, [^o list] k1↦x1 ∈ l1, f k1 x1 x2).
+Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
+
+Lemma big_opM_opM `{Countable K1} {A} `{Countable K2} {B}
+    (f : K1 → A → K2 → B → M) (m1 : gmap K1 A) (m2 : gmap K2 B) :
+  ([^o map] k1↦x1 ∈ m1, [^o map] k2↦x2 ∈ m2, f k1 x1 k2 x2) ≡
+  ([^o map] k2↦x2 ∈ m2, [^o map] k1↦x1 ∈ m1, f k1 x1 k2 x2).
+Proof. repeat setoid_rewrite big_opM_map_to_list. by rewrite big_opL_opL. Qed.
+Lemma big_opM_opS `{Countable K} {A} `{Countable B}
+    (f : K → A → B → M) (m1 : gmap K A) (X2 : gset B) :
+  ([^o map] k1↦x1 ∈ m1, [^o set] x2 ∈ X2, f k1 x1 x2) ≡
+  ([^o set] x2 ∈ X2, [^o map] k1↦x1 ∈ m1, f k1 x1 x2).
+Proof.
+  repeat setoid_rewrite big_opM_map_to_list.
+  repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL.
+Qed.
+Lemma big_opM_opMS `{Countable K} {A} `{Countable B} (f : K → A → B → M)
+    (m1 : gmap K A) (X2 : gmultiset B) :
+  ([^o map] k1↦x1 ∈ m1, [^o mset] x2 ∈ X2, f k1 x1 x2) ≡
+  ([^o mset] x2 ∈ X2, [^o map] k1↦x1 ∈ m1, f k1 x1 x2).
+Proof.
+  repeat setoid_rewrite big_opM_map_to_list.
+  repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL.
+Qed.
+
+Lemma big_opS_opS `{Countable A, Countable B}
+    (X : gset A) (Y : gset B) (f : A → B → M) :
+  ([^o set] x ∈ X, [^o set] y ∈ Y, f x y) ≡ ([^o set] y ∈ Y, [^o set] x ∈ X, f x y).
+Proof. repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL. Qed.
+Lemma big_opS_opMS `{Countable A, Countable B}
+    (X : gset A) (Y : gmultiset B) (f : A → B → M) :
+  ([^o set] x ∈ X, [^o mset] y ∈ Y, f x y) ≡ ([^o mset] y ∈ Y, [^o set] x ∈ X, f x y).
+Proof.
+  repeat setoid_rewrite big_opS_elements.
+  repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL.
+Qed.
+
+Lemma big_opMS_opMS `{Countable A, Countable B}
+    (X : gmultiset A) (Y : gmultiset B) (f : A → B → M) :
+  ([^o mset] x ∈ X, [^o mset] y ∈ Y, f x y) ≡ ([^o mset] y ∈ Y, [^o mset] x ∈ X, f x y).
+Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
+
 End big_op.
 
 Section homomorphisms.

iris/bi/big_op.v

@@ -357,19 +357,6 @@ Section sep_list.
 End sep_list.
 
 (* Some lemmas depend on the generalized versions of the above ones. *)
-Lemma big_sepL_sepL {A B : Type} (Φ : nat → A → nat → B → PROP) (l1 : list A) (l2 : list B) :
-  ([∗ list] k1↦x1 ∈ l1, [∗ list] k2↦x2 ∈ l2, Φ k1 x1 k2 x2) ⊣⊢
-  ([∗ list] k2↦x2 ∈ l2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 k2 x2).
-Proof.
-  revert Φ l2. induction l1 as [|x1 l1 IH]; intros Φ l2.
-  { rewrite big_sepL_nil. setoid_rewrite big_sepL_nil.
-    rewrite big_sepL_emp. done. }
-  rewrite big_sepL_cons.
-  setoid_rewrite big_sepL_cons.
-  rewrite big_sepL_sep. f_equiv.
-  rewrite IH //.
-Qed.
-
 Lemma big_sepL_sep_zip_with {A B C} (f : A → B → C) (g1 : C → A) (g2 : C → B)
     (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
   (∀ x y, g1 (f x y) = x) →
@@ -2024,7 +2011,7 @@ Section gset.
   Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
 
   Lemma big_sepS_elements Φ X :
-    ([∗ set] x ∈ X, Φ x) ⊣⊢ [∗ list] _↦x ∈ elements X, Φ x.
+    ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ list] x ∈ elements X, Φ x).
   Proof. by rewrite big_opS_elements. Qed.
 
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
@@ -2249,14 +2236,6 @@ Section gset.
   Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
 End gset.
 
-Lemma big_sepS_sepS `{Countable A, Countable B}
-    (X : gset A) (Y : gset B) (Φ : A → B → PROP) :
-  ([∗ set] x ∈ X, [∗ set] y ∈ Y, Φ x y) ⊣⊢ ([∗ set] y ∈ Y, [∗ set] x ∈ X, Φ x y).
-Proof.
-  repeat setoid_rewrite big_sepS_elements.
-  rewrite big_sepL_sepL. done.
-Qed.
-
 Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
   ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom _ m, Φ k).
 Proof. apply big_opM_dom. Qed.
@@ -2471,4 +2450,56 @@ Section gmultiset.
     (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
 End gmultiset.
+
+(** Commuting lemmas *)
+Lemma big_sepL_sepL {A B} (Φ : nat → A → nat → B → PROP) (l1 : list A) (l2 : list B) :
+  ([∗ list] k1↦x1 ∈ l1, [∗ list] k2↦x2 ∈ l2, Φ k1 x1 k2 x2) ⊣⊢
+  ([∗ list] k2↦x2 ∈ l2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 k2 x2).
+Proof. apply big_opL_opL. Qed.
+Lemma big_sepL_sepM {A} `{Countable K} {B}
+    (Φ : nat → A → K → B → PROP) (l1 : list A) (m2 : gmap K B) :
+  ([∗ list] k1↦x1 ∈ l1, [∗ map] k2↦x2 ∈ m2, Φ k1 x1 k2 x2) ⊣⊢
+  ([∗ map] k2↦x2 ∈ m2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 k2 x2).
+Proof. apply big_opL_opM. Qed.
+Lemma big_sepL_sepS {A} `{Countable B}
+    (Φ : nat → A → B → PROP) (l1 : list A) (X2 : gset B) :
+  ([∗ list] k1↦x1 ∈ l1, [∗ set] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
+  ([∗ set] x2 ∈ X2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 x2).
+Proof. apply big_opL_opS. Qed.
+Lemma big_sepL_sepMS {A} `{Countable B}
+    (Φ : nat → A → B → PROP) (l1 : list A) (X2 : gmultiset B) :
+  ([∗ list] k1↦x1 ∈ l1, [∗ mset] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
+  ([∗ mset] x2 ∈ X2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 x2).
+Proof. apply big_opL_opMS. Qed.
+
+Lemma big_sepM_sepM `{Countable K1} {A} `{Countable K2} {B}
+    (Φ : K1 → A → K2 → B → PROP) (m1 : gmap K1 A) (m2 : gmap K2 B) :
+  ([∗ map] k1↦x1 ∈ m1, [∗ map] k2↦x2 ∈ m2, Φ k1 x1 k2 x2) ⊣⊢
+  ([∗ map] k2↦x2 ∈ m2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 k2 x2).
+Proof. apply big_opM_opM. Qed.
+Lemma big_sepM_sepS `{Countable K} {A} `{Countable B}
+    (Φ : K → A → B → PROP) (m1 : gmap K A) (X2 : gset B) :
+  ([∗ map] k1↦x1 ∈ m1, [∗ set] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
+  ([∗ set] x2 ∈ X2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 x2).
+Proof. apply big_opM_opS. Qed.
+Lemma big_sepM_sepMS `{Countable K} {A} `{Countable B} (Φ : K → A → B → PROP)
+    (m1 : gmap K A) (X2 : gmultiset B) :
+  ([∗ map] k1↦x1 ∈ m1, [∗ mset] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
+  ([∗ mset] x2 ∈ X2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 x2).
+Proof. apply big_opM_opMS. Qed.
+
+Lemma big_sepS_sepS `{Countable A, Countable B}
+    (X : gset A) (Y : gset B) (Φ : A → B → PROP) :
+  ([∗ set] x ∈ X, [∗ set] y ∈ Y, Φ x y) ⊣⊢ ([∗ set] y ∈ Y, [∗ set] x ∈ X, Φ x y).
+Proof. apply big_opS_opS. Qed.
+Lemma big_sepS_sepMS `{Countable A, Countable B}
+    (X : gset A) (Y : gmultiset B) (Φ : A → B → PROP) :
+  ([∗ set] x ∈ X, [∗ mset] y ∈ Y, Φ x y) ⊣⊢ ([∗ mset] y ∈ Y, [∗ set] x ∈ X, Φ x y).
+Proof. apply big_opS_opMS. Qed.
+
+Lemma big_sepMS_sepMS `{Countable A, Countable B}
+    (X : gmultiset A) (Y : gmultiset B) (Φ : A → B → PROP) :
+  ([∗ mset] x ∈ X, [∗ mset] y ∈ Y, Φ x y) ⊣⊢ ([∗ mset] y ∈ Y, [∗ mset] x ∈ X, Φ x y).
+Proof. apply big_opMS_opMS. Qed.
+
 End big_op.