Merge branch 'robbert/nested_ispecialize' into 'master'

Allow `iSpecialize` to be nested.

See merge request FP/iris-coq!198

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/base_logic/lib/invariants.v

@@ -102,8 +102,8 @@ Proof.
   rewrite difference_diag_L.
   iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
   rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
-  iIntros (E') "HP". iSpecialize ("H" with "HP").
-  iPoseProof (fupd_mask_frame_r _ _ E' with "H") as "H"; first set_solver.
+  iIntros (E') "HP".
+  iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
   by rewrite left_id_L.
 Qed.
 

theories/heap_lang/lib/par.v

@@ -31,7 +31,7 @@ Proof.
   iIntros (l) "Hl". wp_let. wp_bind (f2 _).
   wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
-  iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". by wp_pures.
+  iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :

theories/program_logic/adequacy.v

@@ -168,8 +168,7 @@ Proof.
   iIntros (?) "Hφ Hσ He Ht". rewrite Nat_iter_S_r.
   iDestruct (wptp_steps _ n with "Hσ He Ht") as "H"; first done.
   iApply (step_fupdN_wand with "H"). iDestruct 1 as (e2' t2' ->) "[Hσ _]".
-  iSpecialize ("Hφ" with "Hσ").
-  iMod (fupd_plain_mask_empty _ ⌜φ⌝%I with "Hφ") as %?.
+  iMod (fupd_plain_mask_empty _ ⌜φ⌝%I with "(Hφ Hσ)") as %?.
   by iApply step_fupd_intro.
 Qed.
 End adequacy.

theories/program_logic/hoare.v

@@ -75,7 +75,7 @@ Lemma ht_vs s E P P' Φ Φ' e :
   ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
-  iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
+  iApply wp_fupd. iApply (wp_wand with "(Hwp HP)").
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
@@ -85,7 +85,7 @@ Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
-  iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
+  iApply (wp_wand with "(Hwp HP)").
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
@@ -94,7 +94,7 @@ Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
   ⊢ {{ P }} K e @ s; E {{ Φ' }}.
 Proof.
   iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
-  iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
+  iApply (wp_wand with "(Hwpe HP)").
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
 

theories/program_logic/total_adequacy.v

@@ -94,12 +94,12 @@ Proof.
   iMod ("IH" with "Hσ1") as "[_ IH]".
   iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
   iModIntro. iExists (length efs + n). iFrame "Hσ".
-  iApply (twptp_app [_] with "[IH]"); first by iApply "IH".
+  iApply (twptp_app [_] with "(IH [//])").
   clear. iInduction efs as [|e efs] "IH"; simpl.
   { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n1 Hstep).
     destruct Hstep; simplify_eq/=; discriminate_list. }
   iDestruct "IHfork" as "[[IH' _] IHfork]".
-  iApply (twptp_app [_] with "[IH']"). by iApply "IH'". by iApply "IH".
+  iApply (twptp_app [_] with "(IH' [//])"). by iApply "IH".
 Qed.
 
 Lemma twptp_total n σ t :

theories/program_logic/weakestpre.v

@@ -292,7 +292,7 @@ Section proofmode_classes.
   Proof.
     intros ?. rewrite /ElimAcc.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
-    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+    iApply (wp_wand with "(Hinner Hα)").
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
 
@@ -304,7 +304,7 @@ Section proofmode_classes.
     rewrite /ElimAcc.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply wp_fupd.
-    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+    iApply (wp_wand with "(Hinner Hα)").
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
 End proofmode_classes.

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

@@ -470,6 +470,12 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
      |(* subgoal *)]
   |fail 1 "iIntro: nothing to introduce"].
 
+Local Tactic Notation "iIntro" constr(H) "as" constr(p) :=
+  lazymatch p with
+  | true => iIntro #H
+  | _ =>  iIntro H
+  end.
+
 Local Tactic Notation "iIntro" "_" :=
   iStartProof;
   first
@@ -716,8 +722,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 +737,33 @@ 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] *)
+           |iIntro H1 as p]);
+         (* 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 ||
@@ -1499,12 +1534,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
     lazymatch Hs with
     | [] => tac
     | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
-    | ESelIdent ?p ?H :: ?Hs =>
-       iRevertHyp H; go Hs;
-       match p with
-       | true => iIntro #H
-       | false => iIntro H
-       end
+    | ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
     end in
   try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
 

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) :=