Commit 160cd18c authored by Robbert Krebbers's avatar Robbert Krebbers

Curried version of wp_wand.

parent 9f79b4c9
Pipeline #2982 passed with stage
in 9 minutes and 52 seconds
......@@ -13,5 +13,5 @@ Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply (wp_wand_r with "[- $HΦ]"). iIntros (v) "[% ?]"; subst. by wp_if.
iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
......@@ -30,7 +30,7 @@ Proof.
rewrite /par. wp_value. wp_let. wp_proj.
wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand_r with "[- $Hf2]"); iIntros (v) "H2". wp_let.
iApply (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_let.
Qed.
......
......@@ -58,7 +58,7 @@ Proof.
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply (wp_wand_r with "[ $Hf]"); iIntros (v) "Hv".
- wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
......
......@@ -64,7 +64,7 @@ Lemma ht_vs E P P' Φ Φ' e :
{{ P }} e @ E {{ Φ }}.
Proof.
iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
iApply wp_fupd; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
iIntros (v) "Hv". by iApply "HΦ".
Qed.
......@@ -75,7 +75,7 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
Proof.
iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
iMod ("Hvs" with "HP") as "HP". iModIntro.
iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
iIntros (v) "Hv". by iApply "HΦ".
Qed.
......@@ -84,7 +84,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
{{ P }} K e @ E {{ Φ' }}.
Proof.
iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
iIntros (v) "Hv". by iApply "HwpK".
Qed.
......
......@@ -275,15 +275,18 @@ Lemma wp_frame_step_r' E e Φ R :
to_val e = None WP e @ E {{ Φ }} R WP e @ E {{ v, Φ v R }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.
Lemma wp_wand_l E e Φ Ψ :
( v, Φ v - Ψ v) WP e @ E {{ Φ }} WP e @ E {{ Ψ }}.
Lemma wp_wand E e Φ Ψ :
WP e @ E {{ Φ }} ( v, Φ v - Ψ v) - WP e @ E {{ Ψ }}.
Proof.
iIntros "[H Hwp]". iApply (wp_strong_mono E); auto.
iIntros "Hwp H". iApply (wp_strong_mono E); auto.
iFrame "Hwp". iIntros (?) "?". by iApply "H".
Qed.
Lemma wp_wand_l E e Φ Ψ :
( v, Φ v - Ψ v) WP e @ E {{ Φ }} WP e @ E {{ Ψ }}.
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
Lemma wp_wand_r E e Φ Ψ :
WP e @ E {{ Φ }} ( v, Φ v - Ψ v) WP e @ E {{ Ψ }}.
Proof. by rewrite comm wp_wand_l. Qed.
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
End wp.
(** Proofmode class instances *)
......
......@@ -31,7 +31,7 @@ Section client.
iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]".
wp_seq. wp_load.
iApply wp_wand_r. iSplitR; [iApply "Hf"|by iIntros (v) "_"].
iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
Qed.
Lemma client_safe : heapN N heap_ctx WP client {{ _, True }}.
......
......@@ -37,7 +37,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
Proof.
iIntros "[Hl #He]". wp_apply (wait_spec with "[- $Hl]"); simpl.
iDestruct 1 as (x) "[#Hγ Hx]".
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
iIntros (v) "?"; iExists x; by iSplit.
Qed.
......@@ -81,7 +81,7 @@ Proof.
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par (λ _, True)%I workers_post with "[- $Hh]").
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
- wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iMod (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). }
......
......@@ -94,6 +94,6 @@ Proof.
iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
- iIntros (n) "!# _". wp_proj. iApply "Hf1".
- iIntros "!# _". wp_proj.
iApply (wp_wand_r with "[- $Hf2]"). by iIntros (v) "#? !# _".
iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
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