Allow `iSpecialize` to be nested.

It now supports the specialization pattern `(H spat1 .. spatn)`, which first
recursively specializes the hypothesis `H` using the specialization patterns
`spat1 .. spatn`.

ProofMode.md

@@ -260,6 +260,11 @@ _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.
 
+- `(H spat1 .. spatn)` : first recursively specialize the hypothesis `H` using
+  the specialization patterns `spat1 .. spatn`, and finally use the result of
+  the specialization of `H` (it should match the premise exactly). If `H` is
+  spatial, it will be consumed.
+
 - `[H1 .. Hn]` and `[H1 .. Hn //]` : generate a goal for the premise with the
   (spatial) hypotheses `H1 ... Hn` and all intuitionistic hypotheses. The
   spatial hypotheses among `H1 ... Hn` will be consumed, and will not be

tests/proofmode.ref

@@ -74,6 +74,22 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ▷^(S n + S m) emp
   
+"test_specialize_nested_intuitionistic"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  φ : Prop
+  P, P2, Q, R1, R2 : PROP
+  H : φ
+  ============================
+  "HP" : P
+  "HQ" : P -∗ Q
+  --------------------------------------□
+  "HR" : R2
+  --------------------------------------∗
+  R2
+  
 "test_iSimpl_in"
      : string
 1 subgoal

tests/proofmode.v

@@ -405,6 +405,45 @@ Lemma test_assert_pure (φ : Prop) P :
   φ → P ⊢ P ∗ ⌜φ⌝.
 Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
 
+Lemma test_specialize_very_nested (φ : Prop) P P2 Q R1 R2 :
+  φ →
+  P -∗ P2 -∗
+  (<affine> ⌜ φ ⌝ -∗ P2 -∗ Q) -∗
+  (P -∗ Q -∗ R1) -∗
+  (R1 -∗ True -∗ R2) -∗
+  R2.
+Proof.
+  iIntros (?) "HP HP2 HQ H1 H2".
+  by iApply ("H2" with "(H1 HP (HQ [% //] [-])) [//]").
+Qed.
+
+Lemma test_specialize_very_very_nested P1 P2 P3 P4 P5 :
+  □ P1 -∗
+  □ (P1 -∗ P2) -∗
+  (P2 -∗ P2 -∗ P3) -∗
+  (P3 -∗ P4) -∗
+  (P4 -∗ P5) -∗
+  P5.
+Proof.
+  iIntros "#H #H1 H2 H3 H4".
+  by iSpecialize ("H4" with "(H3 (H2 (H1 H) (H1 H)))").
+Qed.
+
+Check "test_specialize_nested_intuitionistic".
+Lemma test_specialize_nested_intuitionistic (φ : Prop) P P2 Q R1 R2 :
+  φ →
+  □ P -∗ □ (P -∗ Q) -∗ (Q -∗ Q -∗ R2) -∗ R2.
+Proof.
+  iIntros (?) "#HP #HQ HR".
+  iSpecialize ("HR" with "(HQ HP) (HQ HP)").
+  Show.
+  done.
+Qed.
+
+Lemma test_specialize_intuitionistic P Q :
+  □ P -∗ □ (P -∗ Q) -∗ □ Q.
+Proof. iIntros "#HP #HQ". iSpecialize ("HQ" with "HP"). done. Qed.
+
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : PROP.
 Proof.
   iIntros (H).
@@ -435,7 +474,7 @@ Lemma test_with_ident P Q R : P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R.
 Proof.
   iIntros "? HQ H".
   iMatchHyp (fun H _ =>
-    iApply ("H" with [spec_patterns.SIdent H; spec_patterns.SIdent "HQ"])).
+    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
 Qed.
 
 Lemma iFrame_with_evar_r P Q :

theories/proofmode/coq_tactics.v

