From 5b224d9c2ce17394502b54c303e4be30d64f0786 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Apr 2016 21:20:23 +0200
Subject: [PATCH] More uniform treatment of arguments of iApply, iPoseProof,
 iSpecialize and iDestruct.

These tactics now all take an iTrm, which is a tuple consisting of
a.) a lemma or name of a hypotheses b.) arguments to instantiate
c.) a specialization pattern.
---
 heap_lang/lib/barrier/proof.v |  32 ++--
 heap_lang/lib/lock.v          |   6 +-
 heap_lang/lib/par.v           |   2 +-
 heap_lang/lib/spawn.v         |  10 +-
 heap_lang/proofmode.v         |   6 -
 program_logic/hoare.v         |  15 +-
 program_logic/hoare_lifting.v |  15 +-
 program_logic/viewshifts.v    |   4 +-
 proofmode/coq_tactics.v       |  49 +++--
 proofmode/pviewshifts.v       |  67 ++-----
 proofmode/spec_patterns.v     |  18 +-
 proofmode/tactics.v           | 335 +++++++++++-----------------------
 tests/barrier_client.v        |   8 +-
 tests/heap_lang.v             |   6 +-
 tests/joining_existentials.v  |  18 +-
 tests/one_shot.v              |  10 +-
 tests/proofmode.v             |  20 +-
 17 files changed, 238 insertions(+), 383 deletions(-)

diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 5c6680d2e..858409d21 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -82,12 +82,12 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
   ⊢ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))).
 Proof.
   iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
-  iDestruct (big_sepS_delete _ _ i) "HΨ" as "[#HΨi HΨ]"; first done.
+  iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
   iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
-  - iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
-    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize "HPΨ" "HP". 
-    iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done.
-    iDestruct "HQR" "HΨ" as "[HR1 HR2]".
+  - iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
+    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
+    iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
+    iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
     rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2".
   - rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit.
 Qed.
@@ -102,8 +102,8 @@ Proof.
   rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
   iApply "HΦ".
   iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
-  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
-    "-" as {γ'} "[#? Hγ']"; eauto.
+  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "-")
+    as {γ'} "[#? Hγ']"; eauto.
   { iNext. rewrite /barrier_inv /=. iFrame "Hl".
     iExists (const P). rewrite !big_sepS_singleton /=.
     iSplit; [|done]. by iIntros "> ?". }
@@ -113,7 +113,7 @@ Proof.
     ★ sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     + set_solver.
-    + iApply sts_own_weaken "Hγ'";
+    + iApply (sts_own_weaken with "Hγ'");
         auto using sts.closed_op, i_states_closed, low_states_closed;
         set_solver. }
   iPvsIntro. rewrite /recv /send. iSplitL "Hr".
@@ -132,7 +132,7 @@ Proof.
   iSplit; [iPureIntro; by eauto using signal_step|].
   iSplitR "HΦ"; [iNext|by iIntros "?"].
   rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
-  iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
+  iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
   iIntros "> _"; by iApply "Hr".
 Qed.
 
