Merge branch 'robbert/big_sepL2' into 'gen_proofmode'

Separating big operator over two lists.

See merge request FP/iris-coq!158

tests/proofmode.ref

@@ -88,6 +88,32 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P
   
+1 subgoal
+  
+  PROP : sbi
+  x1, x2 : nat
+  l1, l2 : list nat
+  P : PROP
+  ============================
+  "HP" : P
+  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
+  _ : <affine> ⌜x1 = x2⌝
+      ∗ ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
+  --------------------------------------∗
+  P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
+  
+1 subgoal
+  
+  PROP : sbi
+  Φ : nat → nat → PROP
+  x1, x2 : nat
+  l1, l2 : list nat
+  ============================
+  _ : Φ x1 x2
+  _ : [∗ list] y1;y2 ∈ l1;l2, Φ y1 y2
+  --------------------------------------∗
+  <absorb> Φ x1 x2
+  
 1 subgoal
   
   PROP : sbi

tests/proofmode.v

@@ -486,11 +486,28 @@ Proof.
 Qed.
 
 Lemma test_big_sepL_simpl x (l : list nat) P :
-  P -∗
+   P -∗
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
   ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
   P.
 Proof. iIntros "HP ?? /=". Show. done. Qed.
+
+Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
+  P -∗
+  ([∗ list] k↦y1;y2 ∈ []; l2, <affine> ⌜ y1 = y2 ⌝) -∗
+  ([∗ list] y1;y2 ∈ x1 :: l1; (x2 :: l2) ++ l2, <affine> ⌜ y1 = y2 ⌝) -∗
+  P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True).
+Proof. iIntros "HP ?? /=". Show. by iLeft. Qed.
+
+Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) :
+  ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗
+  <absorb> Φ x1 x2.
+Proof. iIntros "[??]". Show. iFrame. Qed.
+
+Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P :
+  Φ 0 10 -∗ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) -∗
+  ([∗ list] y1;y2 ∈ (0 :: l1);(10 :: l2), Φ y1 y2).
+Proof. iIntros "$ ?". iFrame. Qed.
 End tests.
 
 (** Test specifically if certain things print correctly. *)

theories/bi/big_op.v