@@ -221,27 +221,21 @@ 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. *)
-Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
-  envs_lookup_delete false i Δ = Some (p, P1, Δ') →
+Lemma tac_specialize remove_intuitionistic Δ Δ' Δ'' i p j q P1 P2 R Q :
+  envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
   envs_lookup j Δ' = Some (q, R) →
   IntoWand q p R P1 P2 →
-  match p with
-  | true  => envs_simple_replace j q (Esnoc Enil j P2) Δ
-  | false => envs_replace j q false (Esnoc Enil j P2) Δ'
-             (* remove [i] and make [j] spatial *)
-  end = Some Δ'' →
+  envs_replace j q (p && q) (Esnoc Enil j P2) Δ' = Some Δ'' →
   envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hj ? Hj' <-.
-  rewrite (envs_lookup_sound' _ false) //; simpl. destruct p; simpl.
-  - move: Hj; rewrite envs_delete_intuitionistic=> Hj.
-    rewrite envs_simple_replace_singleton_sound //; simpl.
-    rewrite -intuitionistically_if_idemp -intuitionistically_idemp into_wand /=.
-    rewrite assoc (intuitionistically_intuitionistically_if q).
-    by rewrite intuitionistically_if_sep_2 wand_elim_r wand_elim_r.
-  - move: Hj Hj'; rewrite envs_delete_spatial=> Hj Hj'.
-    rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Δ'') //; simpl.
-    by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
+  rewrite envs_entails_eq /IntoWand.
+  intros [? ->]%envs_lookup_delete_Some ? HR ? <-.
+  rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
+  rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
+  - rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
+    rewrite {1}(intuitionistically_intuitionistically_if q).
+    by rewrite HR assoc intuitionistically_if_sep_2 !wand_elim_r.
+  - by rewrite HR assoc !wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :

theories/proofmode/ltac_tactics.v

@@ -716,8 +716,10 @@ Ltac iSpecializePat_go H1 pats :=
     | SForall :: ?pats =>
        idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
        iSpecializePat_go H1 pats
-    | SIdent ?H2 :: ?pats =>
-       notypeclasses refine (tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
+    | SIdent ?H2 [] :: ?pats =>
+       (* If we not need to specialize [H2] we can avoid a lot of unncessary
+       context manipulation. *)
+       notypeclasses refine (tac_specialize false _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H2 := pretty_ident H2 in
           fail "iSpecialize:" H2 "not found"
@@ -729,6 +731,36 @@ Ltac iSpecializePat_go H1 pats :=
           let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
           fail "iSpecialize: cannot instantiate" P "with" Q
          |pm_reflexivity|iSpecializePat_go H1 pats]
+    | SIdent ?H2 ?pats1 :: ?pats =>
+       (* If [H2] is in the intuitionistic context, we copy it into a new
+       hypothesis [Htmp], so that it can be used multiple times. *)
+       let H2tmp := iFresh in
+       iPoseProofCoreHyp H2 as H2tmp;
+       (* Revert [H1] and re-introduce it later so that it will not be consumsed
+       by [pats1]. *)
+       iRevertHyp H1 with (fun p =>
+         iSpecializePat_go H2tmp pats1;
+           [.. (* side-conditions of [iSpecialize] *)
+           |lazymatch p with
+            | true => iIntro #H1
+            | _ => iIntro H1
+            end]);
+         (* We put the stuff below outside of the closure to get less verbose
+         Ltac backtraces (which would otherwise include the whole closure). *)
+         [.. (* side-conditions of [iSpecialize] *)
+         |(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
+          notypeclasses refine (tac_specialize true _ _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _ _);
+            [pm_reflexivity ||
+             let H2tmp := pretty_ident H2tmp in
+             fail "iSpecialize:" H2tmp "not found"
+            |pm_reflexivity ||
+             let H1 := pretty_ident H1 in
+             fail "iSpecialize:" H1 "not found"
+            |iSolveTC ||
+             let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
+             let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
+             fail "iSpecialize: cannot instantiate" P "with" Q
+            |pm_reflexivity|iSpecializePat_go H1 pats]]
     | SPureGoal ?d :: ?pats =>
        notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||

theories/proofmode/spec_patterns.v

@@ -14,7 +14,7 @@ Record spec_goal := SpecGoal {
 
 Inductive spec_pat :=
   | SForall : spec_pat
-  | SIdent : ident → spec_pat
+  | SIdent : ident → list spec_pat → spec_pat
   | SPureGoal (perform_done : bool) : spec_pat
   | SGoal : spec_goal → spec_pat
   | SAutoFrame : goal_kind → spec_pat.
@@ -29,31 +29,50 @@ Definition spec_pat_modal (p : spec_pat) : bool :=
   end.
 
 Module spec_pat.
-Inductive state :=
-  | StTop : state
-  | StAssert : spec_goal → state.
+Inductive stack_item :=
+  | StPat : spec_pat → stack_item
+  | StIdent : string → stack_item.
+Notation stack := (list stack_item).
 
-Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
+Fixpoint close (k : stack) (ps : list spec_pat) : option (list spec_pat) :=
+  match k with
+  | [] => Some ps
+  | StPat p :: k => close k (p :: ps)
+  | StIdent _ :: _ => None
+  end.
+
+Fixpoint close_ident (k : stack) (ps : list spec_pat) : option stack :=
+  match k with
+  | [] => None
+  | StPat p :: k => close_ident k (p :: ps)
+  | StIdent s :: k => Some (StPat (SIdent s ps) :: k)
+  end.
+
+Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
   match ts with
-  | [] => Some (reverse k)
-  | TName s :: ts => parse_go ts (SIdent s :: k)
+  | [] => close k []
+  | TParenL :: TName s :: ts => parse_go ts (StIdent s :: k)
+  | TParenR :: ts => k ← close_ident k []; parse_go ts k
+  | TName s :: ts => parse_go ts (StPat (SIdent s []) :: k)
   | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
-     parse_go ts (SAutoFrame GIntuitionistic :: k)
+     parse_go ts (StPat (SAutoFrame GIntuitionistic) :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
-     parse_go ts (SAutoFrame GSpatial :: k)
+     parse_go ts (StPat (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)
+     parse_go ts (StPat (SAutoFrame GModal) :: k)
+  | TBracketL :: TPure :: TBracketR :: ts =>
+     parse_go ts (StPat (SPureGoal false) :: k)
+  | TBracketL :: TPure :: TDone :: TBracketR :: ts =>
+     parse_go ts (StPat (SPureGoal true) :: k)
   | TBracketL :: TAlways :: ts => parse_goal ts GIntuitionistic 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)
+  | TForall :: ts => parse_go ts (StPat SForall :: k)
   | _ => None
   end
 with parse_goal (ts : list token)
     (ki : goal_kind) (neg : bool) (frame hyps : list ident)
-    (k : list spec_pat) : option (list spec_pat) :=
+    (k : stack) : option (list spec_pat) :=
   match ts with
   | TMinus :: ts =>
      guard (¬neg ∧ frame = [] ∧ hyps = []);
@@ -61,9 +80,9 @@ with parse_goal (ts : list token)
   | TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
   | TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
   | TDone :: TBracketR :: ts =>
-     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
+     parse_go ts (StPat (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true)) :: k)
   | TBracketR :: ts =>
-     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false) :: k)
+     parse_go ts (StPat (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false)) :: k)
   | _ => None
   end.
 Definition parse (s : string) : option (list spec_pat) :=