From 65bfa071cfb0526b1bada6a3833df993a4c1b696 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 May 2016 13:41:43 +0200
Subject: [PATCH] Make specialization patterns for persistent premises more
 uniform.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Changes:
- We no longer have a different syntax for specializing a term H : P -★ Q whose
  range P or domain Q is persistent. There is just one syntax, and the system
  automatically determines whether either P or Q is persistent.
- While specializing a term, always modalities are automatically stripped. This
  gets rid of the specialization pattern !.
- Make the syntax of specialization patterns more consistent. The syntax for
  generating a goal is [goal_spec] where goal_spec is one of the following:

    H1 .. Hn : generate a goal using hypotheses H1 .. Hn
   -H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn
           # : generate a goal for the premise in which all hypotheses can be
               used. This is only allowed when specializing H : P -★ Q where
               either P or Q is persistent.
           % : generate a goal for a pure premise.
---
 heap_lang/lib/barrier/proof.v | 10 ++---
 heap_lang/lib/lock.v          |  4 +-
 heap_lang/lib/par.v           |  2 +-
 heap_lang/lifting.v           |  5 +--
 program_logic/auth.v          |  4 +-
 program_logic/hoare.v         |  6 +--
 program_logic/hoare_lifting.v | 12 +++---
 program_logic/sts.v           |  2 +-
 program_logic/viewshifts.v    |  5 +--
 proofmode/coq_tactics.v       | 69 ++++++++++++++++++---------------
 proofmode/pviewshifts.v       |  4 +-
 proofmode/spec_patterns.v     | 46 +++++++++++-----------
 proofmode/tactics.v           | 73 +++++++++++++++++------------------
 tests/heap_lang.v             |  2 +-
 tests/joining_existentials.v  |  7 ++--
 tests/one_shot.v              |  8 ++--
 tests/proofmode.v             |  6 +--
 17 files changed, 133 insertions(+), 132 deletions(-)

diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 95edcac58..33225fe11 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -84,7 +84,7 @@ Proof.
   iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
   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) with "#") as "Heq"; first by iSplit.
+  - 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]".
@@ -102,7 +102,7 @@ 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 {[ γ ]}) with "-")
+  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 /=.
@@ -110,7 +110,7 @@ Proof.
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { rewrite /barrier_ctx. by repeat iSplit. }
   iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ★ sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
+    ★ 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 with "Hγ'");
@@ -162,7 +162,7 @@ Proof.
     iSplitL "HΨ' Hl Hsp"; [iNext|].
     + rewrite {2}/barrier_inv /=; iFrame "Hl".
       iExists Ψ; iFrame "Hsp". by iIntros "> _".
-    + iPoseProof (saved_prop_agree i Q (Ψ i) with "#") 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.
@@ -185,7 +185,7 @@ Proof.
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
   - iIntros "Hγ".
     iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
-      ★ sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
+      ★ 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 with "Hγ");
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index df476fbf4..8b1b522ce 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -57,7 +57,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) with "-[HΦ]") as "#?"; first done.
+  iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
   { iIntros ">". iExists false. by iFrame "Hl HR". }
   iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
 Qed.
@@ -73,7 +73,7 @@ Proof.
     + wp_if. by iApply "IH".
   - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
     + iNext. iExists true. by iSplit.