@@ -4,6 +4,21 @@ From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
+(** A version of the separating big operator that ranges over two lists. This
+version also ensures that both lists have the same length. Although this version
+can be defined in terms of the unary using a [zip] (see [big_sepL2_alt]), we do
+not define it that way to get better computational behavior (for [simpl]). *)
+Fixpoint big_sepL2 {PROP : bi} {A B}
+    (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) : PROP :=
+  match l1, l2 with
+  | [], [] => emp
+  | x1 :: l1, x2 :: l2 => Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2
+  | _, _ => False
+  end%I.
+Instance: Params (@big_sepL2) 3.
+Arguments big_sepL2 {PROP A B} _ !_ !_ /.
+Typeclasses Opaque big_sepL2.
+
 (* Notations *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
   (big_opL bi_sep (λ k x, P) l) : bi_scope.
@@ -12,6 +27,11 @@ Notation "'[∗' 'list]' x ∈ l , P" :=
 
 Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
 
+Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
+  (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
+Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
+  (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
+
 Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
   (big_opL bi_and (λ k x, P) l) : bi_scope.
 Notation "'[∧' 'list]' x ∈ l , P" :=
@@ -185,7 +205,7 @@ Section sep_list.
   Proof. induction 1; simpl; apply _. Qed.
 End sep_list.
 
-Section sep_list2.
+Section sep_list_more.
   Context {A : Type}.
   Implicit Types l : list A.
   Implicit Types Φ Ψ : nat → A → PROP.
@@ -199,6 +219,217 @@ Section sep_list2.
     - by rewrite big_sepL_emp left_id.
     - by rewrite IH.
   Qed.
+End sep_list_more.
+
+Lemma big_sepL2_alt {A B} (Φ : nat → A → B → PROP) l1 l2 :
+  ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2)
+  ⊣⊢ ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ y ∈ zip l1 l2, Φ k (y.1) (y.2).
+Proof.
+  apply (anti_symm _).
+  - apply and_intro.
+    + revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2] /=;
+        auto using pure_intro, False_elim.
+      rewrite IH sep_elim_r. apply pure_mono; auto.
+    + revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2] /=;
+        auto using pure_intro, False_elim.
+      by rewrite IH.
+  - apply pure_elim_l=> /Forall2_same_length Hl. revert Φ.
+    induction Hl as [|x1 l1 x2 l2 _ _ IH]=> Φ //=. by rewrite -IH.
+Qed.
+
+(** ** Big ops over two lists *)
+Section sep_list2.
+  Context {A B : Type}.
+  Implicit Types Φ Ψ : nat → A → B → PROP.
+
+  Lemma big_sepL2_nil Φ : ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2) ⊣⊢ emp.
+  Proof. done. Qed.
+  Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2.
+  Proof. apply (affine _). Qed.
+
+  Lemma big_sepL2_cons Φ x1 x2 l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ x1 :: l1; x2 :: l2, Φ k y1 y2)
+    ⊣⊢ Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2, Φ (S k) y1 y2.
+  Proof. done. Qed.
+  Lemma big_sepL2_cons_inv_l Φ x1 l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ x1 :: l1; l2, Φ k y1 y2) -∗
+    ∃ x2 l2', ⌜ l2 = x2 :: l2' ⌝ ∧
+              Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2', Φ (S k) y1 y2.
+  Proof.
+    destruct l2 as [|x2 l2]; simpl; auto using False_elim.
+    by rewrite -(exist_intro x2) -(exist_intro l2) pure_True // left_id.
+  Qed.
+  Lemma big_sepL2_cons_inv_r Φ x2 l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1; x2 :: l2, Φ k y1 y2) -∗
+    ∃ x1 l1', ⌜ l1 = x1 :: l1' ⌝ ∧
+              Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1';l2, Φ (S k) y1 y2.
+  Proof.
+    destruct l1 as [|x1 l1]; simpl; auto using False_elim.
+    by rewrite -(exist_intro x1) -(exist_intro l1) pure_True // left_id.
+  Qed.
+
+  Lemma big_sepL2_singleton Φ x1 x2 :
+    ([∗ list] k↦y1;y2 ∈ [x1];[x2], Φ k y1 y2) ⊣⊢ Φ 0 x1 x2.
+  Proof. by rewrite /= right_id. Qed.
+
+  Lemma big_sepL2_length Φ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) -∗ ⌜ length l1 = length l2 ⌝.
+  Proof. by rewrite big_sepL2_alt and_elim_l. Qed.
+
+  Lemma big_sepL2_app Φ l1 l2 l1' l2' :
+    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) -∗
+    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k) y1 y2) -∗
+    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2).
+  Proof.
+    apply wand_intro_r. revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /=.
+    - by rewrite left_id.
+    - rewrite left_absorb. apply False_elim.
+    - rewrite left_absorb. apply False_elim.
+    - by rewrite -assoc IH.
+  Qed.
+  Lemma big_sepL2_app_inv_l Φ l1' l1'' l2 :
+    ([∗ list] k↦y1;y2 ∈ l1' ++ l1''; l2, Φ k y1 y2) -∗
+    ∃ l2' l2'', ⌜ l2 = l2' ++ l2'' ⌝ ∧
+                ([∗ list] k↦y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
+                ([∗ list] k↦y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
+  Proof.
+    rewrite -(exist_intro (take (length l1') l2))
+      -(exist_intro (drop (length l1') l2)) take_drop pure_True // left_id.
+    revert Φ l2. induction l1' as [|x1 l1' IH]=> Φ -[|x2 l2] /=;
+       [by rewrite left_id|by rewrite left_id|apply False_elim|].
+    by rewrite IH -assoc.
+  Qed.
+  Lemma big_sepL2_app_inv_r Φ l1 l2' l2'' :
+    ([∗ list] k↦y1;y2 ∈ l1; l2' ++ l2'', Φ k y1 y2) -∗
+    ∃ l1' l1'', ⌜ l1 = l1' ++ l1'' ⌝ ∧
+                ([∗ list] k↦y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
+                ([∗ list] k↦y1;y2 ∈ l1'';l2'', Φ (length l2' + k) y1 y2).
+  Proof.
+    rewrite -(exist_intro (take (length l2') l1))
+      -(exist_intro (drop (length l2') l1)) take_drop pure_True // left_id.
+    revert Φ l1. induction l2' as [|x2 l2' IH]=> Φ -[|x1 l1] /=;
+       [by rewrite left_id|by rewrite left_id|apply False_elim|].
+    by rewrite IH -assoc.
+  Qed.
+
+  Lemma big_sepL2_mono Φ Ψ l1 l2 :
+    (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
+    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2.
+  Proof.
+    intros H. rewrite !big_sepL2_alt. f_equiv. apply big_sepL_mono=> k [y1 y2].
+    rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
+  Qed.
+  Lemma big_sepL2_proper Φ Ψ l1 l2 :
+    (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊣⊢ Ψ k y1 y2) →
+    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2.
+  Proof.
+    intros; apply (anti_symm _);
+      apply big_sepL2_mono; auto using equiv_entails, equiv_entails_sym.
+  Qed.
+
+  Global Instance big_sepL2_ne n :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
+      ==> (=) ==> (=) ==> (dist n))
+           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof.
+    intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite !big_sepL2_alt. f_equiv.
+    f_equiv=> k [y1 y2]. apply HΦ.
+  Qed.
+  Global Instance big_sepL2_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
+      ==> (=) ==> (=) ==> (⊢))
+           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_mono; intros; apply Hf. Qed.
+  Global Instance big_sepL2_proper' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
+      ==> (=) ==> (=) ==> (⊣⊢))
+           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_proper; intros; apply Hf. Qed.
+
+  Lemma big_sepL2_lookup_acc Φ l1 l2 i x1 x2 :
+    l1 !! i = Some x1 → l2 !! i = Some x2 →
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢
+    Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)).
+  Proof.
+    intros Hl1 Hl2. rewrite big_sepL2_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.
+  Qed.
+
+  Lemma big_sepL2_lookup Φ l1 l2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
+    l1 !! i = Some x1 → l2 !! i = Some x2 →
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ Φ i x1 x2.
+  Proof. intros. rewrite big_sepL2_lookup_acc //. by rewrite sep_elim_l. Qed.
+
+  Lemma big_sepL2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ f <$> l1; l2, Φ k y1 y2)
+    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k (f y1) y2).
+  Proof.
+    rewrite !big_sepL2_alt fmap_length zip_with_fmap_l zip_with_zip big_sepL_fmap.
+    by f_equiv; f_equiv=> k [??].
+  Qed.
+  Lemma big_sepL2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1; g <$> l2, Φ k y1 y2)
+    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 (g y2)).
+  Proof.
+    rewrite !big_sepL2_alt fmap_length zip_with_fmap_r zip_with_zip big_sepL_fmap.
+    by f_equiv; f_equiv=> k [??].
+  Qed.
+
+  Lemma big_sepL2_sepL2 Φ Ψ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2)
+    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
+  Proof.
+    rewrite !big_sepL2_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.
+  Qed.
+
+  Lemma big_sepL2_and Φ Ψ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∧ Ψ k y1 y2)
+    ⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∧ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
+  Proof. auto using and_intro, big_sepL2_mono, and_elim_l, and_elim_r. Qed.
+
+  Lemma big_sepL2_persistently `{BiAffine PROP} Φ l1 l2 :
+    <pers> ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
+    ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, <pers> (Φ k y1 y2).
+  Proof.
+    by rewrite !big_sepL2_alt persistently_and persistently_pure big_sepL_persistently.
+  Qed.
+
+  Lemma big_sepL2_impl Φ Ψ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
+    □ (∀ k x1 x2,
+      ⌜l1 !! k = Some x1⌝ → ⌜l2 !! k = Some x2⌝ → Φ k x1 x2 -∗ Ψ k x1 x2) -∗
+    [∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2.
+  Proof.
+    apply wand_intro_l. revert Φ Ψ l2.
+    induction l1 as [|x1 l1 IH]=> Φ Ψ [|x2 l2] /=; [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)).
+  Qed.
+
+  Global Instance big_sepL2_nil_persistent Φ :
+    Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL2_persistent Φ l1 l2 :
+    (∀ k x1 x2, Persistent (Φ k x1 x2)) →
+    Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. rewrite big_sepL2_alt. apply _. Qed.
+
+  Global Instance big_sepL2_nil_affine Φ :
+    Affine ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL2_affine Φ l1 l2 :
+    (∀ k x1 x2, Affine (Φ k x1 x2)) →
+    Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. rewrite big_sepL2_alt. apply _. Qed.
 End sep_list2.
 
 Section and_list.
@@ -757,6 +988,51 @@ Section list.
   End plainly.
 End list.
 
+Section list2.
+  Context {A B : Type}.
+  Implicit Types Φ Ψ : nat → A → B → PROP.
+
+  Lemma big_sepL2_later_2 Φ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
+  Proof.
+    rewrite !big_sepL2_alt bi.later_and big_sepL_later_2.
+    auto using and_mono, later_intro.
+  Qed.
+
+  Lemma big_sepL2_laterN_2 Φ n l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷^n Φ k y1 y2) ⊢ ▷^n [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
+  Proof.
+    rewrite !big_sepL2_alt bi.laterN_and big_sepL_laterN_2.
+    auto using and_mono, laterN_intro.
+  Qed.
+
+  Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 :
+    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
+    Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. rewrite big_sepL2_alt. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepL2_plainly `{!BiAffine PROP} Φ l1 l2 :
+      ■ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
+      ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■ (Φ k y1 y2).
+    Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed.
+
+    Global Instance big_sepL2_nil_plain `{!BiAffine PROP} Φ :
+      Plain ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+    Proof. simpl; apply _. Qed.
+
+    Global Instance big_sepL2_plain `{!BiAffine PROP} Φ l1 l2 :
+      (∀ k x1 x2, Plain (Φ k x1 x2)) →
+      Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+    Proof. rewrite big_sepL2_alt. apply _. Qed.
+  End plainly.
+End list2.
+
 (** ** Big ops over finite maps *)
 Section gmap.
   Context `{Countable K} {A : Type}.

theories/bi/notation.v

@@ -96,6 +96,13 @@ Reserved Notation "'[∗' 'list]' x ∈ l , P"
   (at level 200, l at level 10, x at level 1, right associativity,
    format "[∗  list]  x  ∈  l ,  P").
 
+Reserved Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P"
+  (at level 200, l1, l2 at level 10, k, x1, x2 at level 1, right associativity,
+   format "[∗  list]  k ↦ x1 ; x2  ∈  l1 ; l2 ,  P").
+Reserved Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P"
+  (at level 200, l1, l2 at level 10, x1, x2 at level 1, right associativity,
+   format "[∗  list]  x1 ; x2  ∈  l1 ; l2 ,  P").
+
 Reserved Notation "'[∗]' Ps" (at level 20).
 
 Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P"

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.

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)) →

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.

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 _ _ _)) =>