From f69e44a985dec2fbb61a492ebffc35b9a87008da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 28 May 2016 03:46:08 +0200
Subject: [PATCH] Deallocation is a local update.

---
 algebra/gmap.v | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/algebra/gmap.v b/algebra/gmap.v
index accb4f183..6753711e0 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -334,9 +334,18 @@ Qed.
 End freshness.
 
 (* Allocation is a local update: Just use composition with a singleton map. *)
-(* Deallocation is *not* a local update. The trouble is that if we
-   own {[ i ↦ x ]}, then the frame could always own "core x", and prevent
-   deallocation. *)
+
+Global Instance gmap_delete_update :
+  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ ∀ y, ¬ ✓{0} (x ⋅ y)) (delete i).
+Proof.
+  split; first apply _.
+  intros n m1 m2 (x&Hix&Hv) Hm j; destruct (decide (i = j)) as [<-|].
+  - rewrite lookup_delete !lookup_op lookup_delete.
+    case Hiy: (m2 !! i)=> [y|]; last constructor.
+    destruct (Hv y); apply cmra_validN_le with n; last omega.
+    move: (Hm i). by rewrite lookup_op Hix Hiy.
+  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
+Qed.
 
 (* Applying a local update at a position we own is a local update. *)
 Global Instance gmap_alter_update `{!LocalUpdate Lv L} i :
-- 
GitLab