From 4d8c4ac832f7a393853fbdda861a61ae0a0e5a39 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 00:51:48 +0200
Subject: [PATCH] More introduction patterns.

Also make those for introduction and elimination more symmetric:

  !%   pure introduction         %        pure elimination
  !#   always introduction       #        always elimination
  !>   later introduction        > pat    timeless later elimination
  !==> view shift introduction   ==> pat  view shift elimination
---
 ProofMode.md                          | 30 ++++++----
 heap_lang/heap.v                      | 10 ++--
 heap_lang/lib/barrier/proof.v         | 12 ++--
 heap_lang/lib/barrier/specification.v |  6 +-
 heap_lang/lib/lock.v                  |  2 +-
 program_logic/auth.v                  |  5 +-
 program_logic/boxes.v                 | 18 +++---
 program_logic/counter_examples.v      |  6 +-
 program_logic/hoare.v                 | 24 ++++----
 program_logic/invariants.v            |  6 +-
 program_logic/lifting.v               |  2 +-
 program_logic/pviewshifts.v           |  5 +-
 program_logic/sts.v                   |  2 +-
 program_logic/weakestpre.v            |  4 +-
 proofmode/intro_patterns.v            | 73 +++++++++++++++--------
 proofmode/spec_patterns.v             |  3 +-
 proofmode/tactics.v                   | 85 ++++++++++++++++-----------
 tests/barrier_client.v                |  4 +-
 tests/one_shot.v                      | 22 ++++---
 tests/proofmode.v                     |  4 +-
 20 files changed, 182 insertions(+), 141 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 49a5bb573..59846cef5 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -93,14 +93,14 @@ Rewriting
 Iris
 ----
 
-- `iPvsIntro` : introduction of a primitive view shift. Generates a goal if
-  the masks are not syntactically equal.
-- `iPvs pm_trm as (x1 ... xn) "ipat"` : runs a primitive view shift `pm_trm`.
+- `iVsIntro` : introduction of a raw or primitive view shift.
+- `iVs pm_trm as (x1 ... xn) "ipat"` : run a raw or primitive view shift
+  `pm_trm` (if the goal permits, i.e. it is a raw or primitive view shift, or
+   a weakest precondition).
 - `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
-- `iInv> N as (x1 ... xn) "ipat"` : open the invariant `N` and establish that
-  it is timeless so no laters have to be added.
-- `iTimeless "H"` : strip a later of a timeless hypotheses `H` in case the
-  conclusion is a primitive view shifts or weakest precondition.
+- `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
+   permits, i.e. it is a later, True now, raw or primitive view shift, or a
+   weakest precondition).
 
 Miscellaneous
 -------------
@@ -123,20 +123,24 @@ introduction patterns:
 - `?` : create an anonymous hypothesis.
 - `_` : remove the hypothesis.
 - `$` : frame the hypothesis in the goal.
-- `# ipat` : move the hypothesis to the persistent context.
-- `%` : move the hypothesis to the pure Coq context (anonymously).
 - `[ipat ipat]` : (separating) conjunction elimination.
 - `[ipat|ipat]` : disjunction elimination.
 - `[]` : false elimination.
+- `%` : move the hypothesis to the pure Coq context (anonymously).
+- `# ipat` : move the hypothesis to the persistent context.
+- `> ipat` : remove a later of a timeless hypothesis (if the goal permits).
+- `==> ipat` : run a view shift (if the goal permits).
 
 Apart from this, there are the following introduction patterns that can only
 appear at the top level:
 
-- `!` : introduce a box (provided that the spatial context is empty).
-- `>` : introduce a later (which strips laters from all hypotheses).
 - `{H1 ... Hn}` : clear `H1 ... Hn`.
 - `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
   previous pattern, e.g., `{$H1 H2 $H3}`).
+- `!%` : introduce a pure goal (and leave the proof mode).
+- `!#` : introduce an always modality (given that the spatial context is empty).
+- `!>` : introduce a later (which strips laters from all hypotheses).
+- `!==>` : introduce a view shift.
 - `/=` : perform `simpl`.
 - `*` : introduce all universal quantifiers.
 - `**` : introduce all universal quantifiers, as well as all arrows and wands.
@@ -147,7 +151,7 @@ For example, given:
 
 You can write
 
-        iIntros (x) "% ! $ [[] | #[HQ HR]] /= >".
+        iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
 
 which results in:
 
@@ -173,7 +177,7 @@ so called specification patterns to express this splitting:
 - `[H1 ... Hn]` : generate a goal with the spatial hypotheses `H1 ... Hn` and
   all persistent hypotheses. The hypotheses `H1 ... Hn` will be consumed.
 - `[-H1 ... Hn]`  : negated form of the above pattern