@@ -149,20 +149,20 @@ Proof.
     { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
     iIntros "Hγ".
     iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
-    { iApply sts_own_weaken "Hγ"; eauto using i_states_closed. }
-    wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext.
+    { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
+    wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
   - (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
     iExists (State High (I ∖ {[ i ]})), (∅ : set token).
     iSplit; [iPureIntro; by eauto using wait_step|].
     iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
-    iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done.
+    iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
     iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
     { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
     iSplitL "HΨ' Hl Hsp"; [iNext|].
     + rewrite {2}/barrier_inv /=; iFrame "Hl".
       iExists Ψ; iFrame "Hsp". by iIntros "> _".
-    + iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
+    + iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
       iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
       iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
 Qed.
@@ -188,7 +188,8 @@ Proof.
       ★ sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
     { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
       + set_solver.
-      + iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed.
+      + iApply (sts_own_weaken with "Hγ");
+          eauto using sts.closed_op, i_states_closed.
         set_solver. }
     iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
     + iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
@@ -205,8 +206,7 @@ Proof.
   iIntros "> HQ". by iApply "HP"; iApply "HP1".
 Qed.
 
-Lemma recv_mono l P1 P2 :
-  P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
+Lemma recv_mono l P1 P2 : P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
 Proof.
   intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
 Qed.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 05a5dbdef..043afce2d 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -56,7 +56,7 @@ Proof.
   iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
   wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (lock_inv γ l R)) "-[HΦ]" as "#?"; first done.
+  iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done.
   { iNext. iExists false. by iFrame "Hl HR". }
   iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
 Qed.
@@ -72,7 +72,7 @@ Proof.
     + wp_if. by iApply "IH".
   - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
     + iNext. iExists true. by iSplit.
-    + wp_if. iPvsIntro. iApply "HΦ" "-[HR] HR". iExists N, γ. by repeat iSplit.
+    + wp_if. iApply ("HΦ" with "-[HR] HR"). iExists N, γ. by repeat iSplit.
 Qed.
 
 Lemma release_spec R l (Φ : val → iProp) :
@@ -83,6 +83,6 @@ Proof.
   iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b.
   - wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
   - wp_store. iDestruct "Hγ'" as "[Hγ' _]".
-    iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
+    iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%".
 Qed.
 End proof.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 12d3c18c0..8f1812620 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -32,7 +32,7 @@ Proof.
   iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
   wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
-  iSpecialize "HΦ" "-"; first by iSplitL "H1". by wp_let.
+  iSpecialize ("HΦ" with "* -"); first by iSplitL "H1". by wp_let.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 454c1489c..53fc6d6c7 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -59,11 +59,11 @@ Proof.
   iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
   wp_let; wp_alloc l as "Hl"; wp_let.
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (spawn_inv γ l Ψ)) "[Hl]" as "#?"; first done.
+  iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. }
   wp_apply wp_fork. iSplitR "Hf".
-  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. iSplit; first done.
-    iExists γ. iFrame "Hγ"; by iSplit.
+  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
+    iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
   - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
     iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]".
     wp_store. iSplit; [iNext|done].
@@ -78,13 +78,13 @@ Proof.
   iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
-    wp_case. wp_seq. iApply "IH" "Hγ Hv".
+    wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
   - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
     + iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame "Hl"; iRight.
         iExists _; iSplit; [done|by iRight]. }
       wp_case. wp_let. iPvsIntro. by iApply "Hv".
-    + iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
+    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
 Qed.
 End proof.
 
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index ffd83b20b..3092b1176 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -90,12 +90,6 @@ Tactic Notation "wp_apply" open_constr(lem) :=
     wp_bind K; iApply lem; try iNext)
   end.
 
-Tactic Notation "wp_apply" open_constr(lem) constr(Hs) :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind K; iApply lem Hs; try iNext)
-  end.
-
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 1e978fcd7..c2d7b69f7 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -62,9 +62,9 @@ Lemma ht_vs E P P' Φ Φ' e :
   ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
-  iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs "Hvs" "HP" as "HP".
+  iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs ("Hvs" with "HP") as "HP".
   iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
-  iIntros {v} "Hv". by iApply "HΦ" "!".
+  iIntros {v} "Hv". by iApply ("HΦ" with "!").
 Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
@@ -73,9 +73,9 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
   iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
-  iPvs "Hvs" "HP" as "HP"; first set_solver. iPvsIntro.
+  iPvs ("Hvs" with "HP") as "HP"; first set_solver. iPvsIntro.
   iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
-  iIntros {v} "Hv". by iApply "HΦ" "!".
+  iIntros {v} "Hv". by iApply ("HΦ" with "!").
 Qed.
 
 Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
@@ -84,7 +84,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
 Proof.
   iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
   iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
-  iIntros {v} "Hv". by iApply "HwpK" "!".
+  iIntros {v} "Hv". by iApply ("HwpK" with "!").
 Qed.
 
 Lemma ht_mask_weaken E1 E2 P Φ e :
@@ -110,9 +110,8 @@ Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
   iApply (wp_frame_step_l E E1 E2); try done.
   iSplitL "HR"; [|by iApply "Hwp"].
-  iPvs "Hvs1" "HR"; first by set_solver.
-  iPvsIntro. iNext.
-  by iPvs "Hvs2" "Hvs1"; first by set_solver.
+  iPvs ("Hvs1" with "HR"); first by set_solver.
+  iPvsIntro. iNext. by iApply "Hvs2".
 Qed.
 
 Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index bd4d17c8b..e64ef99d4 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -31,13 +31,13 @@ Lemma ht_lift_step E1 E2
 Proof.
   iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
   iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
-  iPvs "Hvs" "HP" as "[Hσ HP]"; first set_solver.
+  iPvs ("Hvs" with "HP") as "[Hσ HP]"; first set_solver.
   iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"].
