Commit 795d9e57 authored by Ralf Jung's avatar Ralf Jung
Browse files

slightly optimize eauto fuel

parent 00cc5b5a
...@@ -23,7 +23,7 @@ Lemma wp_alloc_pst E σ e v Q : ...@@ -23,7 +23,7 @@ Lemma wp_alloc_pst E σ e v Q :
Proof. Proof.
intros. set (φ v' σ' := l, v' = LocV l σ' = <[l:=v]>σ σ !! l = None). intros. set (φ v' σ' := l, v' = LocV l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
last by intros; inv_step; eauto 10. last by intros; inv_step; eauto 8.
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l. apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
rewrite always_and_sep_l' -associative -always_and_sep_l'. rewrite always_and_sep_l' -associative -always_and_sep_l'.
......
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