-    + wp_if. iApply ("HΦ" with "-[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) :
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index e394bfc47..ae36dc62e 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Φ" with "* -"); 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/lifting.v b/heap_lang/lifting.v
index b81fac901..3f2f3dffa 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -34,9 +34,8 @@ Proof.
     ef = None ∧ e' = Lit (LitLoc l) ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
   iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
     [by intros; subst φ; inv_head_step; eauto 8|].
-  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
-  (* FIXME: I should not have to refer to "H0". *)
-  destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
+  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[Hφ HP]".
+  iDestruct "Hφ" as %(l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
   iSplit; last done. iApply "HΦ"; by iSplit.
 Qed.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 029e21f17..460f89b10 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -61,7 +61,7 @@ Section auth.
     iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
     iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
     iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
-    iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
+    iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
     { iNext. iExists a. by iFrame "Hφ". }
     iPvsIntro; iExists γ; by iFrame "Hγ'".
   Qed.
@@ -83,7 +83,7 @@ Section auth.
     iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
     iInv N as {a'} "[Hγ Hφ]".
     iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid _ with "Hγ !") as "Hvalid".
+    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
     iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
     iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
     rewrite ->(left_id _ _) in Ha'; setoid_subst.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index e5898f1f8..8745e5e49 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -64,7 +64,7 @@ Lemma ht_vs E P P' Φ Φ' e :
 Proof.
   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Φ" with "!").
+  iIntros {v} "Hv". by iApply "HΦ".
 Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
@@ -75,7 +75,7 @@ Proof.
   iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
   iPvs ("Hvs" with "HP") as "HP"; first set_solver. iPvsIntro.
   iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
-  iIntros {v} "Hv". by iApply ("HΦ" with "!").
+  iIntros {v} "Hv". by iApply "HΦ".
 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" with "!").
+  iIntros {v} "Hv". by iApply "HwpK".
 Qed.
 
 Lemma ht_mask_weaken E1 E2 P Φ e :
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index e64ef99d4..3e772244b 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -33,11 +33,11 @@ Proof.
   iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
   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 with "! -"). 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" with "!").
-  - destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e) with "!").
+  - by iApply "He2".
+  - destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e)).
 Qed.
 
 Lemma ht_lift_atomic_step
@@ -74,9 +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" with "!"); by iSplit.
+  - iApply "He2"; by iSplit.
   - destruct ef as [e|]; last done.
-    iApply ("Hef" $! _ (Some e) with "!"); by iSplit.
+    iApply ("Hef" $! _ (Some e)); by iSplit.
 Qed.
 
 Lemma ht_lift_pure_det_step
@@ -92,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" with "!").
+    iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef".
 Qed.
 End lifting.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 18fd96dac..58d6a00ba 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -101,7 +101,7 @@ Section sts.
   Proof.
     iIntros {??} "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
     iInv N as {s} "[Hγ Hφ]"; iTimeless "Hγ".
-    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ !") as %Hvalid.
+    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.
     iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 5e2dbdeda..aff248a17 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" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!").
+  iPvs ("HvsP" with "HP") as "HQ"; first done. by iApply "HvsQ".
 Qed.
 
 Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
@@ -94,8 +94,7 @@ Proof. intros; apply vs_mask_frame; set_solver. Qed.
 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". iInv N as "HR".
-  iApply ("Hvs" with "!"). by iSplitL "HR".
+  iIntros {?} "#[? Hvs] ! HP". iInv N as "HR". iApply "Hvs". 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 4bf945085..d3f295f67 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -294,9 +294,13 @@ Qed.
 
 (** * Basic rules *)
 Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : □?p P ⊢ Q.
+Arguments to_assumption _ _ _ {_}.
 Global Instance to_assumption_exact p P : ToAssumption p P P.
 Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
-Global Instance to_assumption_always P Q :
+Global Instance to_assumption_always_l p P Q :
+  ToAssumption p P Q → ToAssumption p (□ P) Q.
+Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
+Global Instance to_assumption_always_r P Q :
   ToAssumption true P Q → ToAssumption true P (□ Q).
 Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
 
@@ -465,6 +469,8 @@ Global Instance to_wand_iff_l P Q : ToWand (P ↔ Q) P Q.
 Proof. by apply and_elim_l', impl_wand. Qed.
 Global Instance to_wand_iff_r P Q : ToWand (P ↔ Q) Q P.
 Proof. apply and_elim_r', impl_wand. Qed.
+Global Instance to_wand_always R P Q : ToWand R P Q → ToWand (□ R) P Q.
++Proof. rewrite /ToWand=> ->. apply always_elim. Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
@@ -508,32 +514,34 @@ Proof.
     by rewrite always_if_elim assoc HP1 wand_elim_l wand_elim_r.
 Qed.
 
