More wp_ tactics

theories/examples/circ_buff/proof_gps.v

@@ -179,7 +179,7 @@ Proof.
 
   (* init indexes *)
   (* sequential reasoning *)
-  wp_let. wp_op. wp_write.
+  wp_pures. wp_write.
 
   iMod (GPS_iSP_Init (circbufN q) (consInt Ns γ q) (consInt Ns γ q false) _ O
           with "ori []") as (γj tj) "ConsP".
@@ -229,35 +229,33 @@ Proof.
               [solve_ndisj|done|done|by right|..].
   { by iIntros "!> !> #$". }
 
-  iIntros "(pW & Eq & #CEs)".
-  iDestruct "Eq" as %(w & ? & ?). subst vi w.
-  wp_let.
+  iIntros "(pW & Eq & #CEs)". iDestruct "Eq" as %(w & -> & ->).
+  wp_pures.
 
   (* read ri *)
-  wp_op. iDestruct "cR" as (tr vr γr) "#cR".
+  iDestruct "cR" as (tr vr γr) "#cR".
   wp_apply (GPS_iSP_Read (circbufN q) (consInt Ns γ q) (consInt Ns γ q false)
               (consInt Ns γ q false (q >> ri) γr) with "[$cR]");
               [solve_ndisj|done|done|by right|..].
   { iIntros "!>" (t' s' v' Lt') "!>"; iSplit; last iSplit; by iIntros "#$". }
 
   iIntros (t2 j rz) "([Lej _] & cR2 & Eq & #PEs)".
-  iDestruct "Eq" as %(r & ? & ?). subst rz r. iDestruct "Lej" as %Lej%inj_le.
+  iDestruct "Eq" as %(? & -> & ->). iDestruct "Lej" as %Lej%inj_le.
 
-  wp_let. wp_op. wp_op. wp_let. wp_op.
+  wp_pures.
 
   rewrite -!Nat2Z_inj_mod -(Nat2Z.inj_add _ 1)
           -Nat2Z_inj_mod Nat.add_mod_idemp_l; [|lia].
   case (bool_decide _) eqn:Eqr.
   - (* buffer full *)
-    wp_case. iApply "Post". iSplitR "P"; last by iRight.
+    wp_finish. iApply "Post". iSplitR "P"; last by iRight.
     iExists γ, i, j.
     iSplit; last iSplitL "pW"; last iSplitR "pToks"; [..|done].
     + iPureIntro. lia.
     + by iExists _, _, _.
     + by iExists _, _, _.
 
-  - wp_case. wp_op. wp_op.
-
+  - wp_pures.
     iDestruct (pToks_from_extract with "pToks") as "(iTok & pToks)".
     iPoseProof ("PEs" $! i with "[%]") as "PEi"; [lia|].
 

theories/examples/lock/proof_ticket_lock_gps.v

@@ -592,9 +592,8 @@ Proof.
       iSplit; iExists t; by iFrame "Eq".
     - iDestruct 1 as (t) "[#Eq F]". iSplitR ""; iExists t; by iFrame "Eq". }
   iIntros (t' [] v') "(_ & TCP' & %t & ->)".
-  wp_let. wp_op. wp_op.
+  wp_pures.
   rewrite Z.add_mod_idemp_l; [|lia].
-  wp_let.
 
   (* CAS *)
 
