From 982a55c7311bc0560f97de45a0ce7b3a1f82779a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Jun 2018 21:30:26 +0200
Subject: [PATCH] Proof mode class instances for `big_sepL2`.

All those for `big_sepL` that hold.
---
 theories/proofmode/class_instances_bi.v  | 44 ++++++++++++++++++++++++
 theories/proofmode/class_instances_sbi.v |  8 +++++
 theories/proofmode/frame_instances.v     | 16 ++++++++-
 theories/proofmode/ltac_tactics.v        |  2 ++
 4 files changed, 69 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 3b611e660..47352dc51 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -548,6 +548,28 @@ Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat → A → PROP) l
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
 
+Global Instance from_and_big_sepL2_cons_persistent {A B}
+    (Φ : nat → A → B → PROP) l1 x1 l1' l2 x2 l2' :
+  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
+  Persistent (Φ 0 x1 x2) →
+  FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
+    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
+Proof.
+  rewrite /IsCons=> -> -> ?.
+  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
+Qed.
+Global Instance from_and_big_sepL2_app_persistent {A B}
+    (Φ : nat → A → B → PROP) l1 l1' l1'' l2 l2' l2'' :
+  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
+  (∀ k y1 y2, Persistent (Φ k y1 y2)) →
+  FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
+    ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
+    ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
+Proof.
+  rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
+  apply wand_elim_l', big_sepL2_app.
+Qed.
+
 (** FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
 Proof. by rewrite /FromSep. Qed.
@@ -587,6 +609,20 @@ Global Instance from_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
 
+Global Instance from_sep_big_sepL2_cons {A B} (Φ : nat → A → B → PROP)
+    l1 x1 l1' l2 x2 l2' :
+  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
+  FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
+    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
+Proof. rewrite /IsCons=> -> ->. by rewrite /FromSep big_sepL2_cons. Qed.
+Global Instance from_sep_big_sepL2_app {A B} (Φ : nat → A → B → PROP)
+    l1 l1' l1'' l2 l2' l2'' :
+  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
+  FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
+    ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
+    ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
+Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.
+
 Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
@@ -728,6 +764,14 @@ Global Instance into_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.
 
+(* No instance for app, since that only works when the LHSs have the same length *)
+Global Instance into_sep_big_sepL2_cons {A B}
+    (Φ : nat → A → B → PROP) l1 x1 l1' l2 x2 l2' :
+  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
+  IntoSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
+    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
+Proof. rewrite /IsCons=>-> ->. by rewrite /IntoSep big_sepL2_cons. Qed.
+
 (** FromOr *)
 Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
 Proof. by rewrite /FromOr. Qed.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 6c9e2203b..a502d691e 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -606,6 +606,14 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opL_commute. by apply big_sepL_mono.
 Qed.
+Global Instance into_laterN_big_sepL2 n {A B} (Φ Ψ : nat → A → B → PROP) l1 l2 :
+  (∀ x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2)) →
+  IntoLaterN false n ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
+    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2).
+Proof.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
+  rewrite -big_sepL2_laterN_2. by apply big_sepL2_mono.
+Qed.
 Global Instance into_laterN_big_sepM n `{Countable K} {A}
     (Φ Ψ : K → A → PROP) (m : gmap K A) :
   (∀ x k, IntoLaterN false n (Φ k x) (Ψ k x)) →
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index b382f7f90..9dc54746d 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -89,7 +89,21 @@ Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
   Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
            [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
   Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
+Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
+
+Global Instance frame_big_sepL2_cons {A B} p (Φ : nat → A → B → PROP)
+    R Q l1 x1 l1' l2 x2 l2' :
+  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
+  Frame p R (Φ 0 x1 x2 ∗ [∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2) Q →
+  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
+Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
+Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
+    R Q l1 l1' l1'' l2 l2' l2'' :
+  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
+  Frame p R (([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
+           [∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2) Q →
+  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
+Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
 Global Instance make_and_true_l P : KnownLMakeAnd True P P.
 Proof. apply left_id, _. Qed.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index f7b1df291..1bd449ec2 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2091,6 +2091,8 @@ Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
   rewrite envs_entails_eq; apply bi.internal_eq_refl.
 Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepL_nil'.
+Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
+  rewrite envs_entails_eq; apply big_sepL2_nil'.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepM_empty'.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
-- 
GitLab