-Lemma tac_specialize_range_persistent Δ Δ' Δ'' j q P1 P2 R Q :
-  envs_lookup_delete j Δ = Some (q, R, Δ')%I →
-  ToWand R P1 P2 → PersistentP P1 →
-  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  Δ' ⊢ P1 → Δ'' ⊢ Q → Δ ⊢ Q.
+Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
+  envs_lookup j Δ = Some (q, R) →
+  ToWand R P1 P2 → ToPure P1 φ →
+  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
+  φ → Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
-  rewrite envs_lookup_sound //.
-  rewrite -(idemp uPred_and (envs_delete _ _ _)).
-  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
-  rewrite envs_simple_replace_sound' //; simpl.
-  rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
-  by rewrite wand_elim_r.
+  intros. rewrite envs_simple_replace_sound //; simpl.
+  by rewrite right_id (to_wand R) (to_pure P1) const_equiv // wand_True wand_elim_r.
 Qed.
 
-Lemma tac_specialize_domain_persistent Δ Δ' Δ'' j q P1 P2 P2' R Q :
-  envs_lookup_delete j Δ = Some (q, R, Δ')%I →
-  ToWand R P1 P2 → ToPersistentP P2 P2' →
-  envs_replace j q true (Esnoc Enil j P2') Δ = Some Δ'' →
-  Δ' ⊢ P1 → Δ'' ⊢ Q → Δ ⊢ Q.
+Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+  envs_lookup_delete j Δ = Some (q, R, Δ') →
+  ToWand R P1 P2 →
+  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
+  Δ' ⊢ P1 → (PersistentP P1 ∨ PersistentP P2) →
+  Δ'' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
-  rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
-  rewrite envs_replace_sound //; simpl.
-  rewrite (sep_elim_r _ (_ -★ _)) right_id (to_wand R) always_if_elim.
-  by rewrite wand_elim_l (to_persistentP P2) always_and_sep_l' wand_elim_r.
+  intros [? ->]%envs_lookup_delete_Some ?? HP1 [?|?] <-.
+  - rewrite envs_lookup_sound //.
+    rewrite -(idemp uPred_and (envs_delete _ _ _)).
+    rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+    rewrite envs_simple_replace_sound' //; simpl.
+    rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+    by rewrite wand_elim_r.
+  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
+    rewrite envs_simple_replace_sound //; simpl.
+    rewrite (sep_elim_r _ (_ -★ _)) right_id (to_wand R) always_if_elim.
+    by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
@@ -553,22 +561,19 @@ Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
-  envs_app (envs_persistent Δ1) (Esnoc Enil j P) Δ2 = Some Δ2' →
+  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
   Δ1 ⊢ P → Δ2' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ?? HP ?. rewrite envs_split_sound //.
-  destruct (envs_persistent Δ1) eqn:?.
-  - rewrite (persistentP Δ1) HP envs_app_sound //; simpl.
-    by rewrite right_id wand_elim_r.
-  - rewrite HP envs_app_sound //; simpl. by rewrite right_id wand_elim_r.
+  intros ?? HP HQ. rewrite envs_split_sound //.
+  rewrite (envs_app_sound Δ2) //; simpl.
+  by rewrite right_id HP HQ wand_elim_r.
 Qed.
 
 Lemma tac_assert_persistent Δ Δ' j P Q :
-  PersistentP P →
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  Δ ⊢ P → Δ' ⊢ Q → Δ ⊢ Q.
+  Δ ⊢ P → PersistentP P → Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ?? HP ?.
+  intros ? HP ??.
   rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
   by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
 Qed.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 82b553043..5f4823b0f 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -26,7 +26,7 @@ Global Instance frame_pvs E1 E2 R P mQ :
   Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> if mQ is Some Q then Q else True))%I.
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
 Global Instance to_wand_pvs E1 E2 R P Q :
-  ToWand R P Q → ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+  ToWand R P Q → ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
 Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
 Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
@@ -190,7 +190,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
-  | SAssert ?lr ?Hs =>
+  | SGoal ?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 6b85e90ad..e3c065a65 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -1,11 +1,10 @@
 From iris.prelude Require Export strings.
 
 Inductive spec_pat :=
-  | SAssert : bool → list string → spec_pat
-  | SPersistent : spec_pat
-  | SPure : spec_pat
-  | SAlways : spec_pat
-  | SName : string → spec_pat
+  | SGoal : bool → list string → spec_pat
+  | SGoalPersistent : spec_pat
+  | SGoalPure : spec_pat
+  | SName : bool → string → spec_pat (* first arg = persistent *)
   | SForall : spec_pat.
 
 Module spec_pat.
@@ -16,7 +15,6 @@ Inductive token :=
   | TBracketR : token
   | TPersistent : token
   | TPure : token
-  | TAlways : token
   | TForall : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
@@ -30,37 +28,39 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
   | 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) (g : option (bool * list string))
+Inductive state :=
+  | StTop : state
+  | StAssert : bool → list string → state.
+
+Fixpoint parse_go (ts : list token) (s : state)
     (k : list spec_pat) : option (list spec_pat) :=
-  match g with
-  | None =>
+  match s with
+  | StTop =>
      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 (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)
+     | TName s :: ts => parse_go ts StTop (SName false s :: k)
+     | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
+     | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
+     | TBracketL :: ts => parse_go ts (StAssert false []) k
+     | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
+     | TForall :: ts => parse_go ts StTop (SForall :: k)
      | _ => None
      end
-  | Some (b, ss) =>
+  | StAssert neg ss =>
      match ts with
-     | TName s :: ts => parse_go ts (Some (b,s :: ss)) k
-     | TBracketR :: ts => parse_go ts None (SAssert b (rev ss) :: k)
+     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert true ss) k
+     | TName s :: ts => parse_go ts (StAssert neg (s :: ss)) k
+     | TBracketR :: ts => parse_go ts StTop (SGoal neg (rev ss) :: k)
      | _ => None
      end
   end.
 Definition parse (s : string) : option (list spec_pat) :=
