From 6af84c026a70daa601b7be55a0e030ce3827ff23 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 25 Mar 2019 15:57:35 +0100
Subject: [PATCH] Implement big_sepM2 lemmas.

---
 theories/bi/big_op.v          | 303 ++++++++++++++++++++++------------
 theories/bi/derived_laws_bi.v |   7 +
 2 files changed, 202 insertions(+), 108 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 7c7f5145c..edccb879a 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -736,91 +736,23 @@ Section map2.
   Context `{Countable K} {A B : Type}.
   Implicit Types Φ Ψ : K → A → B → PROP.
 
-  Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
-  Proof.
-    rewrite /big_sepM2 pure_True ?left_id //.
-    intros k. rewrite !lookup_empty; split; by inversion 1.
-  Qed.
-  Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
-  Proof. rewrite big_sepM2_empty. apply (affine _). Qed.
-
-  Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
-    (m1 !! i = None ∨ m2 !! i = None) →
-    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
-    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
-  Proof.
-    intros Hm. rewrite /big_sepM2 -map_insert_zip_with.
-  Admitted.
-(*
-  Lemma big_sepM2_cons_inv_l Φ x1 m1 m2 :
-    ([∗ map] k↦y1;y2 ∈ x1 :: m1; m2, Φ k y1 y2) -∗
-    ∃ x2 m2', ⌜ m2 = x2 :: m2' ⌝ ∧
-              Φ 0 x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2', Φ (S k) y1 y2.
-  Proof.
-    destruct m2 as [|x2 m2]; simpl; auto using False_elim.
-    by rewrite -(exist_intro x2) -(exist_intro m2) pure_True // left_id.
-  Qed.
-  Lemma big_sepM2_cons_inv_r Φ x2 m1 m2 :
-    ([∗ map] k↦y1;y2 ∈ m1; x2 :: m2, Φ k y1 y2) -∗
-    ∃ x1 m1', ⌜ m1 = x1 :: m1' ⌝ ∧
-              Φ 0 x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1';m2, Φ (S k) y1 y2.
-  Proof.
-    destruct m1 as [|x1 m1]; simpl; auto using False_elim.
-    by rewrite -(exist_intro x1) -(exist_intro m1) pure_True // left_id.
-  Qed.
-*)
-
-  Lemma big_sepM2_singleton Φ i x1 x2 :
-    ([∗ map] k↦y1;y2 ∈ {[ i := x1 ]}; {[ i := x2 ]}, Φ k y1 y2) ⊣⊢ Φ i x1 x2.
-  Proof. rewrite /big_sepM2. Admitted.
-
   Lemma big_sepM2_dom Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) -∗ ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
-  Proof. Admitted.
-
-(*
-  Lemma big_sepM2_app Φ m1 m2 m1' m2' :
-    ([∗ map] k↦y1;y2 ∈ m1; m1', Φ k y1 y2) -∗
-    ([∗ map] k↦y1;y2 ∈ m2; m2', Φ (length m1 + k) y1 y2) -∗
-    ([∗ map] k↦y1;y2 ∈ m1 ++ m2; m1' ++ m2', Φ k y1 y2).
-  Proof.
-    apply wand_intro_r. revert Φ m1'. induction m1 as [|x1 m1 IH]=> Φ -[|x1' m1'] /=.
-    - by rewrite left_id.
-    - rewrite left_absorb. apply False_elim.
-    - rewrite left_absorb. apply False_elim.
-    - by rewrite -assoc IH.
-  Qed.
-  Lemma big_sepM2_app_inv_l Φ m1' m1'' m2 :
-    ([∗ map] k↦y1;y2 ∈ m1' ++ m1''; m2, Φ k y1 y2) -∗
-    ∃ m2' m2'', ⌜ m2 = m2' ++ m2'' ⌝ ∧
-                ([∗ map] k↦y1;y2 ∈ m1';m2', Φ k y1 y2) ∗
-                ([∗ map] k↦y1;y2 ∈ m1'';m2'', Φ (length m1' + k) y1 y2).
-  Proof.
-    rewrite -(exist_intro (take (length m1') m2))
-      -(exist_intro (drop (length m1') m2)) take_drop pure_True // left_id.
-    revert Φ m2. induction m1' as [|x1 m1' IH]=> Φ -[|x2 m2] /=;
-       [by rewrite left_id|by rewrite left_id|apply False_elim|].
-    by rewrite IH -assoc.
-  Qed.
-  Lemma big_sepM2_app_inv_r Φ m1 m2' m2'' :
-    ([∗ map] k↦y1;y2 ∈ m1; m2' ++ m2'', Φ k y1 y2) -∗
-    ∃ m1' m1'', ⌜ m1 = m1' ++ m1'' ⌝ ∧
-                ([∗ map] k↦y1;y2 ∈ m1';m2', Φ k y1 y2) ∗
-                ([∗ map] k↦y1;y2 ∈ m1'';m2'', Φ (length m2' + k) y1 y2).
   Proof.
-    rewrite -(exist_intro (take (length m2') m1))
-      -(exist_intro (drop (length m2') m1)) take_drop pure_True // left_id.
-    revert Φ m1. induction m2' as [|x2 m2' IH]=> Φ -[|x1 m1] /=;
-       [by rewrite left_id|by rewrite left_id|apply False_elim|].
-    by rewrite IH -assoc.
+    rewrite /big_sepM2 bi.and_elim_l. apply pure_mono=>Hm.
+    set_unfold=>k. by rewrite !elem_of_dom.
   Qed.
 
   Lemma big_sepM2_mono Φ Ψ m1 m2 :
     (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
     ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
   Proof.
-    intros H. rewrite !big_sepM2_alt. f_equiv. apply big_sepL_mono=> k [y1 y2].
-    rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
+    intros Hm1m2. rewrite /big_sepM2. apply bi.and_mono_r, big_sepM_mono.
+    intros k [x1 x2]. rewrite map_lookup_zip_with.
+    specialize (Hm1m2 k x1 x2).
+    destruct (m1 !! k) as [y1|]; last done.
+    destruct (m2 !! k) as [y2|]; simpl; last done.
+    intros ?; simplify_eq. by apply Hm1m2.
   Qed.
   Lemma big_sepM2_proper Φ Ψ m1 m2 :
     (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊣⊢ Ψ k y1 y2) →
@@ -833,30 +765,125 @@ Section map2.
   Global Instance big_sepM2_ne n :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
       ==> (=) ==> (=) ==> (dist n))
-           (big_sepM2 (PROP:=PROP) (A:=A) (B:=B)).
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof.
-    intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite !big_sepM2_alt. f_equiv.
+    intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite /big_sepM2. f_equiv.
     f_equiv=> k [y1 y2]. apply HΦ.
   Qed.
   Global Instance big_sepM2_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
       ==> (=) ==> (=) ==> (⊢))
-           (big_sepM2 (PROP:=PROP) (A:=A) (B:=B)).
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_mono; intros; apply Hf. Qed.
   Global Instance big_sepM2_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
       ==> (=) ==> (=) ==> (⊣⊢))
-           (big_sepM2 (PROP:=PROP) (A:=A) (B:=B)).
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
 
+  Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
+  Proof.
+    rewrite /big_sepM2 pure_True ?left_id //.
+    intros k. rewrite !lookup_empty; split; by inversion 1.
+  Qed.
+  Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
+  Proof. rewrite big_sepM2_empty. apply (affine _). Qed.
+
+  Lemma big_sepM2_empty_l m1 Φ :
+    ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
+  Proof.
+    rewrite /big_sepM2 and_elim_l.
+    apply pure_elim'=>Hm1. apply pure_mono=>_.
+    apply map_eq=>k. specialize (Hm1 k). revert Hm1.
+    rewrite !lookup_empty /=. destruct (m1 !! k) as [x|]; last done.
+    intros Hm1. exfalso. eapply is_Some_None, Hm1. eauto.
+  Qed.
+
+  Lemma big_sepM2_empty_r m2 Φ :
+    ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
+  Proof.
+    rewrite /big_sepM2 and_elim_l.
+    apply pure_elim'=>Hm2. apply pure_mono=>_.
+    apply map_eq=>k. specialize (Hm2 k). revert Hm2.
+    rewrite !lookup_empty /=. destruct (m2 !! k) as [x|]; last done.
+    intros Hm2. exfalso. eapply is_Some_None, Hm2. eauto.
+  Qed.
+
+  Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
+    m1 !! i = None → m2 !! i = None →
+    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
+    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
+  Proof.
+    intros Hm1 Hm2. rewrite /big_sepM2 -map_insert_zip_with.
+    rewrite big_sepM_insert.
+    2:{ rewrite map_lookup_zip_with Hm1 //. }
+    rewrite !persistent_and_affinely_sep_l /=.
+    rewrite sep_assoc (sep_comm _ (Φ _ _ _)) -sep_assoc.
+    repeat apply sep_proper=>//.
+    apply affinely_proper, pure_proper.
+    split.
+    - intros H1 k. destruct (decide (i = k)) as [->|?].
+      + rewrite Hm1 Hm2 //. by split; intros ?; exfalso; eapply is_Some_None.
+      + specialize (H1 k). revert H1. rewrite !lookup_insert_ne //.
+    - intros H1 k. destruct (decide (i = k)) as [->|?].
+      + rewrite !lookup_insert. split; by econstructor.
+      + rewrite !lookup_insert_ne //.
+  Qed.
+
+  Lemma big_sepM2_delete Φ m1 m2 i x1 x2 :
+    m1 !! i = Some x1 → m2 !! i = Some x2 →
+    ([∗ map] k↦x;y ∈ m1;m2, Φ k x y) ⊣⊢
+      Φ i x1 x2 ∗ [∗ map] k↦x;y ∈ delete i m1;delete i m2, Φ k x y.
+  Proof.
+    rewrite /big_sepM2 => Hx1 Hx2.
+    rewrite !persistent_and_affinely_sep_l /=.
+    rewrite sep_assoc (sep_comm  (Φ _ _ _)) -sep_assoc.
+    apply sep_proper.
+    - apply affinely_proper, pure_proper. split.
+      + intros Hm k. destruct (decide (i = k)) as [->|?].
+        { rewrite !lookup_delete. split; intros []%is_Some_None. }
+        rewrite !lookup_delete_ne //.
+      + intros Hm k. specialize (Hm k). revert Hm. destruct (decide (i = k)) as [->|?].
+        { intros _. rewrite Hx1 Hx2. split; eauto. }
+        rewrite !lookup_delete_ne //.
+    - rewrite -map_delete_zip_with.
+      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_insert_2 Φ m1 m2 i x1 x2 :
+    TCOr (∀ x y, Affine (Φ i x y)) (Absorbing (Φ i x1 x2)) →
+    Φ i x1 x2 -∗
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
+    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2).
+  Proof.
+    intros Ha. rewrite /big_sepM2.
+    assert (TCOr (∀ x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
+    { destruct Ha; try apply _. }
+    apply wand_intro_r.
+    rewrite !persistent_and_affinely_sep_l /=.
+    rewrite (sep_comm  (Φ _ _ _)) -sep_assoc. apply sep_mono.
+    { apply affinely_mono, pure_mono. intros Hm k.
+      destruct (decide (i = k)) as [->|].
+      - rewrite !lookup_insert. split; eauto.
+      - rewrite !lookup_insert_ne //. }
+    rewrite (big_sepM_insert_2 (λ k xx, Φ k xx.1 xx.2) (map_zip m1 m2) i (x1, x2)).
+    rewrite map_insert_zip_with. apply wand_elim_r.
+  Qed.
+
   Lemma big_sepM2_lookup_acc Φ m1 m2 i x1 x2 :
     m1 !! i = Some x1 → m2 !! i = Some x2 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢
     Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)).
   Proof.
-    intros Hm1 Hm2. rewrite big_sepM2_alt. apply pure_elim_l=> Hl.
-    rewrite {1}big_sepL_lookup_acc; last by rewrite lookup_zip_with; simplify_option_eq.
-    by rewrite pure_True // left_id.
+    intros Hm1 Hm2. rewrite /big_sepM2. apply pure_elim_l=> Hm.
+    rewrite {1}(big_sepM_lookup_acc _ _ i (x1,x2)).
+    2: { by rewrite map_lookup_zip_with Hm1 Hm2. }
+    apply bi.sep_mono_r. apply bi.wand_mono=>//.
+    rewrite <- (left_id True%I (∧)%I).
+    apply bi.and_mono=>//.
+    + by apply pure_mono=>_.
+    + by rewrite left_id.
   Qed.
 
   Lemma big_sepM2_lookup Φ m1 m2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
@@ -864,29 +891,65 @@ Section map2.
     ([∗ 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_singleton Φ i x1 x2 :
+    ([∗ map] k↦y1;y2 ∈ {[ i := x1 ]}; {[ i := x2 ]}, Φ k y1 y2) ⊣⊢ Φ i x1 x2.
+  Proof.
+    rewrite /big_sepM2 map_zip_with_singleton big_sepM_singleton.
+    apply (anti_symm _).
+    - apply bi.and_elim_r.
+    - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
+      apply bi.and_mono=>//. apply pure_mono=>_ k.
+      rewrite !lookup_insert_is_Some' !lookup_empty.
+      firstorder.
+  Qed.
+
+  Lemma big_sepM2_fmap {A' B'} (f : A → A') (g : B → B') (Φ : nat → A' → B' → PROP) m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ f <$> m1; g <$> m2, Φ k y1 y2)
+    ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) (g y2)).
+  Proof.
+    rewrite /big_sepM2. rewrite map_fmap_zip.
+    apply bi.and_proper.
+    - apply pure_proper. split.
+      + intros Hm k. specialize (Hm k). revert Hm.
+        by rewrite !lookup_fmap !fmap_is_Some.
+      + intros Hm k. specialize (Hm k). revert Hm.
+        by rewrite !lookup_fmap !fmap_is_Some.
+    - by rewrite big_sepM_fmap.
+  Qed.
+
   Lemma big_sepM2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) m1 m2 :
     ([∗ map] k↦y1;y2 ∈ f <$> m1; m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) y2).
-  Proof.
-    rewrite !big_sepM2_alt fmap_length zip_with_fmap_l zip_with_zip big_sepL_fmap.
-    by f_equiv; f_equiv=> k [??].
-  Qed.
+  Proof. rewrite -{1}(map_fmap_id m2). apply big_sepM2_fmap. Qed.
+
   Lemma big_sepM2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; g <$> m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 (g y2)).
+  Proof. rewrite -{1}(map_fmap_id m1). apply big_sepM2_fmap. Qed.
+
+  Lemma big_sepM2_insert_acc Φ m1 m2 i x1 x2 :
+    m1 !! i = Some x1 → m2 !! i = Some x2 →
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢
+    Φ i x1 x2 ∗ (∀ x1' x2', Φ i x1' x2' -∗
+        ([∗ map] k↦y1;y2 ∈ <[i:=x1']>m1;<[i:=x2']>m2, Φ k y1 y2)).
   Proof.
-    rewrite !big_sepM2_alt fmap_length zip_with_fmap_r zip_with_zip big_sepL_fmap.
-    by f_equiv; f_equiv=> k [??].
+    intros ??. rewrite {1}big_sepM2_delete //. apply sep_mono; [done|].
+    apply forall_intro=> x1'. apply forall_intro=> x2'.
+    rewrite -(insert_delete m1) -(insert_delete m2) big_sepM2_insert ?lookup_delete //.
+    by apply wand_intro_l.
   Qed.
 
   Lemma big_sepM2_sepM2 Φ Ψ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∗ Ψ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
-  Proof.simpl
-    rewrite !big_sepM2_alt big_sepL_sepL !persistent_and_affinely_sep_l.
-    rewrite -assoc (assoc _ _ (<affine> _)%I). rewrite -(comm bi_sep (<affine> _)%I).
-    rewrite -assoc (assoc _ _ (<affine> _)%I) -!persistent_and_affinely_sep_l.
-    by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
+  Proof.
+    rewrite /big_sepM2.
+    rewrite -{1}(and_idem ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
+    rewrite -and_assoc.
+    rewrite !persistent_and_affinely_sep_l /=.
+    rewrite -sep_assoc. apply bi.sep_proper=>//.
+    rewrite sep_assoc (sep_comm _ (<affine> _)%I) -sep_assoc.
+    apply bi.sep_proper=>//. apply big_sepM_sepM.
   Qed.
 
   Lemma big_sepM2_and Φ Ψ m1 m2 :
@@ -898,33 +961,57 @@ Section map2.
     <pers> ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊣⊢ [∗ map] k↦y1;y2 ∈ m1;m2, <pers> (Φ k y1 y2).
   Proof.
-    by rewrite !big_sepM2_alt persistently_and persistently_pure big_sepL_persistently.
+    by rewrite /big_sepM2 persistently_and
+         persistently_pure big_sepM_persistently.
   Qed.
 
-  Lemma big_sepM2_impl Φ Ψ m1 m2 :
+ Lemma big_sepM2_forall `{BiAffine PROP} Φ m1 m2 :
+   (∀ k x1 x2, Persistent (Φ k x1 x2)) →
+   ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢
+     ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝
+     ∧ (∀ k x1 x2, ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2).
+ Proof.
+   rewrite /big_sepM2=> ?. apply and_proper=>//.
+   rewrite big_sepM_forall. apply forall_proper=>k.
+   apply (anti_symm _).
+   - apply forall_intro=> x1. apply forall_intro=> x2.
+     rewrite (forall_elim (x1,x2)).
+     rewrite impl_curry -pure_and. apply impl_mono=>//.
+     apply pure_mono. rewrite map_lookup_zip_with. by intros [-> ->].
+   - apply forall_intro=> [[x1 x2]].
+     rewrite (forall_elim x1) (forall_elim x2).
+     rewrite impl_curry -pure_and. apply impl_mono=>//.
+     apply pure_mono. rewrite map_lookup_zip_with.
+     by destruct (m1 !! k), (m2 !! k)=>/= // ?; simplify_eq.
+ Qed.
+
+ Lemma big_sepM2_impl Φ Ψ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
     □ (∀ k x1 x2,
       ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2 -∗ Ψ k x1 x2) -∗
     [∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2.
   Proof.
-    apply wand_intro_l. revert Φ Ψ m2.
-    induction m1 as [|x1 m1 IH]=> Φ Ψ [|x2 m2] /=; [by rewrite sep_elim_r..|].
-    rewrite intuitionistically_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
-    apply sep_mono.
-    - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2) !pure_True // !True_impl.
-      by rewrite intuitionistically_elim wand_elim_l.
-    - rewrite comm -(IH (Φ ∘ S) (Ψ ∘ S)) /=.
-      apply sep_mono_l, affinely_mono, persistently_mono.
-      apply forall_intro=> k. by rewrite (forall_elim (S k)).
+    apply wand_intro_l.
+    rewrite /big_sepM2.
+    rewrite !persistent_and_affinely_sep_l /=.
+    rewrite sep_assoc. rewrite (sep_comm (â–¡ _)%I) -sep_assoc.
+    apply sep_mono_r. apply wand_elim_r'.
+    rewrite (big_sepM_impl _ (λ k xx, Ψ k xx.1 xx.2)). apply wand_mono=>//.
+    apply intuitionistically_mono'.
+    apply forall_mono=> k. apply forall_intro=> [[x y]].
+    rewrite (forall_elim x) (forall_elim y).
+    rewrite impl_curry -pure_and. apply impl_mono=>//.
+    apply pure_mono. rewrite map_lookup_zip_with.
+    destruct (m1 !! k) as [x1|], (m2 !! k) as [x2|]; naive_solver.
   Qed.