-  iSpecialize "HΦ" {e2 σ2 ef} "! -". by iFrame "Hφ HP Hown".
+  iSpecialize ("HΦ" $! e2 σ2 ef with "! -"). by iFrame "Hφ HP Hown".
   iPvs "HΦ" as "[H1 H2]"; first by set_solver.
   iPvsIntro. iSplitL "H1".
-  - by iApply "He2" "!".
-  - destruct ef as [e|]; last done. by iApply "Hef" {_ _ (Some e)} "!".
+  - by iApply ("He2" with "!").
+  - destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e) with "!").
 Qed.
 
 Lemma ht_lift_atomic_step
@@ -74,8 +74,9 @@ Proof.
   iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
   iApply (wp_lift_pure_step E φ _ e1); auto.
   iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
-  - iApply "He2" "!"; by iSplit.
-  - destruct ef as [e|]; last done. iApply "Hef" {_ (Some e)} "!"; by iSplit.
+  - iApply ("He2" with "!"); by iSplit.
+  - destruct ef as [e|]; last done.
+    iApply ("Hef" $! _ (Some e) with "!"); by iSplit.
 Qed.
 
 Lemma ht_lift_pure_det_step
@@ -91,6 +92,6 @@ Proof.
   iSplit; iIntros {e2' ef'}.
   - iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2".
   - destruct ef' as [e'|]; last done.
-    iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef" "!".
+    iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply ("Hef" with "!").
 Qed.
 End lifting.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index ba657409b..b66bed545 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -65,7 +65,7 @@ Lemma vs_transitive E1 E2 E3 P Q R :
   E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
 Proof.
   iIntros {?} "#[HvsP HvsQ] ! HP".