-  parse_go (tokenize s) None [].
+  parse_go (tokenize s) StTop [].
 
 Ltac parse s :=
   lazymatch type of s with
@@ -76,4 +76,4 @@ Ltac parse_one s :=
               | Some [?pat] => pat | _ => fail "invalid spec_pat" s
               end
   end.
-End spec_pat.
\ No newline at end of file
+End spec_pat.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 8fad7e786..1620fd289 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -129,7 +129,7 @@ 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) :=
+Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
   match xs with
   | hnil => idtac
   | _ =>
@@ -139,7 +139,7 @@ Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
       |env_cbv; reflexivity|]
   end.
 
-Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
+Local 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
@@ -147,25 +147,7 @@ Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
     lazymatch pats with
     | [] => idtac
     | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
-    | SAlways :: ?pats => iPersistent H1; go H1 pats
-    | SAssert true [] :: SAlways :: ?pats =>
-       eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
-         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
-         |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
-          apply _ || fail "iSpecialize:" Q "not persistent"
-         |env_cbv; reflexivity
-         | |go H1 pats]
-    | SName ?H2 :: SAlways :: ?pats =>
-       eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
-         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
-         |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
-          apply _ || fail "iSpecialize:" Q "not persistent"
-         |env_cbv; reflexivity
-         |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
-         |go H1 pats]
-    | SName ?H2 :: ?pats =>
+    | SName false ?H2 :: ?pats =>
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
@@ -173,26 +155,43 @@ Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
           let Q := match goal with |- ToWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
          |env_cbv; reflexivity|go H1 pats]
-    | SPersistent :: ?pats =>
-       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
+    | SName true ?H2 :: ?pats =>
+       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
          [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| |go H1 pats]
