Commit 63b05e9b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

parent 832a63d6
......@@ -47,7 +47,7 @@ Section tests.
Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E
{{{ RET #0 ; vs1' vs2', vs1 = (#0, #1)::vs1' vs2 = (#0, #2)::vs2' proph p1 vs1' proph p2 vs2' }}}.
Proof.
iIntros (Φ) "[Hp1 Hp2] HΦ".
iIntros (Φ) "[Hp1 Hp2] HΦ". wp_pures.
wp_apply (wp_resolve with "Hp1"); first done.
wp_apply (wp_resolve with "Hp2"); first done.
wp_op.
......
......@@ -482,19 +482,28 @@ End heap.
[wp_bind K; tac H] for every possible evaluation context. [tac] can do
[iApplyHyp H] to actually apply the hypothesis. TC resolution of [lem] premises
happens *after* [tac H] got executed. *)
Ltac wp_pures_reshape_expr tac :=
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[ reshape_expr e ltac:(fun K e' => wp_bind_core K; tac K e')
| wp_pure _; [wp_pures_reshape_expr tac] ]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[ reshape_expr e ltac:(fun K e' => twp_bind_core K; tac K e')
| wp_pure _; [wp_pures_reshape_expr tac] ]
end.
Tactic Notation "wp_apply_core" open_constr(lem) tactic3(tac) :=
wp_pures;
iPoseProofCore lem as false (fun H =>
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
wp_bind_core K; tac H) ||
wp_pures_reshape_expr ltac:(fun K e' => tac H) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
twp_bind_core K; tac H) ||
wp_pures_reshape_expr ltac:(fun K e' => tac H) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
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