Merge branch 'more_spec_patterns'

ProofMode.md

@@ -203,6 +203,8 @@ appear at the top level:
 - `!#` : introduce an always modality (given that the spatial context is empty).
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
+- `//` : perform `try done` on all goals.
+- `//=` : syntactic sugar for `/= //`
 - `*` : introduce all universal quantifiers.
 - `**` : introduce all universal quantifiers, as well as all arrows and wands.
 
@@ -235,30 +237,52 @@ _specification patterns_ to express splitting of hypotheses:
 
 - `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
   spatial, it will be consumed.
-- `[H1 ... Hn]` : generate a goal with the (spatial) hypotheses `H1 ... Hn` and
-  all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
-  consumed. Hypotheses may be prefixed with a `$`, which results in them being
-  framed in the generated goal.
-- `[-H1 ... Hn]` : negated form of the above pattern.
-- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
-  is a modality, in which case the modality will be kept in the generated goal
-  for the premise will be wrapped into the modality.
-- `>[-H1 ... Hn]`  : negated form of the above pattern.
-- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
-  lemma).
-- `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P`
-  persistent. Using this pattern, all hypotheses are available in the goal for
-  `P`, as well the remaining goal.
-- `[%]` : This pattern can be used when eliminating `P -∗ Q` when `P` is pure.
-  It will generate a Coq goal for `P` and does not consume any hypotheses.
+
+- `[H1 .. Hn]` and `[H1 .. Hn //]` : generate a goal for the premise with the
+  (spatial) hypotheses `H1 ... Hn` and all persistent hypotheses. The spatial
+  hypotheses among `H1 ... Hn` will be consumed, and will not be available for
+  subsequent goals. Hypotheses prefixed with a `$` will be framed in the
+  goal for the premise. The pattern can be terminated with a `//`, which causes
+  `done` to be called to close the goal (after framing).
+- `[-H1 ... Hn]` and `[-H1 ... Hn //]` : the negated forms of the above
+  patterns, where the goal for the premise will have all spatial premises except
+  `H1 .. Hn`.
+
+- `[> H1 ... Hn]` and `[> H1 ... Hn //]` : like the above patterns, but these
+  patterns can only be used if the goal is a modality `M`, in which case
+  the goal for the premise will be wrapped in the modality `M`.
+- `[> -H1 ... Hn]` and `[> -H1 ... Hn //]` : the negated forms of the above
+  patterns.
+
+- `[# $H1 .. $Hn]` and `[# $H1 .. $Hn //]` : generate a goal for a persistent
+  premise in which all hypotheses are available. This pattern does not consume
+  any hypotheses; all hypotheses are available in the goal for the premise, as
+  well in the subsequent goal. The hypotheses `$H1 ... $Hn` will be framed in
+  the goal for the premise. These patterns can be terminated with a `//`, which
+  causes `done` to be called to close the goal (after framing).
+- `[%]` and `[% //]` : generate a Coq goal for a pure premise. This pattern
+  does not consume any hypotheses. The pattern can be terminated with a `//`,
+  which causes `done` to be called to close the goal.
+
+- `[$]` : solve the premise by framing. It will first repeatedly frame the
+  spatial hypotheses, and then repeatedly frame the persistent hypotheses.
+  Spatial hypothesis that are not framed are carried over to the subsequent
+  goal.
+- `[> $]` : like the above pattern, but this pattern can only be used if the
+  goal is a modality `M`, in which case the goal for the premise will be wrapped
+  in the modality `M` before framing.
+- `[# $]` : solve the persistent premise by framing. It will first repeatedly
+  frame the spatial hypotheses, and then repeatedly frame the persistent
+  hypotheses. This pattern does not consume any hypotheses.
 
 For example, given:
 
-        H : □ P -∗ P 2 -∗ x = 0 -∗ Q1 ∗ Q2
+        H : □ P -∗ P 2 -∗ R -∗ x = 0 -∗ Q1 ∗ Q2
+
+One can write:
 
-You can write:
+        iDestruct ("H" with "[#] [H1 $H2] [$] [% //]") as "[H4 H5]".
 
-        iDestruct ("H" with "[#] [H1 H2] [%]") as "[H4 H5]".
 
 Proof mode terms
 ================

theories/base_logic/lib/boxes.v

@@ -225,7 +225,7 @@ Lemma box_empty E f P :
 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 (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
     iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.

theories/base_logic/lib/wsat.v

@@ -104,7 +104,7 @@ Qed.
 Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup I i P with "[$Hw $Hi]") as (Q) "[% #HPQ]".
+  iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
     iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
@@ -114,9 +114,9 @@ Qed.
 Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup with "[$Hw $Hi]") as (Q) "[% #HPQ]".
