Commit b623cbea authored by Robbert Krebbers's avatar Robbert Krebbers

Make use of nested `iSpecialize`.

parent 3b5472b5
......@@ -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.
......
......@@ -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 Σ) :
......
......@@ -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.
......
......@@ -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.
......
......@@ -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 :
......
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment