Commit 6d038c53 authored by Robbert Krebbers's avatar Robbert Krebbers

Use simpl to get rid of some %V scopes delimiters go away.

NB: these scopes delimiters were already there before Janno's a0067662.
parent ce5f7710
Pipeline #2646 passed with stage
in 9 minutes and 1 second
...@@ -96,7 +96,7 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) : ...@@ -96,7 +96,7 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
heap_ctx ( l, recv l P send l P - Φ #l) WP newbarrier #() {{ Φ }}. heap_ctx ( l, recv l P send l P - Φ #l) WP newbarrier #() {{ Φ }}.
Proof. Proof.
iIntros (HN) "[#? HΦ]". iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl". rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with "==>[-]"). iApply ("HΦ" with "==>[-]").
iVs (saved_prop_alloc (F:=idCF) P) as (γ) "#?". iVs (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iVs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]") iVs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
...@@ -120,7 +120,7 @@ Qed. ...@@ -120,7 +120,7 @@ Qed.
Lemma signal_spec l P (Φ : val iProp Σ) : Lemma signal_spec l P (Φ : val iProp Σ) :
send l P P Φ #() WP signal #l {{ Φ }}. send l P P Φ #() WP signal #l {{ Φ }}.
Proof. Proof.
rewrite /signal /send /barrier_ctx. rewrite /signal /send /barrier_ctx /=.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let. iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
......
...@@ -50,7 +50,7 @@ Lemma newlock_spec (R : iProp Σ) Φ : ...@@ -50,7 +50,7 @@ Lemma newlock_spec (R : iProp Σ) Φ :
heapN N heapN N
heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}. heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}.
Proof. Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock. iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
wp_seq. wp_alloc l as "Hl". wp_seq. wp_alloc l as "Hl".
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?". iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
...@@ -75,7 +75,7 @@ Lemma release_spec R l (Φ : val → iProp Σ) : ...@@ -75,7 +75,7 @@ Lemma release_spec R l (Φ : val → iProp Σ) :
locked l R R Φ #() WP release #l {{ Φ }}. locked l R R Φ #() WP release #l {{ Φ }}.
Proof. Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)". iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)".
rewrite /release. wp_let. iInv N as (b) "[Hl _]" "Hclose". rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame. wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed. Qed.
End proof. End proof.
...@@ -52,13 +52,13 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) : ...@@ -52,13 +52,13 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l) heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}. WP spawn e {{ Φ }}.
Proof. Proof.
iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn. iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn /=.
(* TODO: Coq is printing %V here. *) (* TODO: Coq is printing %V here. *)
wp_let. wp_alloc l as "Hl". wp_let. wp_let. wp_alloc l as "Hl". wp_let.
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. } { iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf". wp_apply wp_fork; simpl. iSplitR "Hf".
- iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto. - iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv". - wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose". iInv N as (v') "[Hl _]" "Hclose".
......
...@@ -78,7 +78,7 @@ Proof. apply _. Qed. ...@@ -78,7 +78,7 @@ Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ) Φ : Lemma newlock_spec (R : iProp Σ) Φ :
heap_ctx R ( l, is_lock l R - Φ l) WP newlock #() {{ Φ }}. heap_ctx R ( l, is_lock l R - Φ l) WP newlock #() {{ Φ }}.
Proof. Proof.
iIntros "(#Hh & HR & HΦ)". rewrite /newlock. iIntros "(#Hh & HR & HΦ)". rewrite /newlock /=.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln". wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done. iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
iVs (own_alloc_strong (Auth (Excl' ) ) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done. iVs (own_alloc_strong (Auth (Excl' ) ) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
......
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