From a5753b1b545af7aa95f8d2f708034c35cb0b3c7a Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 29 Mar 2019 14:52:50 +0100
Subject: [PATCH] Proofmode stuff for big_sepM2.

---
 theories/proofmode/class_instances_sbi.v | 8 ++++++++
 theories/proofmode/ltac_tactics.v        | 2 ++
 2 files changed, 10 insertions(+)

diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index d6eaeb496..22ef7853e 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/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}
+    (Φ Ψ : K → A → A → PROP) (m1 m2 : gmap K A) :
+  (∀ 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)) →
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index cf2661ddd..52b46c830 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/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 _ _ _)) =>
-- 
GitLab