From bdf3cc93a2bee992d149158220364e21ce27beb4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 13 Sep 2021 11:29:55 -0400
Subject: [PATCH] generalize to big_opL_take_drop

---
 iris/algebra/big_op.v | 10 ++++++++++
 iris/bi/big_op.v      |  9 ++-------
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index f6a7dd782..de29ac48c 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -104,6 +104,16 @@ Section list.
   Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
 
+  Lemma big_opL_take_drop Φ l n :
+    ([^o list] k ↦ x ∈ l, Φ k x) ≡
+    ([^o list] k ↦ x ∈ take n l, Φ k x) `o` ([^o list] k ↦ x ∈ drop n l, Φ (n + k) x).
+  Proof.
+    rewrite -{1}(take_drop n l) big_opL_app take_length.
+    destruct (decide (length l ≤ n)).
+    - rewrite drop_ge //=.
+    - rewrite Nat.min_l //=; lia.
+  Qed.
+
   Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M)
         l1 (l2 : list B) :
     R monoid_unit monoid_unit →
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index fa8cc1bfc..d0c0cca2d 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -98,15 +98,10 @@ 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:
+  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.
+  Proof. by rewrite big_opL_take_drop. Qed.
 
   Lemma big_sepL_submseteq (Φ : A → PROP) `{!∀ x, Affine (Φ x)} l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
-- 
GitLab