Remove wp_X> tactics and improve wp_finish.

Since strip_later is doing a good job stripping laters in the conclusion,
these tactics are thus no longer needed. Also, wp_finish now properly
converts the result in a primitive viewshift in case it is not a weakestpre.

heap_lang/lib/barrier/proof.v

@@ -219,7 +219,7 @@ Proof.
   ecancel [▷ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I.
   apply wand_intro_l.  set savedΨ := _ i (Ψ _). set savedQ := _ i Q.
   to_front [savedΨ; savedQ]. rewrite saved_prop_agree /=.
-  wp_op; [|done]=> _. wp_if. rewrite !assoc. eapply wand_apply_r'; first done.
+  wp_op; [|done]=> _. wp_if. rewrite -pvs_intro. rewrite !assoc. eapply wand_apply_r'; first done.
   eapply wand_apply_r'; first done.
   apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
 Qed.

heap_lang/lib/spawn.v

@@ -69,7 +69,7 @@ Proof.
   rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
   ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
   sep_split left: [_ -★ _; inv _ _; own _ _; heap_ctx _]%I.
-  - wp_seq. eapply wand_apply_l; [done..|].
+  - wp_seq. rewrite -pvs_intro. eapply wand_apply_l; [done..|].
     rewrite /join_handle. rewrite const_equiv // left_id -(exist_intro γ).
     solve_sep_entails.
   - wp_focus (f _). rewrite wp_frame_r wp_frame_l.

heap_lang/wp_tactics.v

@@ -8,22 +8,23 @@ Ltac wp_bind K :=
   | [] => idtac
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
+
 Ltac wp_finish :=
-  let rec go :=
-  match goal with
-  | |- _ ⊢ ▷ _ => etrans; [|fast_by apply later_mono; go]
-  | |- _ ⊢ wp _ _ _ =>
-    etrans; [|eapply wp_value_pvs; fast_done];
-    (* sometimes, we will have to do a final view shift, so only apply
-    pvs_intro if we obtain a consecutive wp *)
-    try (eapply pvs_intro;
-         match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
-  | _ => idtac
-  end in simpl; intros_revert go.
+  intros_revert ltac:(
+    try strip_later;
+    match goal with
+    | |- _ ⊢ wp _ _ _ =>
+      etrans; [|eapply wp_value_pvs; fast_done]; lazy beta;
+      (* sometimes, we will have to do a final view shift, so only apply
+      pvs_intro if we obtain a consecutive wp *)
+      try (etrans; [|apply pvs_intro];
+           match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
+    | _ => idtac
+    end).
 
 Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
 
-Tactic Notation "wp_rec" ">" :=
+Tactic Notation "wp_rec" :=
   löb ltac:(
     (* Find the redex and apply wp_rec *)
     idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
@@ -35,9 +36,8 @@ Tactic Notation "wp_rec" ">" :=
       wp_bind K; etrans; [|eapply wp_rec'; wp_done]; simpl_subst; wp_finish
 (*      end *) end)
      end).
-Tactic Notation "wp_rec" := wp_rec>; try strip_later.
 
-Tactic Notation "wp_lam" ">" :=
+Tactic Notation "wp_lam" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
@@ -45,14 +45,11 @@ Tactic Notation "wp_lam" ">" :=
     wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
 (*    end *) end)
   end.
-Tactic Notation "wp_lam" := wp_lam>; try strip_later.
 
-Tactic Notation "wp_let" ">" := wp_lam>.
 Tactic Notation "wp_let" := wp_lam.
-Tactic Notation "wp_seq" ">" := wp_let>.
 Tactic Notation "wp_seq" := wp_let.
 
-Tactic Notation "wp_op" ">" :=
+Tactic Notation "wp_op" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
@@ -65,9 +62,8 @@ Tactic Notation "wp_op" ">" :=
        wp_bind K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish
     end)
   end.
-Tactic Notation "wp_op" := wp_op>; try strip_later.
 
-Tactic Notation "wp_proj" ">" :=
+Tactic Notation "wp_proj" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
@@ -75,9 +71,8 @@ Tactic Notation "wp_proj" ">" :=
     | Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
     end)
   end.
-Tactic Notation "wp_proj" := wp_proj>; try strip_later.
 
-Tactic Notation "wp_if" ">" :=
+Tactic Notation "wp_if" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with If _ _ _ =>
@@ -85,9 +80,8 @@ Tactic Notation "wp_if" ">" :=
     etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
     end)
   end.
-Tactic Notation "wp_if" := wp_if>; try strip_later.
 
-Tactic Notation "wp_case" ">" :=
+Tactic Notation "wp_case" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with Case _ _ _ =>
@@ -96,7 +90,6 @@ Tactic Notation "wp_case" ">" :=
       wp_finish
     end)
   end.
-Tactic Notation "wp_case" := wp_case>; try strip_later.
 
 Tactic Notation "wp_focus" open_constr(efoc) :=
   match goal with
@@ -104,13 +97,12 @@ Tactic Notation "wp_focus" open_constr(efoc) :=
     match e' with efoc => unify e' efoc; wp_bind K end)
   end.
 
-Tactic Notation "wp" ">" tactic(tac) :=
+Tactic Notation "wp" tactic(tac) :=
   match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    wp_bind K; tac; [try strip_later|..])
   end.
-Tactic Notation "wp" tactic(tac) := (wp> tac); [try strip_later|..].
 
 (* In case the precondition does not match.
    TODO: Have one tactic unifying wp and ewp. *)
 Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
-Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).

tests/heap_lang.v

@@ -46,11 +46,11 @@ Section LiftingTests.
     n1 < n2 → 
     Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
-    revert n1. wp_rec=>n1 Hn.
+    revert n1. wp_rec=> n1 Hn.
     wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id -always_wand_impl always_elim wand_elim_r.
-    - assert (n1 = n2 - 1) as -> by omega; auto with I.
+    - rewrite -pvs_intro. assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
   Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.

tests/one_shot.v

@@ -54,6 +54,7 @@ Proof.
   { ecancel [heap_ctx _; ∀ _, _]%I. rewrite -inv_alloc // -later_intro.
     apply or_intro_l'. solve_sep_entails. }
   rewrite pvs_frame_r pvs_frame_l; apply wp_strip_pvs; wp_let.
+  rewrite -pvs_intro.
   rewrite !assoc 2!forall_elim; eapply wand_apply_r'; first done.
   rewrite (always_sep_dup (_ ★ _)); apply sep_mono.
   - apply forall_intro=>n. apply: always_intro. wp_let.
@@ -105,10 +106,10 @@ Proof.
         rewrite -(exist_intro n) {1}(always_sep_dup (own _ _)).
         solve_sep_entails. }
     cancel [one_shot_inv γ l].
-    wp_let. apply: always_intro. wp_seq.
+    wp_let. rewrite -pvs_intro. apply: always_intro. wp_seq.
     rewrite !sep_or_l; apply or_elim.
     { rewrite assoc.
-      apply const_elim_sep_r=>->. wp_case; wp_seq; eauto with I. }
+      apply const_elim_sep_r=>->. wp_case; wp_seq; rewrite -pvs_intro; eauto with I. }
     rewrite !sep_exist_l; apply exist_elim=> n.
     rewrite [(w=_ ★ _)%I]comm !assoc; apply const_elim_sep_r=>->.
     (* FIXME: why do we need to fold? *)