Change `wp_apply` so it no longer performs `wp_pures`, and add new tactic `wp_smart_apply`

that performs `wp_pure` in small steps until the lemma matches the goal.

iris_heap_lang/lib/array.v

@@ -83,7 +83,7 @@ Section proof.
     iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]".
     iDestruct (array_cons with "Hsrc") as "[Hv2 Hsrc]".
     wp_load; wp_store.
-    wp_apply ("IH" with "[%] [%] Hdst Hsrc"); [ lia .. | ].
+    wp_smart_apply ("IH" with "[%] [%] Hdst Hsrc"); [ lia .. | ].
     iIntros "[Hvdst Hvsrc]".
     iApply "HΦ"; by iFrame.
   Qed.
@@ -107,7 +107,7 @@ Section proof.
     iIntros (Hvl Hn Φ) "Hvl HΦ".
     wp_lam.
     wp_alloc dst as "Hdst"; first by auto.
-    wp_apply (twp_array_copy_to with "[$Hdst $Hvl]").
+    wp_smart_apply (twp_array_copy_to with "[$Hdst $Hvl]").
     - rewrite replicate_length Z2Nat.id; lia.
     - auto.
     - iIntros "[Hdst Hl]".
@@ -147,7 +147,7 @@ Section proof.
       rewrite bool_decide_eq_false_2; last naive_solver lia.
       iDestruct (array_cons with "Hl") as "[Hl HSl]".
       iDestruct "Hf" as "[Hf HSf]".
-      wp_apply (wp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
+      wp_smart_apply (wp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
       rewrite Z.add_1_r -Nat2Z.inj_succ.
       iApply ("IH" with "[%] [HSl] HSf"); first lia.
       { by rewrite loc_add_assoc Z.add_1_r -Nat2Z.inj_succ. }
@@ -174,7 +174,7 @@ Section proof.
       rewrite bool_decide_eq_false_2; last naive_solver lia.
       iDestruct (array_cons with "Hl") as "[Hl HSl]".
       iDestruct "Hf" as "[Hf HSf]".
-      wp_apply (twp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
+      wp_smart_apply (twp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
       rewrite Z.add_1_r -Nat2Z.inj_succ.
       iApply ("IH" with "[%] [HSl] HSf"); first lia.
       { by rewrite loc_add_assoc Z.add_1_r -Nat2Z.inj_succ. }
@@ -195,7 +195,7 @@ Section proof.
       }}}.
     Proof.
       iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
-      wp_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
+      wp_smart_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
       { by rewrite /= Z2Nat.id; last lia. }
       { by rewrite loc_add_0. }
       iIntros "!>" (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
@@ -214,7 +214,7 @@ Section proof.
       }]].
     Proof.
       iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
-      wp_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
+      wp_smart_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
       { by rewrite /= Z2Nat.id; last lia. }
       { by rewrite loc_add_0. }
       iIntros (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.

iris_heap_lang/lib/assert.v

@@ -15,7 +15,7 @@ Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
   WP (assert: e)%V @ E [{ Φ }].
 Proof.
   iIntros "HΦ". wp_lam.
-  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
+  wp_smart_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
 
 Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
@@ -23,5 +23,5 @@ Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
   WP (assert: e)%V @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". wp_lam.
-  wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
+  wp_smart_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.

iris_heap_lang/lib/increment.v

@@ -63,7 +63,7 @@ Section increment.
     { (* abort case *) done. }
     iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
     (* Now go on *)
-    awp_apply cas_spec; first done.
+    wp_pures. awp_apply cas_spec; first done.
     (* Prove the atomic update for CAS *)
     rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
     iModIntro. iExists _. iFrame "Hl". iSplit.
@@ -87,7 +87,7 @@ Section increment.
     iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
     iIntros "$ !> AU !>".
     (* Now go on *)
-    awp_apply cas_spec; first done.
+    wp_pures. awp_apply cas_spec; first done.
     (* Prove the atomic update for CAS *)
     iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
@@ -118,7 +118,7 @@ Section increment.
   Proof.
     iIntros "Hl" (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
-    iIntros "Hl". awp_apply store_spec.
+    iIntros "Hl". wp_pures. awp_apply store_spec.
     (* Prove the atomic update for store *)
     iApply (aacc_aupd_commit with "AU"); first done.
     iIntros (x) "H↦".
@@ -155,7 +155,7 @@ Section increment_client.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
       done.
     }
-    wp_apply wp_par.
+    wp_smart_apply wp_par.
     - iAssumption.
     - iAssumption.
     - iIntros (??) "_ !>". done.

iris_heap_lang/lib/spawn.v

@@ -52,7 +52,7 @@ Proof.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { iNext. iExists NONEV. iFrame; eauto. }
-  wp_apply (wp_fork with "[Hf]").
+  wp_smart_apply (wp_fork with "[Hf]").
   - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
     wp_inj. iInv N as (v') "[Hl _]".
     wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
@@ -66,7 +66,7 @@ Proof.
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
-    wp_apply ("IH" with "Hγ [HΦ]"). auto.
+    wp_smart_apply ("IH" with "Hγ [HΦ]"). auto.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
     + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
       wp_pures. by iApply "HΦ".

iris_heap_lang/proofmode.v

@@ -512,30 +512,40 @@ Proof.
 Qed.
 End heap.
 
-(** Evaluate [lem] to a hypothesis [H] that can be applied, and then run
-[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. *)
-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) ||
-      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) ||
-      lazymatch iTypeOf H with
-      | Some (_,?P) => fail "wp_apply: cannot apply" P
-      end
-    | _ => fail "wp_apply: not a 'wp'"
-    end).
+(** The tactic [wp_apply_core lem tac_suc tac_fail] evaluates [lem] to a
+hypothesis [H] that can be applied, and then runs [wp_bind_core K; tac_suc H]
+for every possible evaluation context [K].
+
+- The tactic [tac_suc] should do [iApplyHyp H] to actually apply the hypothesis,
+  but can perform other operations in addition (see [wp_apply] and [awp_apply]
+  below).
+- The tactic [tac_fail cont] is called when [tac_suc H] fails for all evaluation
+  contexts [K], and can perform further operations before invoking [cont] to
+  try again.
+
+TC resolution of [lem] premises happens *after* [tac_suc H] got executed. *)
+Ltac wp_apply_core lem tac_suc tac_fail := first
+  [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_suc H)
+     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+       reshape_expr e ltac:(fun K e' =>
+         twp_bind_core K; tac_suc H)
+     | _ => fail 1 "wp_apply: not a 'wp'"
+     end)
+  |tac_fail ltac:(fun _ => wp_apply_core lem tac_suc tac_fail)
+  |let P := type of lem in
+   fail "wp_apply: cannot apply" lem ":" P ].
+
 Tactic Notation "wp_apply" open_constr(lem) :=