-- `=>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
+- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a primitive view shift, in which case the view shift will be kept in the
   goal of the premise too.
 - `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 095d82d5e..5c9593aad 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -164,7 +164,7 @@ Section heap.
     iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
     rewrite left_id /heap_inv. iDestruct "Hv" as %?.
     iApply wp_alloc_pst. iFrame "Hh". iNext.
-    iIntros (l) "[% Hh]"; iVsIntro.
+    iIntros (l) "[% Hh] !==>".
     iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").
     { rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
       iFrame "Hh". iPureIntro.
@@ -183,7 +183,7 @@ Section heap.
     rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "> Hown". iVsIntro. iVs ("Hclose" with "* [Hown]").
+    iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]").
     { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
     by iApply "HΦ".
   Qed.
@@ -199,7 +199,7 @@ Section heap.
     rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "> Hl". iVsIntro.
+    iIntros "!> Hl !==>".
     iVs ("Hclose" $! {[l := (1%Qp, DecAgree v)]} with "[Hl]").
     { iSplit.
       - iPureIntro; by apply singleton_local_update, exclusive_local_update.
@@ -218,7 +218,7 @@ Section heap.
     rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "> Hown". iVsIntro. iVs ("Hclose" with "* [Hown]").
+    iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]").
     { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
     by iApply "HΦ".
   Qed.
@@ -234,7 +234,7 @@ Section heap.
     rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "> Hl". iVsIntro.
+    iIntros "!> Hl !==>".
     iVs ("Hclose" $! {[l := (1%Qp, DecAgree v2)]} with "[Hl]").
     { iSplit.
       - iPureIntro; by apply singleton_local_update, exclusive_local_update.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 4827e526b..5b43b5fdd 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -96,7 +96,7 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
 Proof.
   iIntros (HN) "[#? HΦ]".
   rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
-  iApply ("HΦ" with "|==>[-]").
+  iApply ("HΦ" with "==>[-]").
   iVs (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iVs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
@@ -105,7 +105,7 @@ Proof.
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { rewrite /barrier_ctx. by repeat iSplit. }
   iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ★ sts_ownS γ' low_states {[Send]})%I with "|==>[-]" as "[Hr Hs]".
+    ★ sts_ownS γ' low_states {[Send]})%I with "==>[-]" as "[Hr Hs]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     - set_solver.
     - iApply (sts_own_weaken with "Hγ'");
@@ -128,7 +128,7 @@ Proof.
   iSplit; [iPureIntro; by eauto using signal_step|].
   iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
   iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
-  iIntros "> _"; by iApply "Hr".
+  iIntros "!> _"; by iApply "Hr".
 Qed.
 
 Lemma wait_spec l P (Φ : val → iProp Σ) :
@@ -142,7 +142,7 @@ Proof.
   wp_load. destruct p.
   - iVs ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
     { iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
-    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "|==>[Hγ]" as "Hγ".
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     iVsIntro. wp_op=> ?; simplify_eq; wp_if.
     iApply ("IH" with "Hγ [HQR] HΦ"). auto.
@@ -177,7 +177,7 @@ Proof.
     iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
-    ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "|==>[-]" as "[Hγ1 Hγ2]".
+    ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "==>[-]" as "[Hγ1 Hγ2]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     - abstract set_solver.
     - iApply (sts_own_weaken with "Hγ");
@@ -193,7 +193,7 @@ Proof.
   rewrite /recv.
   iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
   iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
-  iIntros "> HQ". by iApply "HP"; iApply "HP1".
+  iIntros "!> HQ". by iApply "HP"; iApply "HP1".
 Qed.
 
 Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index b9ea55b9e..93f70b407 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -20,9 +20,9 @@ Proof.
   intros HN.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "#? ! _". iApply (newbarrier_spec _ P); eauto.
-  - iIntros (l P) "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
-  - iIntros (l P) "! Hl". iApply wait_spec; iFrame "Hl"; eauto.
+  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto.
+  - iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
+  - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
   - intros; by apply recv_split.
   - apply recv_weaken.
 Qed.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 37d589a81..080bb3d6c 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -52,7 +52,7 @@ Proof.
   wp_seq. wp_alloc l as "Hl".
   iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
-  { iIntros ">". iExists false. by iFrame. }
+  { iIntros "!>". iExists false. by iFrame. }
   iVsIntro. iApply "HΦ". iExists γ; eauto.
 Qed.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 1c68c07ff..cd77b3052 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -97,9 +97,8 @@ Section auth.
       ■ ✓ (a ⋅ af) ★ ▷ φ (a ⋅ af) ★ ∀ b,
       ■ (a ~l~> b @ Some af) ★ ▷ φ (b ⋅ af) ={E∖N,E}=★ auth_own γ b.
   Proof.
-    iIntros (?) "(#? & Hγf)". rewrite /auth_ctx /auth_own.
-    iInv N as (a') "[Hγ Hφ]" "Hclose".
-    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
+    iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own.
+    iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ".
     iDestruct (own_valid with "#Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
     simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
     iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index d926a5272..59308593d 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -76,7 +76,7 @@ Lemma box_own_agree γ Q1 Q2 :
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
   rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
-  iIntros "#HQ >". rewrite -{2}(iProp_fold_unfold Q1).
+  iIntros "#HQ !>". rewrite -{2}(iProp_fold_unfold Q1).
   iRewrite "HQ". by rewrite iProp_fold_unfold.
 Qed.
 
@@ -131,10 +131,10 @@ Lemma box_fill f γ P Q :
   slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=> ▷ box N (<[γ:=true]> f) P.
 Proof.
   iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iInv N as (b') "(Hγ & #HγQ & _)" "Hclose". iTimeless "Hγ".
+  iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose".
   iDestruct (big_sepM_later _ f with "Hf") as "Hf".
   iDestruct (big_sepM_delete _ f _ false with "Hf")
-    as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
+    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iVs (box_own_auth_update γ b' false true with "[Hγ Hγ']")
     as "[Hγ Hγ']"; first by iFrame.
   iVs ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
@@ -149,12 +149,12 @@ Lemma box_empty f P Q γ :
   slice N γ Q ★ ▷ box N f P ={N}=> ▷ Q ★ ▷ box N (<[γ:=false]> f) P.
 Proof.
   iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iInv N as (b) "(Hγ & #HγQ & HQ)" "Hclose"; iTimeless "Hγ".
+  iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose".
   iDestruct (big_sepM_later _ f with "Hf") as "Hf".
   iDestruct (big_sepM_delete _ f with "Hf")
-    as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
+    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iDestruct (box_own_auth_agree γ b true with "[#]")
-    as "%"; subst; first by iFrame.
+    as %?; subst; first by iFrame.
   iFrame "HQ".
   iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
   iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
@@ -173,7 +173,7 @@ Proof.
   rewrite big_sepM_fmap; iApply (pvs_big_sepM _ _ f).
   iApply (big_sepM_impl _ _ f); iFrame "Hf".
   iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
-  iInv N as (b) "[Hγ _]" "Hclose"; iTimeless "Hγ".
+  iInv N as (b) "[>Hγ _]" "Hclose".
   iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
   iApply "Hclose". iNext; iExists true. by iFrame.
 Qed.
@@ -184,11 +184,11 @@ Lemma box_empty_all f P Q :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
-    box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "|==>[Hf]" as "[HΦ ?]".
+    box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "==>[Hf]" as "[HΦ ?]".
   { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
     iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
     assert (true = b) as <- by eauto.
-    iInv N as (b) "(Hγ & _ & HΦ)" "Hclose"; iTimeless "Hγ".
+    iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
     iDestruct (box_own_auth_agree γ b true with "[#]")
       as "%"; subst; first by iFrame.
     iVs (box_own_auth_update γ true true false with "[Hγ Hγ']")
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 4c6dc9c69..4a75e2718 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -21,7 +21,7 @@ Section savedprop.
   Proof.
     iIntros "#[H1 H2]".
     iAssert P as "#HP".
-    { iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
+    { iApply "H2". iIntros "!# #HP". by iApply ("H1" with "[#]"). }
     by iApply ("H1" with "[#]").
   Qed.
 
@@ -29,7 +29,7 @@ Section savedprop.
   Definition A (i : sprop) : iProp := ∃ P, saved i P ★ □ P.
   Lemma saved_is_A i P `{!PersistentP P} : saved i P ⊢ □ (A i ↔ P).
   Proof.
-    iIntros "#HS !". iSplit.
+    iIntros "#HS !#". iSplit.
     - iDestruct 1 as (Q) "[#HSQ HQ]".
       iApply (sprop_agree i P Q with "[]"); eauto.
     - iIntros "#HP". iExists P. by iSplit.
@@ -39,7 +39,7 @@ Section savedprop.
      implies that assertion with name [i] is equivalent to its own negation. *)
   Definition Q i := saved i (¬ A i).
   Lemma Q_self_contradiction i : Q i ⊢ □ (A i ↔ ¬ A i).
-  Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed.
+  Proof. iIntros "#HQ !#". by iApply (saved_is_A i (¬A i)). Qed.
 
   (* We can obtain such a [Q i]. *)
   Lemma make_Q : True =r=> ∃ i, Q i.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 39629cdba..49f9085b3 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -53,16 +53,16 @@ Global Instance ht_mono' E :
 Proof. solve_proper. Qed.
 
 Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
-Proof. iIntros (Hwp) "! HP". by iApply Hwp. Qed.
+Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
 
 Lemma ht_val E v : {{ True }} of_val v @ E {{ v', v = v' }}.
-Proof. iIntros "! _". by iApply wp_value'. Qed.
+Proof. iIntros "!# _". by iApply wp_value'. Qed.
 
 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". iVs ("Hvs" with "HP") as "HP".
+  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iVs ("Hvs" with "HP") as "HP".
   iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
@@ -72,7 +72,7 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   □ (P ={E1,E2}=★ P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ □ (∀ v, Φ' v ={E2,E1}=★ Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
+  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
   iVs ("Hvs" with "HP") as "HP". iVsIntro.
   iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
@@ -82,7 +82,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
   {{ P }} e @ E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
   ⊢ {{ P }} K e @ E {{ Φ' }}.
 Proof.
-  iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
+  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
   iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
@@ -90,24 +90,24 @@ Qed.
 Lemma ht_mask_weaken E1 E2 P Φ e :
   E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊢ {{ P }} e @ E2 {{ Φ }}.
 Proof.
-  iIntros (?) "#Hwp ! HP". iApply (wp_mask_mono E1 E2); try done.
+  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono E1 E2); try done.
   by iApply "Hwp".
 Qed.
 
 Lemma ht_frame_l E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ v, R ★ Φ v }}.
-Proof. iIntros "#Hwp ! [$ HP]". by iApply "Hwp". Qed.
+Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_r E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ v, Φ v ★ R }}.
-Proof. iIntros "#Hwp ! [HP $]". by iApply "Hwp". Qed.
+Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
   □ (R1 ={E1,E2}=★ ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
   ⊢ {{ R1 ★ P }} e @ E1 {{ λ v, R2 ★ Φ v }}.
 Proof.
-  iIntros (??) "[#Hvs #Hwp] ! [HR HP]".
+  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
   iApply (wp_frame_step_l E1 E2); try done.
   iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
 Qed.
@@ -117,7 +117,7 @@ Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ :
   □ (R1 ={E1,E2}=★ ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
   ⊢ {{ P ★ R1 }} e @ E1 {{ λ v, Φ v ★ R2 }}.
 Proof.
-  iIntros (??) "[#Hvs #Hwp] ! [HP HR]".
+  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
   iApply (wp_frame_step_r E1 E2); try done.
   iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
 Qed.
@@ -126,7 +126,7 @@ Lemma ht_frame_step_l' E P R e Φ :
   to_val e = None →
   {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ v, R ★ Φ v }}.
 Proof.
-  iIntros (?) "#Hwp ! [HR HP]".
+  iIntros (?) "#Hwp !# [HR HP]".
   iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
@@ -134,7 +134,7 @@ Lemma ht_frame_step_r' E P Φ R e :
   to_val e = None →
   {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ v, Φ v ★ R }}.
 Proof.
-  iIntros (?) "#Hwp ! [HP HR]".
+  iIntros (?) "#Hwp !# [HP HR]".
   iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 End hoare.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index a4e49288c..f87869daf 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -51,13 +51,13 @@ Proof.
   rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
   iIntros "(Hw & [HE $] & $)"; iVsIntro; iRight.
   iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
-  iIntros "HP [Hw $]"; iVsIntro; iRight. iApply ownI_close; by iFrame.
+  iIntros "HP [Hw $] !==>"; iRight. iApply ownI_close; by iFrame.
 Qed.
 
 Lemma inv_open_timeless E N P `{!TimelessP P} :
   nclose N ⊆ E → inv N P ={E,E∖N}=> P ★ (P ={E∖N,E}=★ True).
 Proof.
-  iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[HP Hclose]"; auto.
-  iTimeless "HP"; iVsIntro; iIntros "{$HP} HP". iApply "Hclose"; auto.
+  iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[>HP Hclose]"; auto.
+  iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
 Qed.
 End inv.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 19e113e81..6fd4ecc6b 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -18,7 +18,7 @@ Lemma wp_lift_step E Φ e1 :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & Hσf & H)". iTimeless "Hσf".
+  iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
   iDestruct (ownP_agree σ1 σ1' with "[#]") as %<-; first by iFrame.
   iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 ef Hstep).
   iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 9c14f02f7..e437c640d 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -43,9 +43,8 @@ Proof. apply ne_proper, _. Qed.
 Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=> P.
 Proof.
   intros (E1''&->&?)%subseteq_disjoint_union_L.
-  rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE)".
-  iVsIntro. iApply now_True_intro. iApply "H".
-  iIntros "[$ $]". iVsIntro; iRight; eauto.
+  rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>".
+  iApply now_True_intro. iApply "H". iIntros "[$ $] !==>". iRight; eauto.
 Qed.
 Lemma now_True_pvs E1 E2 P : â—‡ (|={E1,E2}=> P) ={E1,E2}=> P.
 Proof.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 4f599a8b1..671ee6aa9 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -97,7 +97,7 @@ Section sts.
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'.
   Proof.
     iIntros (?) "[#? Hγf]". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
-    iInv N as (s) "[Hγ Hφ]" "Hclose". iTimeless "Hγ".
+    iInv N as (s) "[>Hγ Hφ]" "Hclose".
     iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
     assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9021ea451..69f4a30d6 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -124,7 +124,7 @@ Proof.
   iVsIntro. iNext. iIntros (e2 σ2 ef Hstep).
   destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
   iVs ("H" $! _ σ2 ef with "[#]") as "($ & H & $)"; auto.
-  iVs (wp_value_inv with "H") as "H". iVs "H". by iApply wp_value'.
+  iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
 Qed.
 
 Lemma wp_strong_mono E1 E2 e Φ Ψ :
@@ -133,7 +133,7 @@ Proof.
   iIntros (?) "[HΦ H]". iLöb (e) as "IH". rewrite !wp_unfold /wp_pre.
   iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
   { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
-    iApply (pvs_mask_mono E1 _); first done. by iApply ("HΦ" with "|==>[-]"). }
+    iApply (pvs_mask_mono E1 _); first done. by iApply ("HΦ" with "==>[-]"). }
   iSplit; [done|]; iIntros (σ1) "Hσ".
   iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
   iVs ("H" $! σ1 with "Hσ") as "[$ H]".
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index 0f55cbf3b..ac49db839 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -3,14 +3,18 @@ From iris.prelude Require Export strings.
 Inductive intro_pat :=
   | IName : string → intro_pat
   | IAnom : intro_pat
-  | IAnomPure : intro_pat
   | IDrop : intro_pat
   | IFrame : intro_pat
-  | IPersistent : intro_pat → intro_pat
   | IList : list (list intro_pat) → intro_pat
+  | IPureElim : intro_pat
+  | IAlwaysElim : intro_pat → intro_pat
+  | ILaterElim : intro_pat → intro_pat
+  | IVsElim : intro_pat → intro_pat
+  | IPureIntro : intro_pat
+  | IAlwaysIntro : intro_pat
+  | ILaterIntro : intro_pat
+  | IVsIntro : intro_pat
   | ISimpl : intro_pat
-  | IAlways : intro_pat
-  | INext : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
   | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
@@ -19,23 +23,27 @@ Module intro_pat.
 Inductive token :=
   | TName : string → token
   | TAnom : token
-  | TAnomPure : token
   | TDrop : token
   | TFrame : token
-  | TPersistent : token
   | TBar : token
   | TBracketL : token
   | TBracketR : token
   | TAmp : token
   | TParenL : token
   | TParenR : token
+  | TPureElim : token
+  | TAlwaysElim : token
+  | TLaterElim : token
+  | TVsElim : token
+  | TPureIntro : token
+  | TAlwaysIntro : token
+  | TLaterIntro : token
+  | TVsIntro : token
   | TSimpl : token
-  | TAlways : token
-  | TNext : token
-  | TClearL : token
-  | TClearR : token
   | TForall : token
-  | TAll : token.
+  | TAll : token
+  | TClearL : token
+  | TClearR : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -44,18 +52,24 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | "" => rev (cons_name kn k)
   | String " " s => tokenize_go s (cons_name kn k) ""
   | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
-  | String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) ""
   | String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
-  | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
   | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
   | String "|" s => tokenize_go s (TBar :: cons_name kn k) ""
   | String "(" s => tokenize_go s (TParenL :: cons_name kn k) ""
   | String ")" s => tokenize_go s (TParenR :: cons_name kn k) ""
   | String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
-  | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
-  | String ">" s => tokenize_go s (TNext :: cons_name kn k) ""
+  | String "%" s => tokenize_go s (TPureElim :: cons_name kn k) ""
+  | String "#" s => tokenize_go s (TAlwaysElim :: cons_name kn k) ""
+  | String ">" s => tokenize_go s (TLaterElim :: cons_name kn k) ""
+  | String "=" (String "=" (String ">" s)) =>
+     tokenize_go s (TVsElim :: cons_name kn k) ""
+  | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
+  | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
+  | String "!" (String ">" s) => tokenize_go s (TLaterIntro :: cons_name kn k) ""
+  | String "!" (String "=" (String "=" (String ">" s))) =>
+     tokenize_go s (TVsIntro :: cons_name kn k) ""
   | String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
   | String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
@@ -67,11 +81,13 @@ Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
 Inductive stack_item :=
   | SPat : intro_pat → stack_item
-  | SPersistent : stack_item
   | SList : stack_item
   | SConjList : stack_item
   | SBar : stack_item
-  | SAmp : stack_item.
+  | SAmp : stack_item
+  | SAlwaysElim : stack_item
+  | SLaterElim : stack_item
+  | SVsElim : stack_item.
 Notation stack := (list stack_item).
 
 Fixpoint close_list (k : stack)
@@ -79,8 +95,11 @@ Fixpoint close_list (k : stack)
   match k with
   | SList :: k => Some (SPat (IList (ps :: pss)) :: k)
   | SPat pat :: k => close_list k (pat :: ps) pss
-  | SPersistent :: k =>
-     '(p,ps) ← maybe2 (::) ps; close_list k (IPersistent p :: ps) pss
+  | SAlwaysElim :: k =>
+     '(p,ps) ← maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
+  | SLaterElim :: k =>
+     '(p,ps) ← maybe2 (::) ps; close_list k (ILaterElim p :: ps) pss
+  | SVsElim :: k => '(p,ps) ← maybe2 (::) ps; close_list k (IVsElim p :: ps) pss
   | SBar :: k => close_list k [] (ps :: pss)
   | _ => None
   end.
@@ -102,7 +121,9 @@ Fixpoint close_conj_list (k : stack)
           end;
      Some (SPat (big_conj ps) :: k)
   | SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
-  | SPersistent :: k => p ← cur; close_conj_list k (Some (IPersistent p)) ps
+  | SAlwaysElim :: k => p ← cur; close_conj_list k (Some (IAlwaysElim p)) ps
+  | SLaterElim :: k => p ← cur; close_conj_list k (Some (ILaterElim p)) ps
+  | SVsElim :: k => p ← cur; close_conj_list k (Some (IVsElim p)) ps
   | SAmp :: k => p ← cur; close_conj_list k None (p :: ps)
   | _ => None
   end.
@@ -112,19 +133,23 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | [] => Some k
   | TName s :: ts => parse_go ts (SPat (IName s) :: k)
   | TAnom :: ts => parse_go ts (SPat IAnom :: k)
-  | TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k)
   | TDrop :: ts => parse_go ts (SPat IDrop :: k)
   | TFrame :: ts => parse_go ts (SPat IFrame :: k)
-  | TPersistent :: ts => parse_go ts (SPersistent :: k)
   | TBracketL :: ts => parse_go ts (SList :: k)
   | TBar :: ts => parse_go ts (SBar :: k)
   | TBracketR :: ts => close_list k [] [] ≫= parse_go ts
   | TParenL :: ts => parse_go ts (SConjList :: k)
   | TAmp :: ts => parse_go ts (SAmp :: k)
   | TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
+  | TPureElim :: ts => parse_go ts (SPat IPureElim :: k)
+  | TAlwaysElim :: ts => parse_go ts (SAlwaysElim :: k)
+  | TLaterElim :: ts => parse_go ts (SLaterElim :: k)
+  | TVsElim :: ts => parse_go ts (SVsElim :: k)
+  | TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
+  | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
+  | TLaterIntro :: ts => parse_go ts (SPat ILaterIntro :: k)
+  | TVsIntro :: ts => parse_go ts (SPat IVsIntro :: k)
   | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
-  | TAlways :: ts => parse_go ts (SPat IAlways :: k)
-  | TNext :: ts => parse_go ts (SPat INext :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
   | TClearL :: ts => parse_clear ts [] k
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 410749a13..03f6d40f9 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -32,8 +32,7 @@ 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 (TForall :: cons_name kn k) ""
-  | String "|" (String "=" (String "=" (String ">" s))) =>
-     tokenize_go s (TVs :: cons_name kn k) ""
+  | String "=" (String "=" (String ">" s)) => tokenize_go s (TVs :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 651456ee1..817c628a8 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -483,20 +483,57 @@ Local Tactic Notation "iExistDestruct" constr(H)
     [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
     |revert y; intros x].
 
+(** * Always *)
+Tactic Notation "iAlways":=
+  apply tac_always_intro;
+    [reflexivity || fail "iAlways: spatial context non-empty"|].
+
+(** * Later *)
+Tactic Notation "iNext":=
+  eapply tac_next;
+    [apply _
+    |let P := match goal with |- FromLater ?P _ => P end in
+     apply _ || fail "iNext:" P "does not contain laters"|].
+
+Tactic Notation "iTimeless" constr(H) :=
+  eapply tac_timeless with _ H _ _;
+    [let Q := match goal with |- IsNowTrue ?Q => Q end in
+     apply _ || fail "iTimeless: cannot remove later of timeless hypothesis in goal" Q
+    |env_cbv; reflexivity || fail "iTimeless:" H "not found"
+    |let P := match goal with |- TimelessP ?P => P end in
+     apply _ || fail "iTimeless:" P "not timeless"
+    |env_cbv; reflexivity|].
+
+(** * View shifts *)
+Tactic Notation "iVsIntro" :=
+  eapply tac_vs_intro;
+    [let P := match goal with |- FromVs ?P _ => P end in
+     apply _ || fail "iVsIntro:" P "not a viewshift"|].
+
+Tactic Notation "iVsCore" constr(H) :=
+  eapply tac_vs_elim with _ H _ _ _ _;
+    [env_cbv; reflexivity || fail "iVs:" H "not found"
+    |let P := match goal with |- ElimVs ?P _ _ _ => P end in
+     let Q := match goal with |- ElimVs _ _ _ ?Q => Q end in
+     apply _ || fail "iVs: cannot eliminate" H ":" P "in" Q
+    |env_cbv; reflexivity|].
+
 (** * Basic destruct tactic *)
 Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
   let rec go Hz pat :=
     lazymatch pat with
     | IAnom => idtac
-    | IAnomPure => iPure Hz as ?
     | IDrop => iClear Hz
     | IFrame => iFrame Hz
     | IName ?y => iRename Hz into y
-    | IPersistent ?pat => iPersistent Hz; go Hz pat
     | IList [[]] => iExFalso; iExact Hz
     | IList [[?pat1; ?pat2]] =>
        let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
     | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
+    | IPureElim => iPure Hz as ?
+    | IAlwaysElim ?pat => iPersistent Hz; go Hz pat
+    | ILaterElim ?pat => iTimeless Hz; go Hz pat
+    | IVsElim ?pat => iVsCore Hz; go Hz pat
     | _ => fail "iDestruct:" pat "invalid"
     end
   in let pat := intro_pat.parse_one pat in go H pat.
@@ -533,27 +570,6 @@ 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.
 
-(** * Always *)
-Tactic Notation "iAlways":=
-  apply tac_always_intro;
-    [reflexivity || fail "iAlways: spatial context non-empty"|].
-
-(** * Later *)
-Tactic Notation "iNext":=
-  eapply tac_next;
-    [apply _
-    |let P := match goal with |- FromLater ?P _ => P end in
-     apply _ || fail "iNext:" P "does not contain laters"|].
-
-Tactic Notation "iTimeless" constr(H) :=
-  eapply tac_timeless with _ H _ _;
-    [let Q := match goal with |- IsNowTrue ?Q => Q end in
-     apply _ || fail "iTimeless: cannot remove later of timeless hypothesis in goal" Q
-    |env_cbv; reflexivity || fail "iTimeless:" H "not found"
-    |let P := match goal with |- TimelessP ?P => P end in
-     apply _ || fail "iTimeless:" P "not timeless"
-    |env_cbv; reflexivity|].
-
 (** * Introduction tactic *)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
   [ (* (∀ _, _) *) apply tac_forall_intro; intros x
@@ -608,11 +624,18 @@ Tactic Notation "iIntros" constr(pat) :=
   let rec go pats :=
     lazymatch pats with
     | [] => idtac
+    | IPureElim :: ?pats => iIntro (?); go pats
+    | IAlwaysElim IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
+    | IAnom :: ?pats => let H := iFresh in iIntro H; go pats
+    | IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
+    | IName ?H :: ?pats => iIntro H; go pats
+    | IPureIntro :: ?pats => iPureIntro; go pats
+    | IAlwaysIntro :: ?pats => iAlways; go pats
+    | ILaterIntro :: ?pats => iNext; go pats
+    | IVsIntro :: ?pats => iVsIntro; go pats
+    | ISimpl :: ?pats => simpl; go pats
     | IForall :: ?pats => repeat iIntroForall; go pats
     | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
-    | ISimpl :: ?pats => simpl; go pats
-    | IAlways :: ?pats => iAlways; go pats
-    | INext :: ?pats => iNext; go pats
     | IClear ?cpats :: ?pats =>
        let rec clr cpats :=
          match cpats with
@@ -620,19 +643,13 @@ Tactic Notation "iIntros" constr(pat) :=
          | (false,?H) :: ?cpats => iClear H; clr cpats
          | (true,?H) :: ?cpats => iFrame H; clr cpats
          end in clr cpats
-    | IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
-    | IName ?H :: ?pats => iIntro H; go pats
-    | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
-    | IAnom :: ?pats => let H := iFresh in iIntro H; go pats
-    | IAnomPure :: ?pats => iIntro (?); go pats
-    | IPersistent ?pat :: ?pats =>
+    | IAlwaysElim ?pat :: ?pats =>
        let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
     | ?pat :: ?pats =>
        let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
-    | _ => fail "iIntro: failed with" pats
     end
   in let pats := intro_pat.parse pat in try iProof; go pats.
-Tactic Notation "iIntros" := iIntros "**".
+Tactic Notation "iIntros" := iIntros [IAll].
 
 Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
   try iProof; iIntro ( x1 ).
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index e422df09b..111c5aea5 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -46,12 +46,12 @@ Section client.
       wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
-      iSplitL; [|by iIntros (_ _) "_ >"].
+      iSplitL; [|by iIntros (_ _) "_ !>"].
       iDestruct (recv_weaken with "[] Hr") as "Hr".
       { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
       iVs (recv_split with "Hr") as "[H1 H2]"; first done.
       iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
-      iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]];
+      iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]];
         iApply worker_safe; by iSplit.
 Qed.
 End client.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 9dbb7194f..e644474e6 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -46,17 +46,16 @@ Proof.
   iVs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
   iVsIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!". wp_let.
-    iInv N as "H" "Hclose"; iTimeless "H".
-    iDestruct "H" as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+  - iIntros (n) "!#". wp_let.
+    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
     + wp_cas_suc. iVs (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
       iVs ("Hclose" with "[-]"); last eauto.
       iNext; iRight; iExists n; by iFrame.
     + wp_cas_fail. iVs ("Hclose" with "[-]"); last eauto.
       rewrite /one_shot_inv; eauto 10.
-  - iIntros "!". wp_seq. wp_focus (! _)%E.
-    iInv N as "Hγ" "Hclose"; iTimeless "Hγ".
+  - iIntros "!#". wp_seq. wp_focus (! _)%E.
+    iInv N as ">Hγ" "Hclose".
     iAssert (∃ v, l ↦ v ★ ((v = NONEV ★ own γ Pending) ∨
        ∃ n : Z, v = SOMEV #n ★ own γ (Shot n)))%I with "[Hγ]" as "Hv".
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
@@ -69,12 +68,11 @@ Proof.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iVs ("Hclose" with "[Hinv]") as "_"; eauto; iVsIntro.
-    wp_let. iVsIntro. iIntros "!". wp_seq.
+    wp_let. iVsIntro. iIntros "!#". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_focus (! _)%E.
-    iInv N as "H" "Hclose"; iTimeless "H".
-    iDestruct "H" as "[[Hl Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
+    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m') "[Hl Hγ]".
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
@@ -91,10 +89,10 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
       {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
     }}.
 Proof.
-  iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
+  iIntros "#? !# _". iApply wp_one_shot. iSplit; first done.
   iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
-  - iIntros (n) "! _". wp_proj. iApply "Hf1".
-  - iIntros "! _". wp_proj.
-    iApply wp_wand_l; iFrame "Hf2". by iIntros (v) "#? ! _".
+  - iIntros (n) "!# _". wp_proj. iApply "Hf1".
+  - iIntros "!# _". wp_proj.
+    iApply wp_wand_l; iFrame "Hf2". by iIntros (v) "#? !# _".
 Qed.
 End proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f8d271131..b9af873f5 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -20,7 +20,7 @@ Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat → uPred M) :
     ▷ (∀ 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)".
@@ -91,7 +91,7 @@ Section iris.
     (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q ={E}=★ R.
   Proof.
     iIntros (?) "H HP HQ".
-    iApply ("H" with "[#] HP |==>[HQ] |==>").
+    iApply ("H" with "[#] HP ==>[HQ] ==>").
     - done.
     - by iApply inv_alloc.
     - done.
-- 
GitLab