Merge branch 'robbert/big_sepM2_lookup' into 'master'

Add lemmas `big_sepM2_inv_{l,r}` and rename `big_sepM2_lookup_{1,2}` into `big_sepM2_lookup_{l,r}`.

See merge request iris/iris!692

CHANGELOG.md

@@ -28,6 +28,12 @@ Coq 8.11 is no longer supported in this version of Iris.
   is not very well-behaved.
 * Extend `gmap_view` with lemmas for "big" operations on maps.
 
+**Changes in `bi`:**
+
+* 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`.
+
 **Changes in `proofmode`:**
 
 * Add support for pure names `%H` in intro patterns. This is now natively
@@ -77,6 +83,9 @@ s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_va
 s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
 s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
 s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
+# big_sepM renames
+s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
+s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 EOF
 ```
 

iris/bi/big_op.v

@@ -1471,6 +1471,47 @@ Section map2.
       apply (big_sepM_delete (λ i xx, Φ i xx.1 xx.2) (map_zip m1 m2) i (x1,x2)).
       by rewrite map_lookup_zip_with Hx1 Hx2.
   Qed.
+  Lemma big_sepM2_delete_l Φ m1 m2 i x1 :
+    m1 !! i = Some x1 →
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
+    ⊣⊢ ∃ x2, ⌜m2 !! i = Some x2⌝ ∧
+            (Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
+  Proof.
+    intros Hm1. apply (anti_symm _).
+    - rewrite big_sepM2_eq /big_sepM2_def. apply pure_elim_l=> Hm.
+      assert (is_Some (m2 !! i)) as [x2 Hm2].
+      { apply Hm. by econstructor. }
+      rewrite -(exist_intro x2).
+      rewrite (big_sepM_delete _ _ i (x1,x2)) /=;
+        last by rewrite map_lookup_zip_with Hm1 Hm2.
+      rewrite pure_True // left_id.
+      f_equiv. apply and_intro.
+      + apply pure_intro=> k. by rewrite !lookup_delete_is_Some Hm.
+      + by rewrite -map_delete_zip_with.
+    - apply exist_elim=> x2. apply pure_elim_l=> ?.
+      by rewrite -big_sepM2_delete.
+  Qed.
+  Lemma big_sepM2_delete_r Φ m1 m2 i x2 :
+    m2 !! i = Some x2 →
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
+    ⊣⊢ ∃ x1, ⌜m1 !! i = Some x1⌝ ∧
+            (Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
+  Proof.
+    intros Hm2. apply (anti_symm _).
+    - rewrite big_sepM2_eq /big_sepM2_def.
+      apply pure_elim_l=> Hm.
+      assert (is_Some (m1 !! i)) as [x1 Hm1].
+      { apply Hm. by econstructor. }
+      rewrite -(exist_intro x1).
+      rewrite (big_sepM_delete _ _ i (x1,x2)) /=;
+        last by rewrite map_lookup_zip_with Hm1 Hm2.
+      rewrite pure_True // left_id.
+      f_equiv. apply and_intro.
+      + apply pure_intro=> k. by rewrite !lookup_delete_is_Some Hm.
+      + by rewrite -map_delete_zip_with.
+    - apply exist_elim=> x1. apply pure_elim_l=> ?.
+      by rewrite -big_sepM2_delete.
+  Qed.
 
   Lemma big_sepM2_insert_delete Φ m1 m2 i x1 x2 :
     ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
@@ -1524,39 +1565,21 @@ Section map2.
     m1 !! i = Some x1 → m2 !! i = Some x2 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ Φ i x1 x2.
   Proof. intros. rewrite big_sepM2_lookup_acc //. by rewrite sep_elim_l. Qed.
-
-  Lemma big_sepM2_lookup_1 Φ m1 m2 i x1 `{!∀ x2, Absorbing (Φ i x1 x2)} :
+  Lemma big_sepM2_lookup_l Φ m1 m2 i x1 `{!∀ x2, Absorbing (Φ i x1 x2)} :
     m1 !! i = Some x1 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊢ ∃ x2, ⌜m2 !! i = Some x2⌝ ∧ Φ i x1 x2.
   Proof.
-    intros Hm1. rewrite big_sepM2_eq /big_sepM2_def.
-    rewrite persistent_and_sep_1.
-    apply wand_elim_l'. apply pure_elim'=>Hm.
-    assert (is_Some (m2 !! i)) as [x2 Hm2].
-    { apply Hm. by econstructor. }
-    apply wand_intro_r. rewrite -(exist_intro x2).
-    rewrite /big_sepM2 (big_sepM_lookup _ _ i (x1,x2));
-      last by rewrite map_lookup_zip_with Hm1 Hm2.
-    rewrite pure_True// sep_elim_r.
-    apply and_intro=>//. by apply pure_intro.
+    intros Hm1. rewrite big_sepM2_delete_l //.
+    f_equiv=> x2. by rewrite sep_elim_l.
   Qed.
-
-  Lemma big_sepM2_lookup_2 Φ m1 m2 i x2 `{!∀ x1, Absorbing (Φ i x1 x2)} :
+  Lemma big_sepM2_lookup_r Φ m1 m2 i x2 `{!∀ x1, Absorbing (Φ i x1 x2)} :
     m2 !! i = Some x2 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊢ ∃ x1, ⌜m1 !! i = Some x1⌝ ∧ Φ i x1 x2.
   Proof.
-    intros Hm2. rewrite big_sepM2_eq /big_sepM2_def.
-    rewrite persistent_and_sep_1.
-    apply wand_elim_l'. apply pure_elim'=>Hm.
-    assert (is_Some (m1 !! i)) as [x1 Hm1].
-    { apply Hm. by econstructor. }
-    apply wand_intro_r. rewrite -(exist_intro x1).
-    rewrite /big_sepM2 (big_sepM_lookup _ _ i (x1,x2));
-      last by rewrite map_lookup_zip_with Hm1 Hm2.
-    rewrite pure_True// sep_elim_r.
-    apply and_intro=>//. by apply pure_intro.
+    intros Hm2. rewrite big_sepM2_delete_r //.
+    f_equiv=> x1. by rewrite sep_elim_l.
   Qed.
 
   Lemma big_sepM2_singleton Φ i x1 x2 :