From 6900258e8e88d7281d20aa4c6883214a00f74dff Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 12 Jan 2023 18:26:46 +0100
Subject: [PATCH] add 'wp_apply (...) as'

---
 CHANGELOG.md                          |  2 +
 docs/heap_lang.md                     | 18 +++---
 iris_heap_lang/lib/array.v            | 20 +++---
 iris_heap_lang/lib/clairvoyant_coin.v | 12 ++--
 iris_heap_lang/lib/increment.v        |  4 +-
 iris_heap_lang/lib/logatom_lock.v     |  6 +-
 iris_heap_lang/lib/par.v              |  8 +--
 iris_heap_lang/proofmode.v            | 92 +++++++++++++++++++++++++++
 8 files changed, 125 insertions(+), 37 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 43ed2e393..54539dc6a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -76,6 +76,8 @@ Coq 8.13 is no longer supported.
 **Changes in `heap_lang`:**
 
 * Move operations and lemmas about locations into a module `Loc`.
+* Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the
+  postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
 
 **LaTeX changes:**
 
diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index 23a2f04ac..f405d3547 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -104,14 +104,16 @@ Further tactics:
   particular when accessing invariants, which is only possible when the `WP` in
   the goal is for a single, atomic operation -- `wp_bind` can be used to bring
   the goal into the right shape.
