Commit 86672bca authored by Robbert Krebbers's avatar Robbert Krebbers

More simpl to reduce %V scopes.

parent 37b070a8
......@@ -36,7 +36,7 @@ Lemma newcounter_spec (R : iProp Σ) Φ :
heapN N
heap_ctx ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
iVs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
as (γ) "[#? Hγ]"; try by auto.
iVsIntro. iApply "HΦ". rewrite /counter; eauto 10.
......@@ -74,7 +74,7 @@ Lemma read_spec l j (Φ : val → iProp Σ) :
WP read #l {{ Φ }}.
Proof.
iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)".
rewrite /read. wp_let.
rewrite /read /=. wp_let.
iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
wp_load.
iVs ("Hclose" $! (j `max` j') with "[Hl]") as "Hγf".
......
......@@ -35,7 +35,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
recv N l (barrier_res γ Φ) ( x, {{ Φ x }} e {{ _, Ψ x }})
WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof.
iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
iIntros "[Hl #He]". wp_apply wait_spec; simpl; iFrame "Hl".
iDestruct 1 as (x) "[#Hγ Hx]".
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
iIntros (v) "?"; iExists x; by iSplit.
......
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