Merge branch 'ralf/big-ops' into 'master'

Nested big-op lemmas

See merge request iris/iris!673

CHANGELOG.md

@@ -33,6 +33,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add new lemmas `big_sepM2_delete_l` and `big_sepM2_delete_r`.
 * Rename `big_sepM2_lookup_1` → `big_sepM2_lookup_l` and
   `big_sepM2_lookup_2` → `big_sepM2_lookup_r`.
+* Add lemmas for swapping nested big-ops: `big_sep{L,M,S,MS}_sep{L,M,S,MS}`.
 
 **Changes in `proofmode`:**
 

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,18 @@ 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.
+  Proof. by rewrite big_opS_eq. Qed.
+
   Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
   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).
-  Proof. intros. by rewrite big_opS_eq /big_opS_def elements_union_singleton. Qed.
+  Proof. intros. by rewrite !big_opS_elements elements_union_singleton. Qed.
   Lemma big_opS_fn_insert {B} (f : A → B → M) h X x b :
     x ∉ X →
     ([^o set] y ∈ {[ x ]} ∪ X, f y (<[x:=b]> h y))
@@ -529,7 +541,7 @@ Section gset.
   Qed.
 
   Lemma big_opS_singleton f x : ([^o set] y ∈ {[ x ]}, f y) ≡ f x.
-  Proof. intros. by rewrite big_opS_eq /big_opS_def elements_singleton /= right_id. Qed.
+  Proof. intros. by rewrite big_opS_elements elements_singleton /= right_id. Qed.
 
   Lemma big_opS_unit X : ([^o set] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
   Proof.
@@ -552,7 +564,7 @@ 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.
+  Proof. by rewrite !big_opS_elements -big_opL_op. Qed.
 
   Lemma big_opS_list_to_set f (l : list A) :
     NoDup l →
@@ -623,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.
 
@@ -656,6 +674,100 @@ 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_opL {A} `{Countable K} {B}
+    (f : K → A → nat → B → M) (m1 : gmap K A) (l2 : list B) :
+  ([^o map] k1↦x1 ∈ m1, [^o list] k2↦x2 ∈ l2, f k1 x1 k2 x2) ≡
+  ([^o list] k2↦x2 ∈ l2, [^o map] k1↦x1 ∈ m1, f k1 x1 k2 x2).
+Proof. symmetry. apply big_opL_opM. 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_opL `{Countable A} {B}
+    (f : A → nat → B → M) (X1 : gset A) (l2 : list B) :
+  ([^o set] x1 ∈ X1, [^o list] k2↦x2 ∈ l2, f x1 k2 x2) ≡
+  ([^o list] k2↦x2 ∈ l2, [^o set] x1 ∈ X1, f x1 k2 x2).
+Proof. symmetry. apply big_opL_opS. Qed.
+Lemma big_opS_opM `{Countable A} `{Countable K} {B}
+    (f : A → K → B → M) (X1 : gset A) (m2 : gmap K B) :
+  ([^o set] x1 ∈ X1, [^o map] k2↦x2 ∈ m2, f x1 k2 x2) ≡
+  ([^o map] k2↦x2 ∈ m2, [^o set] x1 ∈ X1, f x1 k2 x2).
+Proof. symmetry. apply big_opM_opS. 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_opL `{Countable A} {B}
+    (f : A → nat → B → M) (X1 : gmultiset A) (l2 : list B) :
+  ([^o mset] x1 ∈ X1, [^o list] k2↦x2 ∈ l2, f x1 k2 x2) ≡
+  ([^o list] k2↦x2 ∈ l2, [^o mset] x1 ∈ X1, f x1 k2 x2).
+Proof. symmetry. apply big_opL_opMS. Qed.
+Lemma big_opMS_opM `{Countable A} `{Countable K} {B} (f : A → K → B → M)
+    (X1 : gmultiset A) (m2 : gmap K B) :
+  ([^o mset] x1 ∈ X1, [^o map] k2↦x2 ∈ m2, f x1 k2 x2) ≡
+  ([^o map] k2↦x2 ∈ m2, [^o mset] x1 ∈ X1, f x1 k2 x2).
+Proof. symmetry. apply big_opM_opMS. Qed.
+Lemma big_opMS_opS `{Countable A, Countable B}
+    (X : gmultiset A) (Y : gset B) (f : A → B → M) :
+  ([^o mset] x ∈ X, [^o set] y ∈ Y, f x y) ≡ ([^o set] y ∈ Y, [^o mset] x ∈ X, f x y).
+Proof. symmetry. apply big_opS_opMS. 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

@@ -2010,6 +2010,10 @@ Section gset.
      Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
   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).
+  Proof. by rewrite big_opS_elements. Qed.
+
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opS_empty. Qed.
   Lemma big_sepS_empty' P `{!Affine P} Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
@@ -2446,4 +2450,85 @@ 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_sepL `{Countable K} {A} {B}
+    (Φ : K → A → nat → B → PROP) (m1 : gmap K A) (l2 : list B) :
+  ([∗ map] k1↦x1 ∈ m1, [∗ list] k2↦x2 ∈ l2, Φ k1 x1 k2 x2) ⊣⊢
+  ([∗ list] k2↦x2 ∈ l2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 k2 x2).
+Proof. apply big_opM_opL. 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_sepL `{Countable A} {B}
+    (f : A → nat → B → PROP) (X1 : gset A) (l2 : list B) :
+  ([∗ set] x1 ∈ X1, [∗ list] k2↦x2 ∈ l2, f x1 k2 x2) ⊣⊢
+  ([∗ list] k2↦x2 ∈ l2, [∗ set] x1 ∈ X1, f x1 k2 x2).
+Proof. apply big_opS_opL. Qed.
+Lemma big_sepS_sepM `{Countable A} `{Countable K} {B}
+    (f : A → K → B → PROP) (X1 : gset A) (m2 : gmap K B) :
+  ([∗ set] x1 ∈ X1, [∗ map] k2↦x2 ∈ m2, f x1 k2 x2) ⊣⊢
+  ([∗ map] k2↦x2 ∈ m2, [∗ set] x1 ∈ X1, f x1 k2 x2).
+Proof. apply big_opS_opM. 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_sepL `{Countable A} {B}
+    (f : A → nat → B → PROP) (X1 : gmultiset A) (l2 : list B) :
+  ([∗ mset] x1 ∈ X1, [∗ list] k2↦x2 ∈ l2, f x1 k2 x2) ⊣⊢
+  ([∗ list] k2↦x2 ∈ l2, [∗ mset] x1 ∈ X1, f x1 k2 x2).
+Proof. apply big_opMS_opL. Qed.
+Lemma big_sepMS_sepM `{Countable A} `{Countable K} {B} (f : A → K → B → PROP)
+    (X1 : gmultiset A) (m2 : gmap K B) :
+  ([∗ mset] x1 ∈ X1, [∗ map] k2↦x2 ∈ m2, f x1 k2 x2) ⊣⊢
+  ([∗ map] k2↦x2 ∈ m2, [∗ mset] x1 ∈ X1, f x1 k2 x2).
+Proof. apply big_opMS_opM. Qed.
+Lemma big_sepMS_sepS `{Countable A, Countable B}
+    (X : gmultiset A) (Y : gset B) (f : A → B → PROP) :
+  ([∗ mset] x ∈ X, [∗ set] y ∈ Y, f x y) ⊣⊢ ([∗ set] y ∈ Y, [∗ mset] x ∈ X, f x y).
+Proof. apply big_opMS_opS. 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.