From 4b2bf95fb61c86b2d06dd5480d683aa359f2c402 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Oct 2020 19:06:21 +0200
Subject: [PATCH] gmap_view: add deletion lemma
---
theories/algebra/lib/gmap_view.v | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 55f3962a1..abe12c6cf 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -237,6 +237,21 @@ Section lemmas.
rewrite lookup_insert_ne //.
Qed.
+ Lemma gmap_view_delete m k v :
+ gmap_view_auth m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
+ gmap_view_auth (delete k m).
+ Proof.
+ apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
+ destruct (decide (j = k)) as [->|Hne].
+ - edestruct (Hrel k) as (v' & _ & Hdf & _).
+ { rewrite lookup_op Hbf lookup_singleton -Some_op. done. }
+ exfalso. apply: dfrac_full_exclusive. apply Hdf.
+ - edestruct (Hrel j) as (v' & ? & ? & Hm).
+ { rewrite lookup_op lookup_singleton_ne // Hbf. done. }
+ exists v'. do 2 (split; first done).
+ rewrite lookup_delete_ne //.
+ Qed.
+
Lemma gmap_view_update m k v v' :
gmap_view_auth m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth (<[k := v']> m) â‹… gmap_view_frag k (DfracOwn 1) v'.
--
GitLab