-  iPvs "HvsP" "! HP" as "HQ"; first done. by iApply "HvsQ" "!".
+  iPvs ("HvsP" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!").
 Qed.
 
 Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
@@ -95,7 +95,7 @@ Lemma vs_inv N E P Q R :
   nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
 Proof.
   iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto.
-  iIntros "HR". iApply "Hvs" "!". by iSplitL "HR".
+  iIntros "HR". iApply ("Hvs" with "!"). by iSplitL "HR".
 Qed.
 
 Lemma vs_alloc N P : â–· P ={N}=> inv N P.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index a2547d594..ae98291a5 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export upred.
 From iris.algebra Require Import upred_big_op upred_tactics.
 From iris.proofmode Require Export environments.
-From iris.prelude Require Import stringmap.
+From iris.prelude Require Import stringmap hlist.
 Import uPred.
 
 Local Notation "Γ !! j" := (env_lookup j Γ).
@@ -287,16 +287,6 @@ Lemma tac_clear_spatial Δ Δ' Q :
   envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q.
 Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
 
-Lemma tac_duplicate Δ Δ' i p j P Q :
-  envs_lookup i Δ = Some (p, P) →
-  p = true →
-  envs_simple_replace i true (Esnoc (Esnoc Enil i P) j P) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
-Proof.
-  intros ? -> ??. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id idemp wand_elim_r.
-Qed.
-
 (** * False *)
 Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
@@ -560,7 +550,7 @@ Proof.
   by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
 Qed.
 
-(** Whenever posing [lem : True ⊢ Q] as [H} we want it to appear as [H : Q] and
+(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
 not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
 [True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
 make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
@@ -579,6 +569,18 @@ Proof.
   by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True.
 Qed.
 
+Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
+  envs_lookup_delete i Δ = Some (p, P, Δ') →
+  envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' →
+  Δ'' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
+  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
+    by rewrite right_id wand_elim_r.
+  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
+    by rewrite right_id wand_elim_r.
+Qed.
+
 Lemma tac_apply Δ Δ' i p R P1 P2 :
   envs_lookup_delete i Δ = Some (p, R, Δ')%I → ToWand R P1 P2 →
   Δ' ⊢ P1 → Δ ⊢ P2.
@@ -826,13 +828,26 @@ Qed.
 Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ (∀ a, Φ a).
 Proof. apply forall_intro. Qed.
 
-Lemma tac_forall_specialize {A} Δ Δ' i p (Φ : A → uPred M) Q a :
-  envs_lookup i Δ = Some (p, ∀ a, Φ a)%I →
-  envs_simple_replace i p (Esnoc Enil i (Φ a)) Δ = Some Δ' →
+Class ForallSpecialize {As} (xs : hlist As)
+    (P : uPred M) (Φ : himpl As (uPred M)) :=
+  forall_specialize : P ⊢ happly Φ xs.
+Arguments forall_specialize {_} _ _ _ {_}.
+
+Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
+Proof. done. Qed.
+Global Instance forall_specialize_cons A As x xs Φ (Ψ : A → himpl As (uPred M)) :
+  (∀ x, ForallSpecialize xs (Φ x) (Ψ x)) →
+  ForallSpecialize (hcons x xs) (∀ x : A, Φ x) Ψ.
+Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
+
+Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
+  envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
+  envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
-  destruct p; by rewrite /= right_id (forall_elim a) wand_elim_r.
+  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
+  - by rewrite right_id (forall_specialize _ P) wand_elim_r.
+  - by rewrite right_id (forall_specialize _ P) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index bc661a364..8a47eec7d 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -118,89 +118,44 @@ Tactic Notation "iPvsCore" constr(H) :=
   end.
 
 Tactic Notation "iPvs" open_constr(H) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as "?").
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
 Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
     constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
     constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
 Tactic Notation "iPvs" open_constr(H) "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) :=
-  iPoseProof H as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
-
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) :=
-  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as "?").
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" constr(pat) :=
-  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
-    constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
-    constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
-    simple_intropattern(x7) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "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) :=
-  iPoseProof lem Hs as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
 
 Tactic Notation "iTimeless" constr(H) :=
@@ -228,7 +183,7 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
   let H := iFresh in
   let Hs := spec_pat.parse_one Hs in
   lazymatch Hs with
-  | SSplit ?lr ?Hs =>
+  | SAssert ?lr ?Hs =>
      eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
        [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
         apply _ || fail "iPvsAssert: " P "not a pvs"
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index ad4e4a39f..6b85e90ad 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -1,11 +1,12 @@
 From iris.prelude Require Export strings.
 
 Inductive spec_pat :=
-  | SSplit : bool → list string → spec_pat
+  | SAssert : bool → list string → spec_pat
   | SPersistent : spec_pat
   | SPure : spec_pat
   | SAlways : spec_pat
-  | SName : string → spec_pat.
+  | SName : string → spec_pat
+  | SForall : spec_pat.
 
 Module spec_pat.
 Inductive token :=
@@ -15,7 +16,8 @@ Inductive token :=
   | TBracketR : token
   | TPersistent : token
   | TPure : token
-  | TAlways : token.
+  | TAlways : token
+  | TForall : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -29,29 +31,31 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
   | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
+  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
-Fixpoint parse_go (ts : list token) (split : option (bool * list string))
+Fixpoint parse_go (ts : list token) (g : option (bool * list string))
     (k : list spec_pat) : option (list spec_pat) :=
-  match split with
+  match g with
   | None =>
      match ts with
      | [] => Some (rev k)
      | TName s :: ts => parse_go ts None (SName s :: k)
      | TMinus :: TBracketL :: ts => parse_go ts (Some (true,[])) k
-     | TMinus :: ts => parse_go ts None (SSplit true [] :: k)
+     | TMinus :: ts => parse_go ts None (SAssert true [] :: k)
      | TBracketL :: ts => parse_go ts (Some (false,[])) k
      | TAlways :: ts => parse_go ts None (SAlways :: k)
      | TPersistent :: ts => parse_go ts None (SPersistent :: k)
      | TPure :: ts => parse_go ts None (SPure :: k)
+     | TForall :: ts => parse_go ts None (SForall :: k)
      | _ => None
      end
   | Some (b, ss) =>
      match ts with
      | TName s :: ts => parse_go ts (Some (b,s :: ss)) k
-     | TBracketR :: ts => parse_go ts None (SSplit b (rev ss) :: k)
+     | TBracketR :: ts => parse_go ts None (SAssert b (rev ss) :: k)
      | _ => None
      end
   end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 2cbeaac53..eaceb0d23 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
 From iris.algebra Require Export upred.
 From iris.proofmode Require Export notation.
-From iris.prelude Require Import stringmap.
+From iris.prelude Require Import stringmap hlist.
 
 Declare Reduction env_cbv := cbv [
   env_lookup env_fold env_lookup_delete env_delete env_app
@@ -11,6 +11,7 @@ Declare Reduction env_cbv := cbv [
   bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
   assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
   string_eq_dec string_rec string_rect (* strings *)
+  himpl happly
   env_persistent env_spatial envs_persistent
   envs_lookup envs_lookup_delete envs_delete envs_app
     envs_simple_replace envs_replace envs_split envs_clear_spatial].
@@ -105,14 +106,6 @@ Local Tactic Notation "iPersistent" constr(H) :=
      apply _ || fail "iPersistent:" H ":" Q "not persistent"
     |env_cbv; reflexivity|].
 
-Tactic Notation "iDuplicate" constr(H1) "as" constr(H2) :=
-  eapply tac_duplicate with _ H1 _ H2 _; (* (i:=H1) (j:=H2) *)
-    [env_cbv; reflexivity || fail "iDuplicate:" H1 "not found"
-    |reflexivity || fail "iDuplicate:" H1 "not in persistent context"
-    |env_cbv; reflexivity || fail "iDuplicate:" H2 "not fresh"|].
-Tactic Notation "iDuplicate" "#" constr(H1) "as" constr(H2) :=
-  iPersistent H1; iDuplicate H1 as H2.
-
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
@@ -123,20 +116,36 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
 Tactic Notation "iPureIntro" := apply uPred.const_intro.
 
 (** * Specialize *)
-Local Tactic Notation "iForallSpecialize" constr(H) open_constr(x) :=
-  eapply tac_forall_specialize with _ H _ _ x; (* (i:=H) (a:=x) *)
-    [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
-    |env_cbv; reflexivity|].
+Record iTrm {X As} :=
+  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
+Arguments ITrm {_ _} _ _ _.
+
+Notation "( H $! x1 .. xn )" :=
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 0).
+Notation "( H $! x1 .. xn 'with' pat )" :=
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 0).
+Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
+
+Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
+  match xs with
+  | hnil => idtac
+  | _ =>
+    eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
+      [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
+      |apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
+      |env_cbv; reflexivity|]
+  end.
 
-Tactic Notation "iSpecialize" constr (H) constr(pat) :=
+Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
   let solve_to_wand H1 :=
     let P := match goal with |- ToWand ?P _ _ => P end in
     apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
   let rec go H1 pats :=
     lazymatch pats with
     | [] => idtac
+    | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
     | SAlways :: ?pats => iPersistent H1; go H1 pats
-    | SSplit true [] :: SAlways :: ?pats =>
+    | SAssert true [] :: SAlways :: ?pats =>
        eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
@@ -167,167 +176,70 @@ Tactic Notation "iSpecialize" constr (H) constr(pat) :=
           apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity| |go H1 pats]
     | SPure :: ?pats =>
-       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _; (* make custom tac_ lemma *)
+       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
+         (* make custom tac_ lemma *)
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |let Q := match goal with |- PersistentP ?Q => Q end in
           apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity|iPureIntro|go H1 pats]