-    | SPure :: ?pats =>
-       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
-         (* make custom tac_ lemma *)
+         |env_cbv; reflexivity
+         |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
+         |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
+          let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
+          first [left; apply _ | right; apply _]
+            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
+         |go H1 pats]
+    | SGoalPersistent :: ?pats =>
+       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |env_cbv; reflexivity
+         |(*goal*)
+         |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
+          let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
+          first [left; apply _ | right; apply _]
+            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
+         |go H1 pats]
+    | SGoalPure :: ?pats =>
+       eapply tac_specialize_pure with _ H1 _ _ _ _ _;
          [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]
-    | SAssert ?lr ?Hs :: ?pats =>
+         |let Q := match goal with |- ToPure ?Q _ => Q end in
+          apply _ || fail "iSpecialize:" Q "not pure"
+         |env_cbv; reflexivity
+         |(*goal*)
+         |go H1 pats]
+    | SGoal ?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"|
+         |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
+         |(*goal*)
          |go H1 pats]
     end in let pats := spec_pat.parse pat in go H pats.
 
@@ -202,7 +201,7 @@ Tactic Notation "iSpecialize" open_constr(t) :=
   end.
 
 (** * Pose proof *)
-Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
+Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
   lazymatch type of H1 with
   | string =>
      eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
@@ -704,12 +703,12 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
-  | [SAssert ?lr ?Hs] =>
+  | [SGoal ?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|
        |iDestructHyp H as pat]
-  | [SAssert true [] :: SAlways]  =>
+  | [SGoalPersistent]  =>
      eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
        [apply _ || fail "iAssert:" Q "not persistent"
        |env_cbv; reflexivity|
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f83c8a8d7..fc0a71d63 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -45,7 +45,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" with "% HΦ"). omega.
+    - iApply ("IH" with "[%] HΦ"). omega.
     - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 969586fdf..02888a70c 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -25,7 +25,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" with "!")].
+  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
   iIntros {v} "?"; iExists x; by iSplit.
 Qed.
 
@@ -43,7 +43,7 @@ Lemma Q_res_join γ : (barrier_res γ Ψ1 ★ barrier_res γ Ψ2) ⊢ ▷ barrie
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
-  iDestruct (one_shot_agree γ x x' with "- !") 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.
@@ -68,8 +68,7 @@ Proof.
     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 with "[] Hr") as "Hr".
-    { iIntros "?". by iApply (P_res_split with "-"). }
+  - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
     iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
     wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
       (λ _, barrier_res γ Ψ2)%I); first done.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 89dd05d94..053847b1e 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -58,13 +58,13 @@ Proof.
     + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
     iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ OneShotPending) ∨
-       ∃ n : Z, v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "Hv" with "-".
+       ∃ n : Z, v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "Hv" with "[-]".
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
       + iExists (InjLV #0). iFrame "Hl". iLeft; by iSplit.
       + iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
     iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
     iAssert (one_shot_inv γ l ★ (v = InjLV #0 ∨ ∃ n : Z,
-      v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "[$ #Hv]" with "-".
+      v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "[$ #Hv]" with "[-]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
       + iSplit. iLeft; by iSplitL "Hl". by iLeft.
       + iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
@@ -76,7 +76,7 @@ Proof.
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct (own_valid with "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.
@@ -91,7 +91,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" with "!").
+  - iIntros {n} "! _". wp_proj. iApply "Hf1".
   - iIntros "! _". wp_proj.
     iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
 Qed.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d7431c406..3052147b6 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -31,7 +31,7 @@ Proof.
   iFrame "Ha Hac".
   iExists (S j + z1), z2.
   iNext.
-  iApply ("H3" $! _ 0 with "H1 ! [] !").
+  iApply ("H3" $! _ 0 with "H1 []").
   - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
   - done.
 Qed.
@@ -67,8 +67,8 @@ Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
   (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
 Proof.
   iIntros "H1 H2".
-  iRewrite (uPred.eq_sym x x with "- !"). iApply uPred.eq_refl.
-  iRewrite -("H1" $! _ with "- !"); first done.
+  iRewrite (uPred.eq_sym x x with "[#]"). iApply uPred.eq_refl.
+  iRewrite -("H1" $! _ with "[#]"); first done.
   iApply uPred.eq_refl.
 Qed.
 
-- 
GitLab