From 79cd8d45aa4b717611f0da6af1ee9a2a90383ed8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 18:15:42 +0100
Subject: [PATCH] one gen_heap_init lemma is enough

---
 CHANGELOG.md                       |  2 ++
 theories/base_logic/lib/gen_heap.v | 20 +++++++-------------
 theories/heap_lang/adequacy.v      |  2 +-
 3 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4ef9d3724..61ee78e40 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -128,6 +128,8 @@ With this release, we dropped support for Coq 8.9.
   by `gen_heap`.
 * Strengthen `mapsto_valid_2` conclusion from `✓ (q1 + q2)%Qp` to
   `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`.
+* Change `gen_heap_init` to also return ownership of the points-to facts for the
+  initial heap.
 
 **Changes in `program_logic`:**
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 843030241..758234e4c 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -290,24 +290,18 @@ Section gen_heap.
   Qed.
 End gen_heap.
 
-(** This lemma drops ownership of the initial [σ] on the floor; see
-[gen_heap_init_big] for a version of the lemma that preserves this ownership. *)
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
-  ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
+  ⊢ |==> ∃ _ : gen_heapG L V Σ,
+    gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
-  iMod (own_alloc (gmap_view_auth 1 (σ : gmap L (leibnizO V)))) as (γh) "Hh".
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO V)))) as (γh) "Hh".
   { exact: gmap_view_auth_valid. }
   iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
   { exact: gmap_view_auth_valid. }
-  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
-  iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
-Qed.
-
-Lemma gen_heap_init_big `{Countable L, !gen_heapPreG L V Σ} σ :
-  ⊢ |==> ∃ _ : gen_heapG L V Σ,
-    gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
-Proof.
-  iMod (gen_heap_init ∅) as (gen_heap) "Hinterp". iExists gen_heap.
+  pose (gen_heap := GenHeapG L V Σ _ _ _ _ _ γh γm).
+  iExists gen_heap.
+  iAssert (gen_heap_interp ∅) with "[Hh Hm]" as "Hinterp".
+  { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
   iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
   { apply map_disjoint_empty_r. }
   rewrite right_id_L. done.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 1c6666270..ed24c8ae3 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -21,7 +21,7 @@ Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
-  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
+  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iModIntro. iExists
-- 
GitLab