From c39795360c57789961907c87c974061135e18b42 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 5 Dec 2016 23:59:35 +0100
Subject: [PATCH] Accessor for big op on lists.

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

diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 639590a1e..0df566de9 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -229,6 +229,16 @@ Section list.
            (big_opL (M:=uPredUR M) l).
   Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
 
+  Lemma big_sepL_lookup_acc Φ l i x :
+    l !! i = Some x →
+    ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)).
+  Proof.
+    intros Hli. apply big_sep_elem_of_acc. revert Φ l Hli.
+    induction i as [|? IH]=>Φ [] //= y l; rewrite imap_cons.
+    - intros [=->]. constructor.
+    - intros ?. constructor. by apply (IH (_ ∘ S)).
+  Qed.
+
   Lemma big_sepL_lookup Φ l i x :
     l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
   Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
-- 
GitLab