From b623cbeaf3c90fd950154a4ba40a85f3d33b103a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Dec 2018 14:18:08 +0100
Subject: [PATCH] Make use of nested `iSpecialize`.

---
 theories/base_logic/lib/invariants.v    | 4 ++--
 theories/heap_lang/lib/par.v            | 2 +-
 theories/program_logic/adequacy.v       | 3 +--
 theories/program_logic/hoare.v          | 6 +++---
 theories/program_logic/total_adequacy.v | 4 ++--
 theories/program_logic/weakestpre.v     | 4 ++--
 6 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 1ecc9bcc7..1405eaf78 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/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.
 
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 47498b0d0..5fd18ec3f 100644
--- a/theories/heap_lang/lib/par.v
+++ b/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 Σ) :
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index fdbb25a23..770e56fb1 100644
--- a/theories/program_logic/adequacy.v
+++ b/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.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index f75756fa6..844842a89 100644
--- a/theories/program_logic/hoare.v
+++ b/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.
 
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index c742a636d..b6243370d 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/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 :
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 8cfeea29f..92ddffd16 100644
--- a/theories/program_logic/weakestpre.v
+++ b/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.
-- 
GitLab