big_sepM2 and associated lemmas

opam

@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-03-16.1.700545bb") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-03-26.0.d98ab4e4") | (= "dev") }
 ]

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.

theories/bi/notation.v

@@ -127,6 +127,13 @@ Reserved Notation "'[∗' 'map]' x ∈ m , P"
   (at level 200, m at level 10, x at level 1, right associativity,
    format "[∗  map]  x  ∈  m ,  P").
 
+Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
+  (at level 200, m1, m2 at level 10, k, x1, x2 at level 1, right associativity,
+   format "[∗  map]  k ↦ x1 ; x2  ∈  m1 ; m2 ,  P").
+Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
+  (at level 200, m1, m2 at level 10, x1, x2 at level 1, right associativity,
+   format "[∗  map]  x1 ; x2  ∈  m1 ; m2 ,  P").
+
 Reserved Notation "'[∗' 'set]' x ∈ X , P"
   (at level 200, X at level 10, x at level 1, right associativity,
    format "[∗  set]  x  ∈  X ,  P").

theories/proofmode/class_instances_sbi.v

@@ -650,6 +650,14 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opM_commute. by apply big_sepM_mono.
 Qed.
+Global Instance into_laterN_big_sepM2 n `{Countable K} {A B}
+    (Φ Ψ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
+  (∀ x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2)) →
+  IntoLaterN false n ([∗ map] k ↦ x1;x2 ∈ m1;m2, Φ k x1 x2) ([∗ map] k ↦ x1;x2 ∈ m1;m2, Ψ k x1 x2).
+Proof.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> HΦΨ.
+  rewrite -big_sepM2_laterN_2. by apply big_sepM2_mono.
+Qed.
 Global Instance into_laterN_big_sepS n `{Countable A}
     (Φ Ψ : A → PROP) (X : gset A) :
   (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →

theories/proofmode/ltac_tactics.v

@@ -2414,6 +2414,8 @@ Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepL2_nil' : core.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepM_empty' : core.
+Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
+  rewrite envs_entails_eq; apply big_sepM2_empty' : core.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepS_empty' : core.
 Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>