+  iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
-  - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
+  - iDestruct (ownD_singleton_twice with "[$]") as %[].
   - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
@@ -127,7 +127,7 @@ Lemma ownI_alloc φ P :
 Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
   iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
-  iMod (own_updateP with "HE") as "HE".
+  iMod (own_updateP with "[$]") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
@@ -149,7 +149,7 @@ Lemma ownI_alloc_open φ P :
 Proof.
   iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
   iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
-  iMod (own_updateP with "HD") as "HD".
+  iMod (own_updateP with "[$]") as "HD".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }

theories/heap_lang/lib/barrier/proof.v

@@ -93,7 +93,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
 Proof.
   iIntros (Φ) "HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
-  iApply ("HΦ" with ">[-]").
+  iApply ("HΦ" with "[> -]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
@@ -102,7 +102,7 @@ Proof.
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { done. }
   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γ'");
@@ -140,7 +140,7 @@ Proof.
   wp_load. destruct p.
   - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
     { iSplit; first done. rewrite /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. }
     iModIntro. wp_if.
     iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
@@ -175,7 +175,7 @@ Proof.
     rewrite /barrier_inv /=. iNext. iFrame "Hl".
     by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
   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γ");

theories/program_logic/weakestpre.v

@@ -129,11 +129,11 @@ Lemma wp_strong_mono E1 E2 e Φ Ψ :
 Proof.
   iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
-  { iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). }
+  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
-  iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iMod ("H" with "[$]") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
+  iMod ("H" with "[//]") as "($ & H & $)"; auto.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
@@ -155,10 +155,10 @@ Proof.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[]") as "(Hphy & H & $)"; first done.
+  iMod ("H" with "[//]") as "(Hphy & H & $)".
   rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
-  - iDestruct "H" as ">> $". iFrame. eauto.
-  - iMod ("H" with "Hphy") as "[H _]".
+  - iDestruct "H" as ">> $". eauto with iFrame.
+  - iMod ("H" with "[$]") as "[H _]".
     iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
 Qed.
 
@@ -167,9 +167,9 @@ Lemma wp_step_fupd E1 E2 e P Φ :
   (|={E1,E2}▷=> P) -∗ WP e @ E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" $! _ with "Hσ") as "[$ H]".
+  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
+  iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
   iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
   iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
@@ -181,11 +181,11 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
-  iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]". iModIntro; iSplit.
+  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
   iNext; iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
+  iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
   by iApply "IH".
 Qed.
 

theories/proofmode/coq_tactics.v

