From 7b9f1cb24dc7565fe78fda3f0ead7787873f3bb9 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 29 Mar 2019 14:47:09 +0100
Subject: [PATCH] Add sbi lemmas for big_sepM2.

---
 theories/bi/big_op.v | 56 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index a46cfcd9b..f2fb0cbd9 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1436,6 +1436,62 @@ Section gmap.
   End plainly.
 End gmap.
 
+Section gmap2.
+  Context `{Countable K} {A : Type}.
+  Implicit Types m : gmap K A.
+  Implicit Types Φ Ψ : K → A → A → PROP.
+
+  Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
+    (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
+    ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
+  Proof.
+    rewrite /big_sepM2 later_and (timeless ⌜_⌝%I).
+    rewrite big_sepM_later except_0_and.
+    auto using and_mono_r, except_0_intro.
+  Qed.
+  Lemma big_sepM2_later_2 Φ m1 m2 :
+    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
+    ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
+  Proof.
+    rewrite /big_sepM2 later_and -(later_intro ⌜_⌝%I).
+    apply and_mono_r. by rewrite big_opM_commute.
+  Qed.
+
+  Lemma big_sepM2_laterN_2 Φ n m1 m2 :
+    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷^n Φ k x1 x2)
+    ⊢ ▷^n [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
+  Proof.
+    induction n as [|n IHn]; first done.
+    rewrite later_laterN -IHn -big_sepM2_later_2.
+    apply big_sepM2_mono. eauto.
+  Qed.
+
+  Global Instance big_sepM2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+  Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
+  Global Instance big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
+    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
+    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+  Proof. intros. rewrite /big_sepM2. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepM2_plainly `{BiAffine PROP} Φ m1 m2 :
+      ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢
+      [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
+    Proof. by rewrite /big_sepM2 plainly_and plainly_pure big_sepM_plainly. Qed.
+
+    Global Instance big_sepM2_empty_plain `{BiAffine PROP} Φ :
+      Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+    Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
+    Global Instance big_sepM2_plain `{BiAffine PROP} Φ m1 m2 :
+      (∀ k x1 x2, Plain (Φ k x1 x2)) →
+      Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+    Proof. intros. rewrite /big_sepM2. apply _. Qed.
+  End plainly.
+End gmap2.
+
 (** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.
-- 
GitLab