Commit 3845293e authored by Ralf Jung's avatar Ralf Jung

proof tuning

parent 0e4b3598
...@@ -28,13 +28,13 @@ Lemma wp_alloc_pst E σ e v Φ : ...@@ -28,13 +28,13 @@ Lemma wp_alloc_pst E σ e v Φ :
( ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) - Φ (LocV l))) ( ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) - Φ (LocV l)))
WP Alloc e @ E {{ Φ }}. WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros {?} "[HP HΦ]".
(* TODO: This works around ssreflect bug #22. *) (* TODO: This works around ssreflect bug #22. *)
intros. set (φ (e' : expr []) σ' ef := l, set (φ (e' : expr []) σ' ef := l,
ef = None e' = Loc l σ' = <[l:=v]>σ σ !! l = None). ef = None e' = Loc l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ; iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
last (by intros; inv_head_step; eauto 8); last (by simpl; eauto). [by intros; subst φ; inv_head_step; eauto 8|].
iIntros "[HP HΦ]". iFrame "HP". iNext. iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
iIntros {v2 σ2 ef} "[% HP]".
(* FIXME: I should not have to refer to "H0". *) (* FIXME: I should not have to refer to "H0". *)
destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl. destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
iSplit; last done. iApply "HΦ"; by iSplit. iSplit; last done. iApply "HΦ"; by iSplit.
......
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