introduce tactics for lambda and the further derived forms; make sp_seq consistent with the rest

barrier/barrier.v

@@ -148,7 +148,7 @@ Section proof.
     (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l))
     ⊑ || newchan '() {{ Φ }}.
   Proof.
-    rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
+    rewrite /newchan. wp_seq.
     rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
     apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
     rewrite !assoc. apply pvs_wand_r.
@@ -206,7 +206,7 @@ Section proof.
     heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ || signal (LocV l) {{ Φ }}.
   Proof.
     intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
-    apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
+    apply exist_elim=>γ. wp_let.
     (* I think some evars here are better than repeating *everything* *)
     eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
       eauto with I ndisj.

heap_lang/derived.v

@@ -26,15 +26,13 @@ Lemma wp_let' E x e1 e2 v Φ :
   ▷ || subst e2 x v @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}.
 Proof. apply wp_lam'. Qed.
 
-Lemma wp_seq E e1 e2 Φ :
-  || e1 @ E {{ λ _, ▷ || e2 @ E {{ Φ }} }} ⊑ || Seq e1 e2 @ E {{ Φ }}.
-Proof.
-  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
-  by rewrite -wp_let' //= ?to_of_val ?subst_empty.
-Qed.
+Lemma wp_seq E e1 e2 v Φ :
+  to_val e1 = Some v →
+  ▷ || e2 @ E {{ Φ }} ⊑ || Seq e1 e2 @ E {{ Φ }}.
+Proof. intros ?. rewrite -wp_let' // subst_empty //. Qed.
 
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ || Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.
+Proof. rewrite -wp_seq // -wp_value //. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
   (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →

heap_lang/tests.v

@@ -34,9 +34,9 @@ Section LiftingTests.
   Proof.
     rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
     wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
-    wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
+    wp_let. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
     wp_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
-    wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
+    wp_seq. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
       by apply const_intro.
   Qed.
 
@@ -57,7 +57,7 @@ Section LiftingTests.
     wp_rec>.
     (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
     rewrite ->(later_intro (Φ _)); rewrite -!later_and; apply later_mono.
-    wp_rec. wp_op. wp_rec. wp_op=> ?; wp_if.
+    wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
     - wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
@@ -65,7 +65,7 @@ Section LiftingTests.
 
   Lemma Pred_spec n E Φ : ▷ Φ (LitV (n - 1)) ⊑ || Pred 'n @ E {{ Φ }}.
   Proof.
-    wp_rec>; apply later_mono; wp_op=> ?; wp_if.
+    wp_lam>; apply later_mono; wp_op=> ?; wp_if.
     - wp_op. wp_op.
       ewp apply FindPred_spec.
       apply and_intro; first auto with I omega.
@@ -76,7 +76,7 @@ Section LiftingTests.
   Lemma Pred_user E :
     (True : iProp) ⊑ || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}.
   Proof.
-    intros. ewp apply Pred_spec. wp_rec. ewp apply Pred_spec. auto with I.
+    intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
   Qed.
 End LiftingTests.
 

heap_lang/wp_tactics.v

@@ -47,6 +47,21 @@ Tactic Notation "wp_rec" ">" :=
   end.
 Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
 
+Tactic Notation "wp_lam" ">" :=
+  match goal with
+  | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval cbv in e' with
+    | App (Rec "" _ _) _ =>
+       wp_bind K; etransitivity; [|eapply wp_lam; reflexivity]; wp_finish
+    end)
+  end.
+Tactic Notation "wp_lam" := wp_lam>; wp_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" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>