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

heap_lang: try to use cancel

parent b94d1262
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 2 deletions
heap_lang/heap.v
+ 3
− 2
View file @ a2e945d9
...@@ -116,8 +116,9 @@ Section heap. ...@@ -116,8 +116,9 @@ Section heap.
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.
rewrite -of_heap_insert left_id right_id !assoc. rewrite -of_heap_insert left_id right_id.
apply sep_mono_l. (* FIXME: cancel (auth_own heap_name {[l := Excl v]} -★ Φ (LocV l))%I. *)
rewrite !assoc. apply sep_mono_l.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None. rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv ?left_id; last by apply (map_insert_valid h). rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
apply later_intro. apply later_intro.
......
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