-- `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
-  applying `wp_bind` as needed.  See the [ProofMode docs](./proof_mode.md) for an
-  explanation of `pm_trm`.
-- `wp_smart_apply pm_trm`: like `wp_apply`, but also performs pure reduction
-  steps to reveal a redex that matches `pm_trm`. Precisely, if applying the
-  lemma fails, `wp_smart_apply` will perform a step of pure reduction (via
-  `wp_pure`), and repeat. (This means that `wp_smart_apply` is not the same
-  as `wp_pures; wp_apply`.)
+- `wp_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  Apply a lemma whose conclusion is a `WP`, automatically applying `wp_bind` as
+  needed. The `as` clause is optional and can be used to introduce the
+  postcondition; this works particularly well for Texan triples. See the
+  [ProofMode docs](./proof_mode.md) for an explanation of `pm_trm` and `ipat`.
+- `wp_smart_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  like `wp_apply`, but also performs pure reduction steps to reveal a redex that
+  matches `pm_trm`. To be precise, if applying the lemma fails, `wp_smart_apply`
+  will perform a step of pure reduction (via `wp_pure`), and repeat. (This means
+  that `wp_smart_apply` is not the same as `wp_pures; wp_apply`.)
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
 
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index a55c84bb2..598c615cd 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -83,8 +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_smart_apply ("IH" with "[%] [%] Hdst Hsrc"); [ lia .. | ].
-    iIntros "[Hvdst Hvsrc]".
+    wp_smart_apply ("IH" with "[%] [%] Hdst Hsrc") as "[Hvdst Hvsrc]"; [ lia .. | ].
     iApply "HΦ"; by iFrame.
   Qed.
   Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
@@ -107,11 +106,10 @@ Section proof.
     iIntros (Hvl Hn Φ) "Hvl HΦ".
     wp_lam.
     wp_alloc dst as "Hdst"; first by auto.
-    wp_smart_apply (twp_array_copy_to with "[$Hdst $Hvl]").
+    wp_smart_apply (twp_array_copy_to with "[$Hdst $Hvl]") as "[Hdst Hl]".
     - rewrite replicate_length Z2Nat.id; lia.
     - auto.
-    - iIntros "[Hdst Hl]".
-      wp_pures.
+    - wp_pures.
       iApply "HΦ"; by iFrame.
   Qed.
   Lemma wp_array_clone stk E l dq vl n :
@@ -147,7 +145,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_smart_apply (wp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
+      wp_smart_apply (wp_wand with "Hf") as (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 +172,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_smart_apply (twp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
+      wp_smart_apply (twp_wand with "Hf") as (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,10 +193,10 @@ Section proof.
       }}}.
     Proof.
       iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
-      wp_smart_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Φ]") as "!> %vs".
       { by rewrite /= Z2Nat.id; last lia. }
       { by rewrite Loc.add_0. }
-      iIntros "!>" (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
+      iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
       iApply ("HΦ" $! _ vs). iModIntro. iSplit.
       { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
       rewrite Loc.add_0. iFrame.
@@ -214,10 +212,10 @@ Section proof.
       }]].
     Proof.
       iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
-      wp_smart_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Φ]") as "%vs".
       { by rewrite /= Z2Nat.id; last lia. }
       { by rewrite Loc.add_0. }
-      iIntros (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
+      iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
       iApply ("HΦ" $! _ vs). iModIntro. iSplit.
       { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
       rewrite Loc.add_0. iFrame.
diff --git a/iris_heap_lang/lib/clairvoyant_coin.v b/iris_heap_lang/lib/clairvoyant_coin.v
index 64fb01617..89adf062e 100644
--- a/iris_heap_lang/lib/clairvoyant_coin.v
+++ b/iris_heap_lang/lib/clairvoyant_coin.v
@@ -40,10 +40,8 @@ Section proof.
   Proof.
     iIntros (Φ) "_ HΦ".
     wp_lam.
-    wp_apply wp_new_proph; first done.
-    iIntros (vs p) "Hp".
-    wp_apply nondet_bool_spec; first done.
-    iIntros (b) "_".
+    wp_apply wp_new_proph as (vs p) "Hp"; first done.
+    wp_apply nondet_bool_spec as (b) "_"; first done.
     wp_alloc c as "Hc".
     wp_pair.
     iApply ("HΦ" $! (#c, #p)%V (b :: prophecy_to_list_bool vs)).
@@ -72,11 +70,9 @@ Section proof.
     iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
     destruct bs as [|b bs]; simplify_eq/=.
     wp_lam. do 2 (wp_proj; wp_let).
-    wp_apply nondet_bool_spec; first done.
-    iIntros (r) "_".
+    wp_apply nondet_bool_spec as (r) "_"; first done.
     wp_store.
-    wp_apply (wp_resolve_proph with "[Hp]"); first done.
-    iIntros (ws) "[-> Hp]".
+    wp_apply (wp_resolve_proph with "[Hp]") as (ws) "[-> Hp]"; first done.
     wp_seq.
     iApply "HΦ"; iSplitR; first done.
     destruct r; rewrite /coin; eauto 10 with iFrame.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 5e8eb17ed..4bfdddd20 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -130,8 +130,8 @@ Section increment.
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros "Hl" (Φ) "AU". wp_lam.
-    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
-    iIntros "Hl". wp_pures. awp_apply store_spec.
+    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl") as "Hl".
+    wp_pures. awp_apply store_spec.
     (* Prove the atomic update for store *)
     iApply (aacc_aupd_commit with "AU"); first done.
     iIntros (x) "H↦".
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index c086cbe59..cb6d7c23c 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -64,8 +64,7 @@ Section tada.
     replace 1%Qp with (3/4 + 1/4)%Qp; last first.
     { rewrite Qp.three_quarter_quarter //. }
     iDestruct "Hvar" as "[Hvar1 Hvar2]".
-    wp_apply (l.(newlock_spec) with "Hvar2").
-    iIntros (lk γlock) "Hlock".
+    wp_apply (l.(newlock_spec) with "Hvar2") as (lk γlock) "Hlock".
     iApply ("HΦ" $! lk (TadaLockName _ _)).
     iFrame.
   Qed.
@@ -77,8 +76,7 @@ Section tada.
     <<< ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked, RET #() >>>.
   Proof.
     iIntros "#Hislock %Φ AU". iApply wp_fupd.
-    wp_apply (l.(acquire_spec) with "Hislock").
-    iIntros "[Hlocked Hvar1]".
+    wp_apply (l.(acquire_spec) with "Hislock") as "[Hlocked Hvar1]".
     iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
     iCombine "Hvar1 Hvar2" gives %[_ <-].
     iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
diff --git a/iris_heap_lang/lib/par.v b/iris_heap_lang/lib/par.v
index 9645118f9..468c06aae 100644
--- a/iris_heap_lang/lib/par.v
+++ b/iris_heap_lang/lib/par.v
@@ -27,10 +27,10 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) (f1 f2 : val) (Φ : val → iProp Σ
   WP par f1 f2 {{ Φ }}.
 Proof.
   iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
-  wp_apply (spawn_spec parN with "Hf1").
-  iIntros (l) "Hl". wp_let. wp_bind (f2 _).
-  wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
-  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
+  wp_apply (spawn_spec parN with "Hf1") as (l) "Hl".
+  wp_let. wp_bind (f2 _).
+  wp_apply (wp_wand with "Hf2") as (v) "H2". wp_let.
+  wp_apply (join_spec with "[$Hl]") as (w) "H1".
   iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
 Qed.
 
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 8b2613cbd..3c2dd0c0e 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -629,6 +629,98 @@ 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 Notation "wp_apply" open_constr(lem) "as" constr(pat) :=
+  wp_apply lem; last iIntros pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
+
+
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" constr(pat) :=
+  wp_smart_apply lem; last iIntros pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
+
+
 (** 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
-- 
GitLab