-    | SSplit ?lr ?Hs :: ?pats =>
+    | SAssert ?lr ?Hs :: ?pats =>
        eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"|
          |go H1 pats]
-    end in
-  repeat (iForallSpecialize H _);
-  let pats := spec_pat.parse pat in go H pats.
-
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) "}" :=
-  iForallSpecialize H x1.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1)
-    open_constr(x2) "}" :=
-  iSpecialize H { x1 }; iForallSpecialize H x2.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" :=
-  iSpecialize H { x1 x2 }; iForallSpecialize H x3.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" :=
-  iSpecialize H { x1 x2 x3 }; iForallSpecialize H x4.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-     open_constr(x3) open_constr(x4) open_constr(x5) "}" :=
-  iSpecialize H { x1 x2 x3 x4 }; iForallSpecialize H x5.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; iForallSpecialize H x6.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; iForallSpecialize H x7.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; iForallSpecialize H x8.
-
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) "}" constr(Hs) :=
-  iSpecialize H { x1 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; iSpecialize H @ Hs.
+    end in let pats := spec_pat.parse pat in go H pats.
+
+Tactic Notation "iSpecialize" open_constr(t) :=
+  match t with
+  | ITrm ?H ?xs ?pat => iSpecializeArgs H xs; iSpecializePat H pat
+  end.
 
 (** * Pose proof *)
-Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
-  eapply tac_pose_proof with _ H _ _ _; (* (j:=H) *)
-    [first
-       [eapply lem
-       |apply uPred.equiv_iff; eapply lem]
-    |apply _
-    |env_cbv; reflexivity || fail "iPoseProof:" H "not fresh"|].
-
-Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" constr(H) :=
-  iPoseProof lem as H; last iSpecialize H Hs.
-
-Tactic Notation "iPoseProof" open_constr(lem) :=
-  let H := iFresh in iPoseProof lem as H.
-Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) :=
-  let H := iFresh in iPoseProof lem Hs as H.
-
-Tactic Notation "iPoseProof" open_constr(lem) "as" tactic(tac) :=
-  lazymatch type of lem with
-  | string => tac lem
-  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
+  lazymatch type of H1 with
+  | string =>
+     eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
+       [env_cbv; reflexivity || fail "iPoseProof:" H1 "not found"
+       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
+  | _ =>
+     eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
+       [first [eapply H1|apply uPred.equiv_iff; eapply H1]
+       |apply _
+       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
   end.
 
-Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" tactic(tac) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs; last tac H).
+Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
+  lazymatch t with
+  | ITrm ?H1 ?xs ?pat =>
+     iPoseProofCore H1 as H; last (iSpecializeArgs H xs; iSpecializePat H pat)
+  | _ => iPoseProofCore t as H
+  end.
+
+Tactic Notation "iPoseProof" open_constr(t) :=
+  let H := iFresh in iPoseProof t as H.
 
 (** * Apply *)
-Tactic Notation "iApply" open_constr (lem) :=
-  iPoseProof lem as (fun H => repeat (iForallSpecialize H _); first
-    [iExact H
-    |eapply tac_apply with _ H _ _ _;
-       [env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
-       |apply _ || fail 1 "iApply: cannot apply" lem|]]).
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" :=
-  iSpecialize H { x1 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1)
-    open_constr(x2) "}" :=
-  iSpecialize H { x1 x2 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" :=
-  iSpecialize H { x1 x2 x3 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" :=
-  iSpecialize H { x1 x2 x3 x4 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-     open_constr(x3) open_constr(x4) open_constr(x5) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H.
-
-(* this is wrong *)
-Tactic Notation "iApply" open_constr (lem) constr(Hs) :=
-  iPoseProof lem Hs as (fun H => first
-    [iExact H
-    |eapply tac_apply with _ H _ _ _;
-       [env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
-       |apply _ || fail 1 "iApply: cannot apply" lem|]]).
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" constr(Hs) :=
-  iSpecialize H { x1 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H Hs.
+Tactic Notation "iApplyCore" constr(H) := first
+  [iExact H
+  |eapply tac_apply with _ H _ _ _;
+     [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
+     |apply _ || fail 1 "iApply: cannot apply" H|]].
+
+Tactic Notation "iApply" open_constr(t) :=
+  let Htmp := iFresh in
+  lazymatch t with
+  | ITrm ?H ?xs ?pat =>
+     iPoseProofCore H as Htmp; last (
+       iSpecializeArgs Htmp xs;
+       try (iSpecializeArgs Htmp (hcons _ _));
+       iSpecializePat Htmp pat; last iApplyCore Htmp)
+  | _ =>
+     iPoseProofCore t as Htmp; last (
+       try (iSpecializeArgs Htmp (hcons _ _));
+       iApplyCore Htmp)
+  end; try apply _.
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=
@@ -548,94 +460,59 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x8) "}" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 x8 } pat.
 
+Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
+  lazymatch type of lem with
+  | string => tac lem
+  | iTrm =>
+     lazymatch lem with
+     | @iTrm string ?H _ hnil ?pat =>
+        iSpecializePat H pat; last tac H
+     | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+     end
+  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+  end.
+
 Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as pat).
+  iDestructHelp H as (fun H => iDestructHyp H as pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
 Tactic Notation "iDestruct" open_constr(H) "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) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
-
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs; last iDestructHyp H as pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
-    constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
-    constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
-    simple_intropattern(x7) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "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) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
 
 Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
   let Htmp := iFresh in iDestruct H as Htmp; iPure Htmp as pat.
-Tactic Notation "iDestruct" open_constr(H) constr(Hs)
-    "as" "%" simple_intropattern(pat) :=
-  let Htmp := iFresh in iDestruct H Hs as Htmp; iPure Htmp as pat.
 
 (** * Always *)
 Tactic Notation "iAlways":=
-   apply tac_always_intro;
-     [reflexivity || fail "iAlways: spatial context non-empty"|].
+  apply tac_always_intro;
+    [reflexivity || fail "iAlways: spatial context non-empty"|].
 
 (** * Later *)
 Tactic Notation "iNext":=
@@ -760,7 +637,7 @@ Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
 
 (* This is pretty ugly, but without Ltac support for manipulating lists of
 idents I do not know how to do this better. *)
-Local Ltac iLöbCore IH tac_before tac_after :=
+Local Ltac iLöbHelp IH tac_before tac_after :=
   match goal with
   | |- of_envs ?Δ ⊢ _ =>
      let Hs := constr:(reverse (env_dom_list (env_spatial Δ))) in
@@ -771,31 +648,31 @@ Local Ltac iLöbCore IH tac_before tac_after :=
     tac_after; iIntros Hs
   end.
 
-Tactic Notation "iLöb" "as" constr (IH) := iLöbCore IH idtac idtac.
+Tactic Notation "iLöb" "as" constr (IH) := iLöbHelp IH idtac idtac.
 Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
+  iLöbHelp IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
+  iLöbHelp IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
     constr (IH):=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 })
               ltac:(iIntros { x1 x2 x3 x4 x5 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
 
 (** * Assert *)
@@ -803,7 +680,7 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
   let H := iFresh in
   let Hs := spec_pat.parse_one Hs in
   lazymatch Hs with
-  | SSplit ?lr ?Hs =>
+  | SAssert ?lr ?Hs =>
      eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
        [env_cbv; reflexivity || fail "iAssert:" Hs "not found"
        |env_cbv; reflexivity|
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 45366e9e0..0338d3e07 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -48,9 +48,9 @@ Section client.
       iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros {_ _} "_ >"].
-      iDestruct recv_weaken "[] Hr" as "Hr".
-      { iIntros "Hy". by iApply y_inv_split "Hy". }
-      iPvs recv_split "Hr" as "[H1 H2]"; first done.
+      iDestruct (recv_weaken with "[] Hr") as "Hr".
+      { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
+      iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
       iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
       iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros {_ _} "_ >"]];
         iApply worker_safe; by iSplit.
@@ -64,7 +64,7 @@ Section ClosedProofs.
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
   Proof.
     iIntros "! Hσ".
-    iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
+    iPvs (heap_alloc (nroot .@ "Barrier") with "Hσ") as {h} "[#Hh _]"; first done.
     iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
   Qed.
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 864c5b7cf..22cabb3ec 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -27,7 +27,7 @@ Section LiftingTests.
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
-    wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
+    wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
   Qed.
 
   Definition FindPred : val :=
@@ -44,7 +44,7 @@ Section LiftingTests.
   Proof.
     iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
-    - iApply "IH" "% HΦ". omega.
+    - iApply ("IH" with "% HΦ"). omega.
     - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
@@ -69,7 +69,7 @@ Section ClosedProofs.
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}.
   Proof.
     iProof. iIntros "! Hσ".
-    iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
+    iPvs (heap_alloc nroot with "Hσ") as {h} "[? _]"; first by rewrite nclose_nroot.
     iApply heap_e_spec; last done; by rewrite nclose_nroot.
   Qed.
 End ClosedProofs.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index a96ddeaf7..377ebcf52 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -24,7 +24,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
 Proof.
   iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
-  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He" "!"].
+  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply ("He" with "!")].
   iIntros {v} "?"; iExists x; by iSplit.
 Qed.
 
@@ -35,14 +35,14 @@ Context {Ψ_join  : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}.
 Lemma P_res_split γ : barrier_res γ Φ ⊢ (barrier_res γ Φ1 ★ barrier_res γ Φ2).
 Proof.
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
-  iDestruct Φ_split "Hx" as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
+  iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
 Qed.
 
 Lemma Q_res_join γ : (barrier_res γ Ψ1 ★ barrier_res γ Ψ2) ⊢ ▷ barrier_res γ Ψ.
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
-  iDestruct (one_shot_agree γ x x') "- !" as "Hxx"; first (by iSplit).
+  iDestruct (one_shot_agree γ x x' with "- !") as "Hxx"; first (by iSplit).
   iNext. iRewrite -"Hxx" in "Hx'".
   iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
 Qed.
@@ -62,20 +62,20 @@ Proof.
   set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
   wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post); first done.
   iFrame "Hh". iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
-  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|iApply "He" "HP"].
+  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
     iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
-    iPvs (one_shot_init _ _ x) "Hγ" as "Hx".
+    iPvs (one_shot_init _ _ x with "Hγ") as "Hx".
     iApply signal_spec; iFrame "Hs"; iSplit; last done.
     iExists x; by iSplitL "Hx".
-  - iDestruct recv_weaken "[] Hr" as "Hr".
-    { iIntros "?". by iApply P_res_split "-". }
-    iPvs recv_split "Hr" as "[H1 H2]"; first done.
+  - iDestruct (recv_weaken with "[] Hr") as "Hr".
+    { iIntros "?". by iApply (P_res_split with "-"). }
+    iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
     wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
       (λ _, barrier_res γ Ψ2)%I); first done.
     iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
     + by iApply worker_spec; iSplitL "H1".
     + by iApply worker_spec; iSplitL "H2".
     + by iIntros {v1 v2} "? >".
