Skip to content
Snippets Groups Projects
Commit bbb33095 authored by Ralf Jung's avatar Ralf Jung
Browse files

heap: slightly simplify

parent 595b0419
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
heap_lang/heap.v
+ 1
− 1
View file @ bbb33095
...@@ -102,7 +102,7 @@ Section heap. ...@@ -102,7 +102,7 @@ Section heap.
rewrite {1}[(▷ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs. rewrite {1}[(▷ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite /wp_fsa -(wp_alloc_pst _ (of_heap h)) //. rewrite /wp_fsa -(wp_alloc_pst _ (of_heap h)) //.
apply sep_mono_r; rewrite HP; apply later_mono. apply sep_mono_r; rewrite HP; apply later_mono.
apply forall_intro=> l; apply wand_intro_l; rewrite (forall_elim l). apply forall_mono=> l; apply wand_intro_l.
rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?. rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
rewrite -(exist_intro (op {[ l ↦ Excl v ]})). rewrite -(exist_intro (op {[ l ↦ Excl v ]})).
repeat erewrite <-exist_intro by apply _; simpl. repeat erewrite <-exist_intro by apply _; simpl.
......
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