@@ -573,6 +573,24 @@ Proof.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
+Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
+Proof. by unlock. Qed.
+
+Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
+  envs_lookup_delete j Δ = Some (q, R, Δ') →
+  IntoWand R P1 P2 →
+  ElimModal P1' P1 Q Q →
+  (Δ' ⊢ P1' ∗ locked Q') →
+  Q' = (P2 -∗ Q)%I →
+  Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+  rewrite envs_lookup_sound //. rewrite HPQ -lock.
+  rewrite (into_wand R) assoc -(comm _ P1') -assoc always_if_elim.
+  rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
+  by rewrite assoc !wand_elim_r.
+Qed.
+
 Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand R P1 P2 → FromPure P1 φ →
@@ -643,14 +661,23 @@ Qed.
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ1 ⊢ P) → PersistentP P →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  PersistentP P →
+  (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ?? HP ? <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
+  intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
   rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.
 
+Lemma tac_assert_pure Δ Δ' j P φ Q :
+  envs_app false (Esnoc Enil j P) Δ = Some Δ' →
+  FromPure P φ →
+  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros ??? <-. rewrite envs_app_sound //; simpl.
+  by rewrite right_id -(from_pure P) pure_True // -always_impl_wand True_impl.
+Qed.
+
 Lemma tac_pose_proof Δ Δ' j P Q :
   P →
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →

theories/proofmode/intro_patterns.v

@@ -15,6 +15,7 @@ Inductive intro_pat :=
   | IAlwaysIntro : intro_pat
   | IModalIntro : intro_pat
   | ISimpl : intro_pat
+  | IDone : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
   | IClear : string → intro_pat
@@ -87,6 +88,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
   | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
   | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
+  | TDone :: ts => parse_go ts (SPat IDone :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
   | TBraceL :: ts => parse_clear ts k

theories/proofmode/spec_patterns.v

@@ -2,22 +2,31 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import tokens.
 Set Default Proof Using "Type".
 
+Inductive goal_kind := GSpatial | GModal | GPersistent.
+
 Record spec_goal := SpecGoal {
-  spec_goal_modal : bool;
+  spec_goal_kind : goal_kind;
   spec_goal_negate : bool;
   spec_goal_frame : list string;
-  spec_goal_hyps : list string
+  spec_goal_hyps : list string;
+  spec_goal_done : bool
 }.
 
 Inductive spec_pat :=
-  | SGoal : spec_goal → spec_pat
-  | SGoalPersistent : spec_pat
-  | SGoalPure : spec_pat
+  | SForall : spec_pat
   | SName : string → spec_pat
-  | SForall : spec_pat.
+  | SPureGoal : bool → spec_pat
+  | SGoal : spec_goal → spec_pat
+  | SAutoFrame : goal_kind → spec_pat.
 
+Definition goal_kind_modal (k : goal_kind) : bool :=
+  match k with GModal => true | _ => false end.
 Definition spec_pat_modal (p : spec_pat) : bool :=
-  match p with SGoal g => spec_goal_modal g | _ => false end.
+  match p with
+  | SGoal g => goal_kind_modal (spec_goal_kind g)
+  | SAutoFrame k => goal_kind_modal k
+  | _ => false
+  end.
 
 Module spec_pat.
 Inductive state :=
@@ -28,30 +37,33 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
   match ts with
   | [] => Some (reverse k)
   | TName s :: ts => parse_go ts (SName s :: k)
-  | TBracketL :: TAlways :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
-  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
-  | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
-  | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
-  | TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
+  | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
+     parse_go ts (SAutoFrame GPersistent :: k)
+  | TBracketL :: TFrame :: TBracketR :: ts =>
+     parse_go ts (SAutoFrame GSpatial :: k)
+  | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
+     parse_go ts (SAutoFrame GModal :: k)
+  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
+  | TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
+  | TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
+  | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
+  | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
-with parse_goal (ts : list token) (g : spec_goal)
+with parse_goal (ts : list token)
+    (ki : goal_kind) (neg : bool) (frame hyps : list string)
     (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | TMinus :: ts =>
-     guard (¬spec_goal_negate g ∧ spec_goal_frame g = [] ∧ spec_goal_hyps g = []);
-     parse_goal ts (SpecGoal (spec_goal_modal g) true
-       (spec_goal_frame g) (spec_goal_hyps g)) k
-  | TName s :: ts =>
-     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (spec_goal_frame g) (s :: spec_goal_hyps g)) k
-  | TFrame :: TName s :: ts =>
-     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (s :: spec_goal_frame g) (spec_goal_hyps g)) k
+     guard (¬neg ∧ frame = [] ∧ hyps = []);
+     parse_goal ts ki true frame hyps k
+  | TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
+  | TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
+  | TDone :: TBracketR :: ts =>
+     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
   | TBracketR :: ts =>
-     parse_go ts (SGoal (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
+     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false) :: k)
   | _ => None
   end.
 Definition parse (s : string) : option (list spec_pat) :=

theories/proofmode/tactics.v

@@ -261,6 +261,72 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
     constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
   iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
 
+(** * Basic introduction tactics *)
+Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
+  try iStartProof;
+  try first
+    [(* (∀ _, _) *) apply tac_forall_intro
+    |(* (?P → _) *) eapply tac_impl_intro_pure;
+      [let P := match goal with |- IntoPure ?P _ => P end in
+       apply _ || fail "iIntro:" P "not pure"|]
+    |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
+      [let P := match goal with |- IntoPure ?P _ => P end in
+       apply _ || fail "iIntro:" P "not pure"|]
+    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
+    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
+  intros x.
+
+Local Tactic Notation "iIntro" constr(H) :=
+  iStartProof;
+  first
+  [ (* (?Q → _) *)
+    eapply tac_impl_intro with _ H; (* (i:=H) *)
+      [reflexivity || fail 1 "iIntro: introducing" H
+                             "into non-empty spatial context"
+      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | (* (_ -∗ _) *)
+    eapply tac_wand_intro with _ H; (* (i:=H) *)
+      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "#" constr(H) :=
+  iStartProof;
+  first
+  [ (* (?P → _) *)
+    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
+       apply _ || fail 1 "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | (* (?P -∗ _) *)
+    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
+       apply _ || fail 1 "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "_" :=
+  try iStartProof;
+  first
+  [ (* (?Q → _) *) apply tac_impl_intro_drop
+  | (* (_ -∗ _) *) apply tac_wand_intro_drop
+  | (* (∀ _, _) *) iIntro (_)
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntroForall" :=
+  try iStartProof;
+  lazymatch goal with
+  | |- ∀ _, ?P => fail
+  | |- ∀ _, _ => intro
+  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
+  end.
+Local Tactic Notation "iIntro" :=
+  try iStartProof;
+  lazymatch goal with
+  | |- _ → ?P => intro
+  | |- _ ⊢ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  end.
+
 (** * Specialize *)
 Record iTrm {X As} :=
   ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
@@ -303,36 +369,58 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
           let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
          |env_cbv; reflexivity|go H1 pats]
-    | SGoalPersistent :: ?pats =>
-       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
+    | SPureGoal ?d :: ?pats =>
+       eapply tac_specialize_assert_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"
+         |let Q := match goal with |- FromPure ?Q _ => Q end in
+          apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
-         |(*goal*)
+         |done_if d (*goal*)
          |go H1 pats]
-    | SGoalPure :: ?pats =>
-       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
+    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
+       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- FromPure ?Q _ => Q end in
-          apply _ || fail "iSpecialize:" Q "not pure"
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity
-         |(*goal*)
+         |iFrame Hs_frame; done_if d (*goal*)
          |go H1 pats]
-    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
+    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
+       fail "iSpecialize: cannot select hypotheses for persistent premise"
+    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
        eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |match m with
-          | false => apply elim_modal_dummy
-          | true => apply _ || fail "iSpecialize: goal not a modality"
+         |lazymatch m with
+          | GSpatial => apply elim_modal_dummy
+          | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
-         |iFrame Hs_frame (*goal*)
+         |iFrame Hs_frame; done_if d (*goal*)
          |go H1 pats]
+    | SAutoFrame GPersistent :: ?pats =>
+       eapply tac_specialize_assert_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
+         |solve [iFrame "∗ #"]
+         |go H1 pats]
+    | SAutoFrame ?m :: ?pats =>
+       eapply tac_specialize_frame with _ H1 _ _ _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |lazymatch m with
+          | GSpatial => apply elim_modal_dummy
+          | GModal => apply _ || fail "iSpecialize: goal not a modality"
+          end
+         |iFrame "∗ #"; apply tac_unlock
+           || fail "iSpecialize: premise cannot be solved by framing"
+         |reflexivity]; iIntro H1; go H1 pats
     end in let pats := spec_pat.parse pat in go H pats.
 
 (* The argument [p] denotes whether the conclusion of the specialized term is
@@ -740,71 +828,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
   iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
 
 (** * Introduction tactic *)
-Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
-  try iStartProof;
-  try first
-    [(* (∀ _, _) *) apply tac_forall_intro
-    |(* (?P → _) *) eapply tac_impl_intro_pure;
-      [let P := match goal with |- IntoPure ?P _ => P end in
-       apply _ || fail "iIntro:" P "not pure"|]
-    |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
-      [let P := match goal with |- IntoPure ?P _ => P end in
-       apply _ || fail "iIntro:" P "not pure"|]
-    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
-    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
-  intros x.
-
-Local Tactic Notation "iIntro" constr(H) :=
-  iStartProof;
-  first
-  [ (* (?Q → _) *)
-    eapply tac_impl_intro with _ H; (* (i:=H) *)
-      [reflexivity || fail 1 "iIntro: introducing" H
-                             "into non-empty spatial context"
-      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
-  | (* (_ -∗ _) *)
-    eapply tac_wand_intro with _ H; (* (i:=H) *)
-      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
-  | fail 1 "iIntro: nothing to introduce" ].
-
-Local Tactic Notation "iIntro" "#" constr(H) :=
-  iStartProof;
-  first
-  [ (* (?P → _) *)
-    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- IntoPersistentP ?P _ => P end in
-       apply _ || fail 1 "iIntro: " P " not persistent"
-      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
-  | (* (?P -∗ _) *)
-    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- IntoPersistentP ?P _ => P end in
-       apply _ || fail 1 "iIntro: " P " not persistent"
-      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
-  | fail 1 "iIntro: nothing to introduce" ].
-
-Local Tactic Notation "iIntro" "_" :=
-  try iStartProof;
-  first
-  [ (* (?Q → _) *) apply tac_impl_intro_drop