From 3bc1f85324e345f9c88039a1aa1b0d3282b3f186 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Mar 2018 20:37:46 +0200
Subject: [PATCH] Short proof of `big_sepL_delete`.

This is a substitute for !136.
---
 theories/base_logic/big_op.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 3ff02f9d0..02d819a9a 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -149,6 +149,19 @@ Section list.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
+  Lemma big_sepL_delete Φ l i x :
+    l !! i = Some x →
+    ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y.
+  Proof.
+    intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
+    rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite pure_False; last by intros []. rewrite False_impl left_id.
+    rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
+    - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
+      rewrite take_length in Hk. by rewrite pure_True ?True_impl; last lia.
+    - apply big_sepL_proper=> k y _. by rewrite pure_True ?True_impl; last lia.
+  Qed.
+
   Global Instance big_sepL_nil_plain Φ : Plain ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_sepL_plain Φ l :
-- 
GitLab