From cc1191b9e28ac49309fa3cf27f253b0a61ba3bce Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2016 20:15:21 +0100
Subject: [PATCH] derive wp_load

---
 heap_lang/heap.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 660461722..56cf8e923 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -95,4 +95,13 @@ Section heap.
   { eexists. eauto. }
   Qed.
 
+  Lemma wp_load E γ l v P Q :
+    nclose N ⊆ E →
+    P ⊑ heap_ctx γ →
+    P ⊑ (heap_mapsto γ l v ★ ▷ (heap_mapsto γ l v -★ Q v)) →
+    P ⊑ wp E (Load (Loc l)) Q.
+  Proof.
+    intros HN. rewrite /heap_mapsto. apply wp_load_heap; first done.
+    by simplify_map_equality.
+  Qed.
 End heap.
-- 
GitLab