Commit 73959011 authored by Ralf Jung's avatar Ralf Jung

fix heap

parent 0cbaab2f
Pipeline #139 passed with stage
...@@ -86,12 +86,14 @@ Section heap. ...@@ -86,12 +86,14 @@ Section heap.
apply to_heap_valid. } apply to_heap_valid. }
apply pvs_mono, exist_elim=> γ. apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r. rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
rewrite /heap_mapsto_def /heap_name.
induction σ as [|l v σ Hl IH] using map_ind. induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty; apply True_intro. } { rewrite big_sepM_empty; apply True_intro. }
rewrite to_heap_insert big_sepM_insert //. rewrite to_heap_insert big_sepM_insert //.
rewrite (map_insert_singleton_op (to_heap σ)); rewrite (map_insert_singleton_op (to_heap σ));
last rewrite lookup_fmap Hl; auto. last rewrite lookup_fmap Hl; auto.
by rewrite auth_own_op IH. (* FIXME: investigate why we have to unfold auth_own here. *)
by rewrite auth_own_op IH auth_own_eq.
Qed. Qed.
Context `{heapG Σ}. Context `{heapG Σ}.
......
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