Commit 79cd8d45 authored by Ralf Jung's avatar Ralf Jung
Browse files

one gen_heap_init lemma is enough

parent 3cb0702d
......@@ -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`:**
......
......@@ -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.
......
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment