From 0cc2c6e098bfb05c056783b9212c9218fa46aa5e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Dec 2016 20:21:45 +0100
Subject: [PATCH] Add lemma gen_heap_dealloc.

---
 theories/program_logic/gen_heap.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/program_logic/gen_heap.v b/theories/program_logic/gen_heap.v
index fad163a12..826a62ddf 100644
--- a/theories/program_logic/gen_heap.v
+++ b/theories/program_logic/gen_heap.v
@@ -68,6 +68,9 @@ Section gen_heap.
   Lemma to_gen_heap_insert l v σ :
     to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
   Proof. by rewrite /to_gen_heap fmap_insert. Qed.
+  Lemma to_gen_heap_delete l σ :
+    to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
+  Proof. by rewrite /to_gen_heap fmap_delete. Qed.
 
   (** General properties of mapsto *)
   Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).
@@ -121,6 +124,14 @@ Section gen_heap.
     iModIntro. rewrite to_gen_heap_insert. iFrame.
   Qed.
 
+  Lemma gen_heap_dealloc σ l v :
+    gen_heap_ctx σ -∗ l ↦ v ==∗ gen_heap_ctx (delete l σ).
+  Proof.
+    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
+    eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
+  Qed.
+
   Lemma gen_heap_valid σ l q v : gen_heap_ctx σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
     iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
-- 
GitLab