-*)
+
   Global Instance big_sepM2_empty_persistent Φ :
     Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
   Proof. rewrite big_sepM2_empty. apply _. Qed.
   Global Instance big_sepM2_persistent Φ m1 m2 :
     (∀ k x1 x2, Persistent (Φ k x1 x2)) →
     Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
-  Proof. (* rewrite big_sepM2_alt. apply _. Qed. *) Admitted.
+  Proof. rewrite /big_sepM2. apply _. Qed.
 
   Global Instance big_sepM2_empty_affine Φ :
     Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
@@ -932,7 +1019,7 @@ Section map2.
   Global Instance big_sepM2_affine Φ m1 m2 :
     (∀ k x1 x2, Affine (Φ k x1 x2)) →
     Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
-  Proof. (* rewrite big_sepM2_alt. apply _. Qed. *) Admitted.
+  Proof. rewrite /big_sepM2. apply _. Qed.
 End map2.
 
 (** ** Big ops over finite sets *)
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index be05410b9..a96754db2 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -245,6 +245,13 @@ Proof.
   - rewrite -(exist_intro ()). done.
 Qed.
 
+Lemma impl_curry P Q R : (P → Q → R) ⊣⊢ (P ∧ Q → R).
+Proof.
+  apply (anti_symm _).
+  - apply impl_intro_l. by rewrite (comm _ P) -and_assoc !impl_elim_r.
+  - do 2 apply impl_intro_l. by rewrite assoc (comm _ Q) impl_elim_r.
+Qed.
+
 Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
 Proof.
   apply (anti_symm (⊢)); first auto.
-- 
GitLab