Commit 1fb1b2c7 authored by Dan Frumin's avatar Dan Frumin Committed by Robbert Krebbers
Browse files

Reorder the assumptions for `tac_wp_pure`

This way `IntoLaterNEnvs` is ought to be computed less frequently
parent 9c8e7799
...@@ -40,9 +40,9 @@ Ltac wp_pure_done := ...@@ -40,9 +40,9 @@ Ltac wp_pure_done :=
end. end.
Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ : Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
IntoLaterNEnvs 1 Δ Δ'
PureExec φ e1 e2 PureExec φ e1 e2
φ φ
IntoLaterNEnvs 1 Δ Δ'
(Δ' WP fill K e2 @ E {{ Φ }}) (Δ' WP fill K e2 @ E {{ Φ }})
(Δ WP fill K e1 @ E {{ Φ }}). (Δ WP fill K e1 @ E {{ Φ }}).
Proof. Proof.
...@@ -55,12 +55,11 @@ Tactic Notation "wp_pure" open_constr(efoc) := ...@@ -55,12 +55,11 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof; iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
let e'' := eval hnf in e' in unify e' efoc;
unify e'' efoc;
eapply (tac_wp_pure K); eapply (tac_wp_pure K);
[apply _ (* IntoLaters *) [unlock; simpl; apply _ (* PureExec *)
|unlock; simpl; apply _ (* PureExec *)
|wp_pure_done (* The pure condition for PureExec *) |wp_pure_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
|simpl_subst; try wp_value_head (* new goal *)]) |simpl_subst; try wp_value_head (* new goal *)])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct" || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'" | _ => fail "wp_pure: not a 'wp'"
......
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