From 41b9962fbbbc3f474cd00811d67d86cf8b0d93da Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Sep 2021 23:10:10 -0400
Subject: [PATCH] lemmas to merge a sepL and a sepL2

---
 iris/bi/big_op.v | 50 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 9e82d6e39..013adb6d5 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -568,6 +568,28 @@ Section sep_list2.
            (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_const_sepL_l (Φ : nat → A → PROP) (l1 : list A) (l2 : list B) :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1) ⊣⊢ ⌜length l1 = length l2⌝ ∧ ([∗ list] k↦y1 ∈ l1, Φ k y1).
+  Proof.
+    rewrite big_sepL2_alt.
+    trans (⌜length l1 = length l2⌝ ∧ [∗ list] k↦y1 ∈ (zip l1 l2).*1, Φ k y1)%I.
+    - rewrite big_sepL_fmap //.
+    - apply (anti_symm (⊢)); apply pure_elim_l=> Hl; rewrite fst_zip;
+      try (rewrite Hl //);
+      (apply and_intro; [by apply pure_intro|done]).
+  Qed.
+
+  Lemma big_sepL2_const_sepL_r (Φ : nat → B → PROP) (l1 : list A) (l2 : list B) :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y2) ⊣⊢ ⌜length l1 = length l2⌝ ∧ ([∗ list] k↦y2 ∈ l2, Φ k y2).
+  Proof.
+    rewrite big_sepL2_alt.
+    trans (⌜length l1 = length l2⌝ ∧ [∗ list] k↦y2 ∈ (zip l1 l2).*2, Φ k y2)%I.
+    - rewrite big_sepL_fmap //.
+    - apply (anti_symm (⊢)); apply pure_elim_l=> Hl; rewrite snd_zip;
+      try (rewrite Hl //);
+      (apply and_intro; [by apply pure_intro|done]).
+  Qed.
+
   Lemma big_sepL2_insert_acc Φ l1 l2 i x1 x2 :
     l1 !! i = Some x1 → l2 !! i = Some x2 →
     ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢
@@ -639,6 +661,34 @@ Section sep_list2.
     by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
   Qed.
 
+  Lemma big_sepL2_sep_sepL_l (Φ : nat → A → PROP) Ψ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 ∗ Ψ k y1 y2)
+    ⊣⊢ ([∗ list] k↦y1 ∈ l1, Φ k y1) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
+  Proof.
+    rewrite big_sepL2_sep big_sepL2_const_sepL_l. apply (anti_symm _).
+    - rewrite and_elim_r. done.
+    - rewrite !big_sepL2_alt [(_ ∗ _)%I]comm -!persistent_and_sep_assoc.
+      apply pure_elim_l=>Hl. apply and_intro.
+      { apply pure_intro. done. }
+      rewrite [(_ ∗ _)%I]comm. apply sep_mono; first done.
+      apply and_intro; last done.
+      apply pure_intro. done.
+  Qed.
+
+  Lemma big_sepL2_sep_sepL_r Φ (Ψ : nat → B → PROP) l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y2)
+    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y2 ∈ l2, Ψ k y2).
+  Proof.
+    rewrite big_sepL2_sep big_sepL2_const_sepL_r. apply (anti_symm _).
+    - rewrite and_elim_r. done.
+    - rewrite !big_sepL2_alt -!persistent_and_sep_assoc.
+      apply pure_elim_l=>Hl. apply and_intro.
+      { apply pure_intro. done. }
+      apply sep_mono; first done.
+      apply and_intro; last done.
+      apply pure_intro. done.
+  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).
-- 
GitLab