From 020acf846aaf5fa367761cff22e7b74160ddc4b0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Nov 2016 15:49:11 +0100
Subject: [PATCH] Accessor like lemmas for big ops.

---
 base_logic/big_op.v | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index f47cab4de..586a1c56f 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -134,6 +134,12 @@ Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [∗] Ps ⊢ [∗] Qs.
 Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
 Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P.
 Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
+Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps).
+Proof.
+  intros (Ps1&Ps2&->)%elem_of_list_split.
+  rewrite !big_sep_app /=. rewrite assoc (comm _ _ P) -assoc.
+  by apply sep_mono_r, wand_intro_l.
+Qed.
 
 (** ** Persistence *)
 Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps).
@@ -327,9 +333,17 @@ Section gmap.
     ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y.
   Proof. apply: big_opM_delete. Qed.
 
+  Lemma big_sepM_lookup_acc Φ m i x :
+    m !! i = Some x →
+    ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ map] k↦y ∈ m, Φ k y)).
+  Proof.
+    intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
+  Qed.
+
   Lemma big_sepM_lookup Φ m i x :
     m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
-  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
+  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.
+
   Lemma big_sepM_lookup_dom (Φ : K → uPred M) m i :
     is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
   Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
@@ -469,6 +483,13 @@ Section gset.
   Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
   Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
 
+  Lemma big_sepS_elem_of_acc Φ X x :
+    x ∈ X →
+    ([∗ set] y ∈ X, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ set] y ∈ X, Φ y)).
+  Proof.
+    intros. rewrite big_sepS_delete //. by apply sep_mono_r, wand_intro_l.
+  Qed.
+
   Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
   Proof. apply: big_opS_singleton. Qed.
 
@@ -573,6 +594,13 @@ Section gmultiset.
   Lemma big_sepMS_elem_of Φ X x : x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊢ Φ x.
   Proof. intros. apply uPred_included. by apply: big_opMS_elem_of. Qed. 
 
+  Lemma big_sepMS_elem_of_acc Φ X x :
+    x ∈ X →
+    ([∗ mset] y ∈ X, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ mset] y ∈ X, Φ y)).
+  Proof.
+    intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
+  Qed.
+
   Lemma big_sepMS_singleton Φ x : ([∗ mset] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
   Proof. apply: big_opMS_singleton. Qed.
 
-- 
GitLab