@@ -679,7 +678,7 @@ Proof.
   rewrite {3}/NSP (fixpoint_unfold (NSP' C P γ) _ _ _ _ _ _).
   iDestruct "NSP" as "[% #ES]". subst v3.
 
-  wp_let. wp_op.
+  wp_pures.
   case (decide (t `mod` Z.pos C = n3 `mod` Z.pos C)) => [Eq|NEq]; last first.
   { (* not our turn yet, keep waiting *)
     iExists 0. rewrite bool_decide_false; [|done]. iSplit; [done|].
@@ -753,8 +752,7 @@ Proof.
   rewrite {3}/NSP (fixpoint_unfold (NSP' C P γ) _ _ _ _ _ _).
   iDestruct "NSP" as "[% #ES]". subst v1.
 
-  wp_op. wp_op. wp_op.
-  rewrite Z.add_mod_idemp_l; [|lia].
+  wp_pures. rewrite Z.add_mod_idemp_l; [|lia].
 
   set Qi: vProp := NSP C P γ true (x >> 0) γn t1 t #(t `mod` Z.pos C).
   wp_apply (GPS_iSP_SWWrite_rel _ _ _ _ (λ _, True)%I Qi True%I _ _

theories/examples/mp/proof_gen_inv.v

@@ -52,8 +52,7 @@ Proof.
   iIntros (m) "(DEL & m & Hm)". rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "m" as "[m0 m1]".
   (* initializing *)
-  wp_let. wp_op. rewrite shift_0. wp_write.
-  wp_op. wp_write.
+  wp_pures. rewrite shift_0. wp_write. wp_op. wp_write.
 
   (* constructing the invariant *)
   iMod UTok_alloc as (γ) "Tok".
@@ -68,9 +67,7 @@ Proof.
   wp_apply (wp_fork with "[SW m1]"); [done|..].
   - iIntros "!>" (tid').
     (* write message *)
-    wp_op. wp_write.
-
-    wp_op. rewrite shift_0.
+    wp_op. wp_write. wp_op. rewrite shift_0.
     (* open shared invariant *)
     iInv (mpN m) as "INV" "Close". rewrite mp_inv'_eq.
     iDestruct "INV" as (ζ' b t0 V0 Vx0) "[>Pts _]".
@@ -150,7 +147,7 @@ Proof.
       iIntros "!>". iExists 1. iSplit; [done|].
       iIntros "!> !>".
 
-      wp_let. wp_op. wp_read. by iApply "Post".
+      wp_pures. wp_read. by iApply "Post".
 Qed.
 
 
@@ -188,8 +185,7 @@ Proof.
   iIntros (m) "(DEL & m & Hm)". rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "m" as "[m0 m1]".
   (* initializing *)
-  wp_let. wp_op. rewrite shift_0. wp_write.
-  wp_op. wp_write.
+  wp_pures. rewrite shift_0. wp_write. wp_op. wp_write.
 
   (* constructing the invariant *)
   iMod (AtomicPtsTo_from_na with "m0") as (γx t V) "(#SeenV & SW & Pts)".
@@ -300,7 +296,7 @@ Proof.
       iIntros "!>". iExists 1. iSplit; [done|]. simpl.
       iIntros "!> !>".
 
-      wp_let. wp_op. wp_read. wp_let.
+      wp_pures. wp_read. wp_let.
 
       iApply wp_hist_inv; [done|]. iIntros "HINV".
       iMod (AtomicPtsTo_to_na with "HINV Pts") as (t' v') "[m2 ?]"; [done|].

theories/examples/mp/proof_gps.v

@@ -46,8 +46,7 @@ Proof.
   iIntros (m) "(DEL & m & Hm)". rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "m" as "[m0 m1]".
   (* initializing *)
-  wp_let. wp_op. rewrite shift_0. wp_write.
-  wp_op. wp_write.
+  wp_pures. rewrite shift_0. wp_write. wp_op. wp_write.
 
   (* constructing protocol for m1 *)
   iMod UTok_alloc as (γ) "Tok".

theories/examples/mp/proof_reclaim_gps.v

@@ -47,7 +47,7 @@ Proof.
   rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "m" as "[m0 m1]".
   (* initializing *)
-  wp_let. wp_op. rewrite shift_0. wp_write.
+  wp_pures. rewrite shift_0. wp_write.
   wp_op. wp_write.
 
   (* constructing protocol for m1 *)

theories/examples/queue/proof_ms_gps.v

@@ -179,7 +179,7 @@ Proof.
   (* allocate first node *)
   wp_apply wp_new; [done..|].
   iIntros (s) "([H†|%] & Hs & Hm)"; [|done].
-  wp_let. wp_op. rewrite shift_0. rewrite own_loc_na_vec_singleton.
+  wp_pures. rewrite shift_0. rewrite own_loc_na_vec_singleton.
   (* initialize node, and create protocol *)
   iMod UTok_alloc as (γt) "Tok".
   wp_apply (GPS_iPP_Init_write (msqueLN s γt) (Link P γt) false s #null Null
@@ -189,23 +189,22 @@ Proof.
     iIntros (t γ) "!>".
     by rewrite /Link (fixpoint_unfold (Link' P) _ _ _ _ _ _ _). }
 
-  iIntros (γi ti) "#PPi". wp_let.
+  iIntros (γi ti) "#PPi". wp_seq.
   (* allocate head & tail *)
   wp_apply wp_new; [done..|].
   iIntros (q) "([H†|%] & Hq & Hmq)"; [|done].
   rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "Hq" as "[oH oT]".
   (* initialize head *)
-  wp_let. wp_op. rewrite shift_0.
+  wp_pures. rewrite shift_0.
   wp_apply (GPS_iPP_Init_write (msqueQN q) (Head P) false q #s ()
               with "[oH Tok]"); [done|..].
-  { iPoseProof (own_loc_na_own_loc with "oH") as "$".
+  { iDestruct (own_loc_na_own_loc with "oH") as "$".
     iIntros (t γ). iExists s. iSplit; [done|]. iExists γt.
     iFrame "Tok". iExists γi, ti. rewrite shift_0. by iFrame "PPi". }
 
-  iIntros (γh th) "PPh". wp_let.
+  iIntros (γh th) "PPh". wp_pures.
   (* initialize tail *)
-  wp_op.
   wp_apply (GPS_iPP_Init_write (msqueQN q) (Tail P) false (q >> tail) #s ()
               with "[oT]"); [done|..].
   { iPoseProof (own_loc_na_own_loc with "oT") as "$".
@@ -228,7 +227,7 @@ Lemma find_tail_spec q tid :
 Proof.
   iIntros (Φ) "#[oH oT] Post".
   iDestruct "oH" as (th vh γh) "PPh". iDestruct "oT" as (tl vl γl) "PPl".
-  wp_lam. wp_op.
+  wp_pures.
 
   (* read tail *)
   wp_apply (GPS_iPP_Read _ _ (Tail P false (q >> tail) γl)
@@ -238,8 +237,7 @@ Proof.
   iIntros (tl' [] vl') "(_ & PPl' & oT)".
   iDestruct "oT" as (n) "[% oT]". subst vl'.
   iDestruct "oT" as (γt γ' t') "oT".
-  wp_let. wp_op.
-
+  wp_pures.
   (* read node *)
   wp_apply (GPS_iPP_Read _ _ (Link P γt false (n >> link) γ') with "[$oT]");
     [solve_ndisj|done|done|by right| |].
@@ -250,14 +248,12 @@ Proof.
   rewrite {3}/Link (fixpoint_unfold (Link' P) _ _ _ _ _ _ _).
   destruct sn' as [[]|sn'].
   - (* found a probable tail *)
-    iDestruct "oL" as "%". subst vn'. wp_let. wp_op. wp_case.
-    iApply "Post". iRight.
+    iDestruct "oL" as "->". wp_pures. iApply "Post". iRight.
     iExists n. iSplit; [done|]. iExists γt, γ', tn'. iFrame "PPn".
   - (* haven't hit the last node, keep going *)
-    iDestruct "oL" as "[% oL]". subst vn'. wp_let. wp_op. wp_case.
-    wp_op.
-    iDestruct "oL" as (γt' v') "(ES & oL)".
+    iDestruct "oL" as "[-> oL]". iDestruct "oL" as (γt' v') "(ES & oL)".
     iDestruct "oL" as (γ1 t1) "oL".
+    wp_pures.
     wp_apply (GPS_iPP_Write _ _ _ _ _ _ (() : unitProtocol) _ #sn'
                 with "[$PPl oL]"); [solve_ndisj|done|done|by right|done|..].
     { iIntros "!>" (tl2 ?) "LL !>".
@@ -297,9 +293,9 @@ Proof.
   iIntros (n)  "([H†|%] & Hn & Hmn)"; [|done].
   rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "Hn" as "[oL oD]".
-  wp_let.
+  wp_pures.
   (* write data *)
-  wp_op. wp_write.
+  wp_write.
   (* initialize link *)
   wp_op. rewrite (shift_0 n). wp_write.
 
@@ -307,10 +303,9 @@ Proof.
   wp_bind (repeat: _)%E.
   iApply (find_tail_repeat_spec with "Queue").
   iIntros "!>" (l') "oL'". iDestruct "oL'" as (γt' γ' t') "oL'".
-  wp_let.
+  wp_pures.
 
   (* CAS to replace head *)
-  wp_op.
   set P' : vProp := (n ↦{1} #null ∗ P x ∗ (n >> data) ↦ #x)%I.
   wp_apply (GPS_iPP_CAS_int_simple _ _ _ _ _ _ _ null #n _ Null
               P' (λ _ _, ∃ γt t γ, GPS_iPP (msqueLN n γt) (Link P γt) n γ Null #null t)%I
@@ -352,17 +347,16 @@ Proof.
     - iIntros "!>" (v NE) "!>". by iSplit; iIntros "$". }
 
   iIntros (b t1 s1 v1) "[%Le1 CASE]".
-  iDestruct "CASE" as "[[(%&%&%) [PP' Q]]|[(%&%&%) (PP' & _ & oN & P & oD)]]".
-  - subst b v1. wp_case. wp_op.
+  iDestruct "CASE" as "[[(->&->&%) [PP' Q]]|[(->&%&%) (PP' & _ & oN & P & oD)]]".
+  - wp_pures.
     (* update tail with new node *)
-    iDestruct "Queue" as "[oH oT]".
-    iDestruct "oT" as (tl vl γl) "oT".
+    iDestruct "Queue" as "[oH oT]". iDestruct "oT" as (tl vl γl) "oT".
     wp_apply (GPS_iPP_Write _ _ _ _ _ _ (() : unitProtocol) _ #n
               with "[$oT Q]"); [solve_ndisj|done|done|by right|done|..].
     { iIntros "!>" (tl2 ?) "LL !>".
       iExists n. iSplit; [done|]. rewrite (shift_0 n). by iFrame "Q". }
     iIntros (t2) "PP2". wp_let. by iApply "Post".
-  - subst b. wp_case.
+  - wp_if.
     (* free the node *)
     wp_apply (wp_delete _ tid 2 _ [ #null; #x] with "[oN oD H†]"); [done|done|..].
     { rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. by iFrame. }
@@ -387,7 +381,7 @@ Lemma try_deq_spec q tid :
   {{{ (x: Z), RET #x; ⌜x = EMPTY⌝ ∨ ⌜x = FAIL_RACE⌝ ∨ P x }}}.
 Proof.
   iIntros (Φ) "#[oH oT] Post".
-  wp_lam. wp_op.
+  wp_pures.
   (* read head *)
   iDestruct "oH" as (th vh γh) "PPh".
   wp_apply (GPS_iPP_Read _ _ (Head P false (q >> head) γh)
@@ -398,7 +392,7 @@ Proof.
   iIntros (t1 [] v1) "(%Lt1 & PP1 & Hd)".
   iDestruct "Hd" as (s ?) "PPs". subst v1.
   iDestruct "PPs" as (γt) "[#PPs _]". iDestruct "PPs" as (γ' t') "PPs".
-  wp_let. wp_op.
+  wp_pures.
 
   (* read node's link *)
   wp_apply (GPS_iPP_Read _ _ (Link P γt false (s >> link) γ') with "[$PPs]");
@@ -411,12 +405,11 @@ Proof.
   rewrite {3}/Link (fixpoint_unfold (Link' P) _ _ _ _ _ _ _).
   destruct s2 as [[]|s2].
   - (* easy case: nothing to pop *)
-    iDestruct "Link" as %?. subst v2.
-    wp_op. wp_case. iApply "Post". by iLeft.
+    iDestruct "Link" as %?. subst v2. wp_pures. iApply "Post". by iLeft.
   - iDestruct "Link" as "[% os2]". subst v2.
     iDestruct "os2" as (γt2 v2) "#(ES & PPs2)".
     iDestruct "PPs2" as (γs2 ts2) "PPs2".
-    wp_op. wp_case. wp_op.
+    wp_pures.
 
     (* CAS on head *)
     set Q : time → unitProtocol → vProp :=
@@ -489,10 +482,10 @@ Proof.
 
   iIntros (b t3 [] v3) "(_ & _ & [((%&%&%) & PP' & HP)|((%&%&%) & PP' & _)])".
   + (* successful dequeue *)
-    subst b. wp_case. iDestruct "HP" as "[Hv HP]".
-    wp_op. wp_read. iApply "Post". by iRight; iRight.
+    subst b. iDestruct "HP" as "[Hv HP]".
+    wp_pures. wp_read. iApply "Post". by iRight; iRight.
   + (* fail, because losing a race against a concurrent try_deq *)
-    subst b. wp_case. iApply "Post". by iRight; iLeft.
+    subst b. wp_if. iApply "Post". by iRight; iLeft.
 Qed.
 
 Lemma dequeue_spec q tid :
@@ -502,9 +495,9 @@ Lemma dequeue_spec q tid :
 Proof.
   iIntros (Φ) "#Q Post". iLöb as "IH". wp_rec.
   wp_apply (try_deq_spec with "Q").
-  iIntros (x) "P". wp_let. wp_op. wp_if.
+  iIntros (x) "P". wp_pures.
   case_bool_decide.
-  - wp_value_head. iApply "Post". iDestruct "P" as "[%Eq0|[%Eqm|P]]".
+  - wp_finish. iApply "Post". iDestruct "P" as "[%Eq0|[%Eqm|P]]".
     + by rewrite decide_True.
     + lia.
     + by case_decide.

theories/examples/stack/proof_na.v

@@ -82,9 +82,9 @@ Proof.
   rewrite /NAStack_def (fixpoint_unfold (NAStack' P) _ _).
   iDestruct "Stack" as (h) "[oH oT]".
   rewrite shift_0. wp_read.
-  wp_let.
+  wp_pures.
   (* let new node point to the current head *)
-  wp_op. rewrite shift_0. wp_write.
+  rewrite shift_0. wp_write.
   (* update head to new node *)
   wp_write.
   (* finish *)
@@ -117,18 +117,17 @@ Proof.
   destruct A as [|v' A'].
   - (* empty stack, nothing to pop *)
     iDestruct "oT" as "%". subst h.
-    wp_op. wp_case.
+    wp_pures.
     iApply "Post". iSplit; [done|].
     rewrite /NAStack /NAStack_def (fixpoint_unfold (NAStack' P) _ _).
     iFrame "Hs†".
     iExists #0. rewrite shift_0. by iFrame.
   - (* popping v' *)
     iDestruct "oT" as (l') "(% & H† & od & P & oT)". subst h.
-    wp_op. wp_case.
+    wp_pures.
     (* read the data of the head element *)
-    wp_op. wp_read. wp_let.
+    wp_read. wp_pures.
     (* read the next of the head element *)
-    wp_op.
     rewrite /NAStack (fixpoint_unfold (NAStack' P) _ _).
     iDestruct "oT" as (h') "[on oT]".
     wp_read. wp_let.

theories/examples/stack/proof_treiber_gps.v

@@ -288,9 +288,9 @@ Proof.
   wp_apply wp_new; [done..|].
   iIntros (n) "([H†|%] & Hn & Hmn)"; [|done].
   (* write data to new node *)
-  wp_let. rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+  rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "Hn" as "[Hn Hd]".
-  wp_op. wp_write. wp_lam.
+  wp_pures. wp_write. wp_lam.
 
   iDestruct "Stack" as (γ ts vs) "#Stack".
   (* read possible head of stack *)
@@ -304,7 +304,7 @@ Proof.
   iDestruct "HD" as (s' ? A) "HD". subst v'.
 
   (* set the next field to the read head s' *)
-  wp_let. wp_op. rewrite shift_0. wp_write.
+  wp_pures. rewrite shift_0. wp_write.
 
   (* Case distinction: if s' is 0 (NULL), then this is a CAS without pointer
     comparison. Otherwise, we know from HD that s' is alive. We then only need
@@ -440,18 +440,17 @@ Proof.
   rewrite /ReachableD (fixpoint_unfold ReachableD' _ _).
   destruct A as [|h' A'].
   { (* s' is 0 (NULL), nothing to pop *)
-    iDestruct "HD" as "%". subst s'.
-    wp_op. wp_case. iApply "Post". by iLeft. }
+    iDestruct "HD" as "%". subst s'. wp_pures. iApply "Post". by iLeft. }
 
   (* From HD we know s' is alive *)
-  iDestruct "HD" as (s1 ? q) "[Hs1 HD]". subst s'.
+  iDestruct "HD" as (s1 -> q) "[Hs1 HD]".
   (* we are leaking fractions of s1 ("Hs1") and others ("HD") here.
     A non-leaking algorithm should have some way to retrieve this fraction.
     Then the setup in this proof will not work any more. *)
 
-  wp_op. wp_case.
+  wp_pures.
   (* read the next field of s1 *)
-  wp_op. wp_read. wp_let.
+  wp_read. wp_let.
 
   (* CAS-ing *)
   rewrite shift_0.
@@ -518,10 +517,10 @@ Proof.
   iIntros (Φ) "#S Post".
   iLöb as "IH". wp_rec. wp_bind (try_pop _)%E.
   iApply (try_pop_spec with "S").
-  iIntros "!>" (v) "P". wp_let. wp_op.
+  iIntros "!>" (v) "P". wp_pures.
   case_bool_decide.
-  - subst v. wp_if. by iApply ("IH" with "Post").
-  - wp_if. iApply "Post". case decide => ?; [done|].
+  - subst v. by iApply ("IH" with "Post").
+  - wp_finish. iApply "Post". case decide => ?; [done|].
     by iDestruct "P" as "[%|[%|P]]".
 Qed.
 End proof.

theories/logic/atomic_exchange.v

@@ -236,7 +236,7 @@ Proof.
   iIntros "sV sζ' Hrel" (Φ) "AU".
   iApply (AtomicSeen_CON_XCHG_aux_int _ _ _ _ _ _ (λ vr vn vw', vw' = vr + vn)
             with "sV sζ' Hrel"); [done..| |].
-  { clear. iIntros (vo vn tid Φ) "_ HΦ". wp_lam. wp_op. by iApply "HΦ". }
+  { clear. iIntros (vo vn tid Φ) "_ HΦ". wp_pures. by iApply "HΦ". }
   iAuIntro. iApply (aacc_aupd_commit with "AU"); [done|].
   iIntros (Vb ζ) "P".
   iAaccIntro with "P"; first by eauto with iFrame.

theories/logic/proofmode.v

@@ -11,12 +11,20 @@ From gpfsl.logic Require Export lifting.
 
 Require Import iris.prelude.options.
 
-Lemma tac_wp_value `{!noprolG Σ} Δ tid E Φ e v :
-  IntoVal e v →
-  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ tid; E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
+Lemma tac_wp_expr_eval `{!noprolG Σ} Δ tid E Φ e e' :
+  (∀ (e'':=e'), e = e'') →
+  envs_entails Δ (WP e' @ tid; E {{ Φ }}) → envs_entails Δ (WP e @ tid; E {{ Φ }}).
+Proof. by intros ->. Qed.
 
-Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
+Tactic Notation "wp_expr_eval" tactic3(t) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?tid ?E ?e ?Q) =>
+    notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _);
+      [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
+  | _ => fail "wp_expr_eval: not a 'wp'"
+  end.
+Ltac wp_expr_simpl := wp_expr_eval simpl.
 
 Lemma tac_wp_pure `{!noprolG Σ} K Δ Δ' tid E e1 e2 φ n Φ :
   (∀ 𝓥, PureExec φ n (e1 at 𝓥) (e2 at 𝓥)) →
@@ -36,20 +44,40 @@ Proof.
   iNext. by iApply ("H" with "[//] [$]").
 Qed.
 
+Lemma tac_wp_value `{!noprolG Σ} Δ tid E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ tid; E {{ Φ }}).
+Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
+
+Ltac wp_finish :=
+  wp_expr_simpl;      (* simplify occurences of subst/fill *)
+  try wp_value_head;  (* in case we have reached a value, get rid of the WP *)
+  pm_prettify.        (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
+                         λs caused by wp_value *)
+
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?tid ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
-    [simpl; apply _                 (* PureExec *)
+    [iSolveTC                       (* PureExec *)
     |try done                       (* The pure condition for PureExec *)
-    |apply _                        (* IntoLaters *)
-    |simpl_subst; try wp_value_head (* new goal *)])
+    |iSolveTC                       (* IntoLaters *)
+    |wp_finish                      (* new goal *)])
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
+Ltac wp_pures :=
+  iStartProof;
+  first [ (* The `;[]` makes sure that no side-condition magically spawns. *)
+          progress repeat (wp_pure _; [])
+        | wp_finish (* In case wp_pure never ran, make sure we do the usual cleanup. *)
+        ].
+
 Lemma tac_wp_eq_loc `{!noprolG Σ} K Δ Δ' tid E i1 i2 l1 l2 q1 q2 Φ :
   ↑histN ⊆ E →
   MaybeIntoLaterNEnvs 1 Δ Δ' →