Commit 53c8199e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

A tactic `wp_simpl` that only `simpl`s the `e` in `WP e @ E {{ Φ }}`.

parent e9f14405
...@@ -5,6 +5,13 @@ From iris.heap_lang Require Export tactics lifting. ...@@ -5,6 +5,13 @@ From iris.heap_lang Require Export tactics lifting.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
Ltac wp_simpl :=
try iStartProof;
try lazymatch goal with
| |- envs_entails ?Δ (wp ?E ?e ?Q) =>
let e' := eval simpl in e in change (envs_entails Δ (wp E e' Q))
end.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ : Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ :
PureExec φ e1 e2 PureExec φ e1 e2
φ φ
...@@ -155,7 +162,7 @@ Tactic Notation "wp_apply" open_constr(lem) := ...@@ -155,7 +162,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch goal with lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => | |- envs_entails _ (wp ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApplyHyp H; try iNext; simpl) || wp_bind_core K; iApplyHyp H; try iNext; wp_simpl) ||
lazymatch iTypeOf H with lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P | Some (_,?P) => fail "wp_apply: cannot apply" P
end end
...@@ -174,7 +181,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) := ...@@ -174,7 +181,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
|first [intros l | fail 1 "wp_alloc:" l "not fresh"]; |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split; eexists; split;
[env_cbv; reflexivity || fail "wp_alloc:" H "not fresh" [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
|simpl; try wp_value_head]] |wp_simpl; try wp_value_head]]
| _ => fail "wp_alloc: not a 'wp'" | _ => fail "wp_alloc: not a 'wp'"
end. end.
...@@ -191,7 +198,7 @@ Tactic Notation "wp_load" := ...@@ -191,7 +198,7 @@ Tactic Notation "wp_load" :=
[apply _ [apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
|simpl; try wp_value_head] |wp_simpl; try wp_value_head]
| _ => fail "wp_load: not a 'wp'" | _ => fail "wp_load: not a 'wp'"
end. end.
...@@ -207,7 +214,7 @@ Tactic Notation "wp_store" := ...@@ -207,7 +214,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity |env_cbv; reflexivity
|simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]] |wp_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
| _ => fail "wp_store: not a 'wp'" | _ => fail "wp_store: not a 'wp'"
end. end.
...@@ -223,7 +230,7 @@ Tactic Notation "wp_cas_fail" := ...@@ -223,7 +230,7 @@ Tactic Notation "wp_cas_fail" :=
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
|try congruence |try congruence
|simpl; try wp_value_head] |wp_simpl; try wp_value_head]
| _ => fail "wp_cas_fail: not a 'wp'" | _ => fail "wp_cas_fail: not a 'wp'"
end. end.
...@@ -240,6 +247,6 @@ Tactic Notation "wp_cas_suc" := ...@@ -240,6 +247,6 @@ Tactic Notation "wp_cas_suc" :=
iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
|try congruence |try congruence
|env_cbv; reflexivity |env_cbv; reflexivity
|simpl; try wp_value_head] |wp_simpl; try wp_value_head]
| _ => fail "wp_cas_suc: not a 'wp'" | _ => fail "wp_cas_suc: not a 'wp'"
end. end.
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