-  wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
+  wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl)
+                    ltac:(fun cont => fail).
+Tactic Notation "wp_smart_apply" open_constr(lem) :=
+  wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl)
+                    ltac:(fun cont => wp_pure _; []; cont ()).
+
 (** Tactic tailored for atomic triples: the first, simple one just runs
 [iAuIntro] on the goal, as atomic triples always have an atomic update as their
 premise.  The second one additionaly does some framing: it gets rid of [Hs] from
@@ -543,10 +553,13 @@ the context, which is intended to be the non-laterable assertions that iAuIntro
 would choke on.  You get them all back in the continuation of the atomic
 operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
-  wp_apply_core lem (fun H => iApplyHyp H);
+  wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
-  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]);
+  wp_apply_core lem
+    ltac:(fun H =>
+      iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]) 
+    ltac:(fun cont => fail);
   last iAuIntro.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=

tests/heap_lang.v

@@ -115,14 +115,14 @@ Section tests.
   Proof.
     iIntros "HΦ". wp_lam.
     wp_op. case_bool_decide.
-    - wp_apply FindPred_spec; first lia. wp_pures.
+    - wp_smart_apply FindPred_spec; first lia. wp_pures.
       by replace (n - 1)%Z with (- (-n + 2 - 1))%Z by lia.
-    - wp_apply FindPred_spec; eauto with lia.
+    - wp_smart_apply FindPred_spec; eauto with lia.
   Qed.
 
   Lemma Pred_user E :
     ⊢ WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }].
-  Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
+  Proof. iIntros "". wp_apply Pred_spec. by wp_smart_apply Pred_spec. Qed.
 
   Definition Id : val :=
     rec: "go" "x" :=

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.

tests/one_shot.v

@@ -84,7 +84,7 @@ Proof.
     iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
     iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
-    wp_apply wp_assert. wp_pures. by case_bool_decide.
+    wp_smart_apply wp_assert. wp_pures. by case_bool_decide.
 Qed.
 
 Lemma ht_one_shot (Φ : val → iProp Σ) :
@@ -95,8 +95,8 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
     }}.
 Proof.
   iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
-  - iIntros (n) "!> _". wp_apply "Hf1".
-  - iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
+  - iIntros (n) "!> _". wp_smart_apply "Hf1".
+  - iIntros "!> _". wp_smart_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
 Qed.
 End proof.
 
@@ -111,8 +111,8 @@ Section client.
   Lemma client_safe : ⊢ WP client {{ _, True }}.
   Proof using Type*.
     rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
-    wp_let. wp_apply wp_par.
-    - wp_apply "Hf1".
+    wp_let. wp_smart_apply wp_par.
+    - wp_smart_apply "Hf1".
     - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
       iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
     - auto.

tests/one_shot_once.v

@@ -113,8 +113,8 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
 Proof.
   iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
   iExists T. iFrame "HT". iSplit.
-  - iIntros (n) "!> HT". wp_apply "Hf1". done.
-  - iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
+  - iIntros (n) "!> HT". wp_smart_apply "Hf1". done.
+  - iIntros "!> _". wp_smart_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
 Qed.
 End proof.
 
@@ -129,8 +129,8 @@ Section client.
   Lemma client_safe : ⊢ WP client {{ _, True }}.
   Proof using Type*.
     rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
-    wp_let. wp_apply (wp_par with "[HT]").
-    - wp_apply "Hf1". done.
+    wp_let. wp_smart_apply (wp_par with "[HT]").
+    - wp_smart_apply "Hf1". done.
     - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
       iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
     - auto.

tests/tree_sum.v

@@ -57,7 +57,7 @@ Lemma sum_wp `{!heapG Σ} v t :
 Proof.
   iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
   wp_lam. wp_alloc l as "Hl".
-  wp_apply (sum_loop_wp with "[$Hl $Ht]").
+  wp_smart_apply (sum_loop_wp with "[$Hl $Ht]").
   rewrite Z.add_0_r.
   iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
 Qed.