From a91d213be8e58d9630a3dc297507713094b8d800 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Sep 2021 17:30:17 -0400
Subject: [PATCH] add big_sepL_take_drop

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

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 9e82d6e39..fa8cc1bfc 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -98,6 +98,16 @@ Section sep_list.
     ([∗ list] k↦y ∈ l ++ [x], Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k y) ∗ Φ (length l) x.
   Proof. by rewrite big_opL_snoc. Qed.
 
+  Lemma big_sepL_take_drop Φ l n:
+    ([∗ list] k ↦ x ∈ l, Φ k x) ⊣⊢
+    ([∗ list] k ↦ x ∈ take n l, Φ k x) ∗ ([∗ list] k ↦ x ∈ drop n l, Φ (n + k) x).
+  Proof.
+    rewrite -{1}(take_drop n l) big_sepL_app take_length.
+    destruct (decide (length l ≤ n)).
+    - rewrite drop_ge //=.
+    - rewrite Nat.min_l //=; lia.
+  Qed.
+
   Lemma big_sepL_submseteq (Φ : A → PROP) `{!∀ x, Affine (Φ x)} l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
   Proof.
-- 
GitLab