-  - iIntros {_ v} "[_ H]"; iPoseProof Q_res_join "H". by iNext; iExists γ.
+  - iIntros {_ v} "[_ H]"; iPoseProof (Q_res_join with "H"). by iNext; iExists γ.
 Qed.
 End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 7fa38345b..a96ffa375 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -44,13 +44,13 @@ Proof.
   iIntros "[#? Hf] /=".
   rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc OneShotPending) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (one_shot_inv γ l)) "[Hl Hγ]" as "#HN"; first done.
+  iPvs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN"; first done.
   { iNext. iLeft. by iSplitL "Hl". }
   iPvsIntro. iApply "Hf"; iSplit.
   - iIntros {n} "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
     + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
-      iPvs own_update "Hγ" as "Hγ".
+      iPvs (own_update with "Hγ") as "Hγ".
       { (* FIXME: canonical structures are not working *)
         by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
@@ -72,10 +72,10 @@ Proof.
     { wp_case. wp_seq. by iPvsIntro. }
     wp_case. wp_let. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
-    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%". }
+    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct own_valid "Hγ !" as % [=->]%dec_agree_op_inv.
+    iDestruct (own_valid with "Hγ !") as % [=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; iExists m; by iSplit|].
     wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=.
     iSplit. done. by iNext.
@@ -90,7 +90,7 @@ Lemma hoare_one_shot (Φ : val → iProp) :
 Proof.
   iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
   iIntros {f1 f2} "[#Hf1 #Hf2]"; iSplit.
-  - iIntros {n} "! _". wp_proj. iApply "Hf1" "!".
+  - iIntros {n} "! _". wp_proj. iApply ("Hf1" with "!").
   - iIntros "! _". wp_proj.
     iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
 Qed.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 5fb1366a5..3435e9b6e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,27 +1,37 @@
 From iris.proofmode Require Import tactics.
 
+Lemma demo_0 {M : cmraT} (P Q : uPred M) :
+  □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
+Proof.
+  iIntros "#H #H2".
+  (* should remove the disjunction "H" *)
+  iDestruct "H" as "[?|?]"; last by iLeft.
+  (* should keep the disjunction "H" because it is instantiated *)
+  iDestruct ("H2" $! 10) as "[%|%]". done. done.
+Qed.
+
 Lemma demo_1 (M : cmraT) (P1 P2 P3 : nat → uPred M) :
   True ⊢ (∀ (x y : nat) a b,
     x ≡ y →
     □ (uPred_ownM (a ⋅ b) -★
     (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -★
-    ▷ (∀ z, P2 z) -★
+    □ ▷ (∀ z, P2 z ∨ True → P2 z) -★
     ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -★
     ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b))).
 Proof.
-  iIntros {i [|j] a b ?} "! [Ha Hb] H1 H2 H3"; setoid_subst.
+  iIntros {i [|j] a b ?} "! [Ha Hb] H1 #H2 H3"; setoid_subst.
   { iLeft. by iNext. }
   iRight.
   iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)".
-  iDuplicate "Hc" as "foo".
+  iPoseProof "Hc" as "foo".
   iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
   iAssert (uPred_ownM (a â‹… core a))%I as "[Ha #Hac]" with "[Ha]".
   { by rewrite cmra_core_r. }
   iFrame "Ha Hac".
   iExists (S j + z1), z2.
   iNext.
-  iApply "H3" { _ 0 } "H1 ! [H2] !".
-  - iSplit. done. iApply "H2".
+  iApply ("H3" $! _ 0 with "H1 ! [] !").
+  - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
   - done.
 Qed.
 
-- 
GitLab