From 63b05e9b439499ed4c657397ab25f83e57f09fc2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Oct 2020 20:12:44 +0100
Subject: [PATCH] Make `wp_apply` perform `wp_pure` in small steps until the
 lemma matches the goal.

---
 tests/heap_lang_proph.v        |  2 +-
 theories/heap_lang/proofmode.v | 19 ++++++++++++++-----
 2 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 109958a5c..3052cf2ef 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -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.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 39f21d758..38076802b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -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
-- 
GitLab