Commit 623adc39 authored by Robbert Krebbers's avatar Robbert Krebbers

Factor out lemma for initializing `gen_heap`.

parent 365fca38
...@@ -72,6 +72,14 @@ Section to_gen_heap. ...@@ -72,6 +72,14 @@ Section to_gen_heap.
Proof. by rewrite /to_gen_heap fmap_delete. Qed. Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap. End to_gen_heap.
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
(|==> _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
Qed.
Section gen_heap. Section gen_heap.
Context `{gen_heapG L V Σ}. Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
......
...@@ -19,9 +19,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ : ...@@ -19,9 +19,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
adequate e σ φ. adequate e σ φ.
Proof. Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh". iMod (gen_heap_init σ) as (?) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. } iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ γ).
iApply (Hwp (HeapG _ _ _)). iApply (Hwp (HeapG _ _ _)).
Qed. Qed.
Markdown is supported
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