curried Texan triples

base_logic/derived.v

@@ -352,14 +352,8 @@ Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q.
 Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
 Lemma wand_elim_r' P Q R : (Q ⊢ P -★ R) → P ★ Q ⊢ R.
 Proof. intros ->; apply wand_elim_r. Qed.
-Lemma wand_apply_l P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> <-; apply wand_elim_r. Qed.
+Lemma wand_apply P Q R S : (P ⊢ Q -★ R) → (S ⊢ P ★ Q) → S ⊢ R.
+Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
 Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
 Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
 Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.

heap_lang/heap.v

@@ -124,10 +124,10 @@ Section heap.
     to_val e = Some v → nclose heapN ⊆ E →
     {{{ heap_ctx }}} Alloc e @ E {{{ l; LitV (LitLoc l), l ↦ v }}}.
   Proof.
-    iIntros (<-%of_to_val ? Φ) "[#Hinv HΦ]". rewrite /heap_ctx.
+    iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
     iMod (auth_empty heap_name) as "Ha".
     iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ]".
+    iApply (wp_alloc_pst with "Hσ"). iNext. iIntros (l) "[% Hσ]".
     iMod ("Hcl" with "* [Hσ]") as "Ha".
     { iFrame. iPureIntro. rewrite to_heap_insert.
       eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
@@ -139,11 +139,11 @@ Section heap.
     {{{ heap_ctx ★ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E
     {{{; v, l ↦{q} v }}}.
   Proof.
-    iIntros (? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ".
+    iApply (wp_load_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
+    iNext; iIntros "Hσ".
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
@@ -152,11 +152,11 @@ Section heap.
     {{{ heap_ctx ★ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E
     {{{; LitV LitUnit, l ↦ v }}}.
   Proof.
-    iIntros (<-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
+    iApply (wp_store_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
+    iNext; iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
     { iFrame. iPureIntro. rewrite to_heap_insert.
       eapply singleton_local_update, exclusive_local_update; last done.
       by eapply heap_singleton_included'. }
@@ -168,11 +168,11 @@ Section heap.
     {{{ heap_ctx ★ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
     {{{; LitV (LitBool false), l ↦{q} v' }}}.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ".
+    iApply (wp_cas_fail_pst _ σ with "Hσ"); [eauto using heap_singleton_included|done|].
+    iNext; iIntros "Hσ".
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
@@ -181,11 +181,11 @@ Section heap.
     {{{ heap_ctx ★ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
     {{{; LitV (LitBool true), l ↦ v2 }}}.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_cas_suc_pst _ σ); first by eauto using heap_singleton_included.
-    iIntros "{$Hσ}". iNext. iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
+    iApply (wp_cas_suc_pst _ σ with "Hσ"); first by eauto using heap_singleton_included.
+    iNext. iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
     { iFrame. iPureIntro. rewrite to_heap_insert.
       eapply singleton_local_update, exclusive_local_update; last done.
       by eapply heap_singleton_included'. }

heap_lang/lib/barrier/proof.v

@@ -94,7 +94,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
   heapN ⊥ N →
   {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P ★ send l P }}}.
 Proof.
-  iIntros (HN Φ) "[#? HΦ]".
+  iIntros (HN Φ) "#? HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
@@ -120,7 +120,7 @@ Lemma signal_spec l P :
   {{{ send l P ★ P }}} signal #l {{{; #(), True }}}.
 Proof.
   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.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   destruct p; [|done]. wp_store.
@@ -136,7 +136,7 @@ Lemma wait_spec l P:
   {{{ recv l P }}} wait #l {{{ ; #(), P }}}.
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
-  iIntros (Φ) "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.

heap_lang/lib/barrier/specification.v

@@ -20,10 +20,10 @@ Proof.
   intros HN.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); first done.
-    iSplit; first done. iNext. eauto.
-  - iIntros (l P) "!# [Hl HP]". iApply signal_spec; iFrame "Hl HP"; by eauto.
-  - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
+  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
+    iNext. eauto.
+  - iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
+  - iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
   - iIntros (l P Q) "!#". by iApply recv_split.
   - apply recv_weaken.
 Qed.

heap_lang/lib/counter.v

@@ -37,7 +37,7 @@ Section mono_proof.
     heapN ⊥ N →
     {{{ heap_ctx }}} newcounter #() {{{ l; #l, mcounter l 0 }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HΦ]". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -47,7 +47,7 @@ Section mono_proof.
   Lemma inc_mono_spec l n :
     {{{ mcounter l n }}} inc #l {{{; #(), mcounter l (S n) }}}.
   Proof.
-    iIntros (Φ) "[Hl HΦ]". iLöb as "IH". wp_rec.
+    iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
     iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
@@ -72,7 +72,7 @@ Section mono_proof.
   Lemma read_mono_spec l j :
     {{{ mcounter l j }}} read #l {{{ i; #i, ■ (j ≤ i)%nat ∧ mcounter l i }}}.
   Proof.
-    iIntros (ϕ) "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
+    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "[$Hγ $Hγf]")
       as %[?%mnat_included _]%auth_valid_discrete_2.
@@ -114,7 +114,7 @@ Section contrib_spec.
     {{{ heap_ctx }}} newcounter #()
     {{{ γ l; #l, ccounter_ctx γ l ★ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HΦ]". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat))))
       as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
@@ -126,7 +126,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ★ ccounter γ q n }}} inc #l
     {{{; #(), ccounter γ q (S n) }}}.
   Proof.
-    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)". iLöb as "IH". wp_rec.
+    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     iModIntro. wp_let. wp_op.
@@ -147,7 +147,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ★ ccounter γ q n }}} read #l
     {{{ c; #c, ■ (n ≤ c)%nat ∧ ccounter γ q n }}}.
   Proof.
-    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
+    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "[$Hγ $Hγf]")
       as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
@@ -159,7 +159,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ★ ccounter γ 1 n }}} read #l
     {{{ n; #n, ccounter γ 1 n }}}.
   Proof.
-    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
+    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
     apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.

heap_lang/lib/par.v

@@ -24,10 +24,10 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
 Proof.
   iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
   rewrite /par. wp_value. wp_let. wp_proj.
-  wp_apply (spawn_spec parN with "[- $Hh $Hf1]"); try wp_done; try solve_ndisj.
+  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.
-  wp_apply (join_spec with "[- $Hl]"). iIntros (w) "H1".
+  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
 

heap_lang/lib/spawn.v

@@ -51,7 +51,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   heapN ⊥ N →
   {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l; #l, join_handle l Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) "((#Hh & Hf) & HΦ)". rewrite /spawn /=.
+  iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
@@ -66,14 +66,14 @@ Qed.
 Lemma join_spec (Ψ : val → iProp Σ) l :
   {{{ join_handle l Ψ }}} join #l {{{ v; v, Ψ v }}}.
 Proof.
-  rewrite /join_handle; iIntros (Φ) "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+  rewrite /join_handle; iIntros (Φ) "[% H] HΦ". iDestruct "H" as (γ) "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
-    iModIntro. wp_match. iApply ("IH" with "Hγ [Hv]"). auto.
+    iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
   - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
     + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
-      iModIntro. wp_match. by iApply "Hv".
+      iModIntro. wp_match. by iApply "HΦ".
     + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
 Qed.
 End proof.

heap_lang/lib/spin_lock.v

@@ -49,7 +49,7 @@ Section proof.
     heapN ⊥ N →
     {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
   Proof.
-    iIntros (? Φ) "[[#Hh HR] HΦ]". rewrite -wp_fupd /newlock /=.
+    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
@@ -61,7 +61,7 @@ Section proof.
     {{{ is_lock γ lk R }}} try_acquire lk
     {{{b; #b, if b is true then locked γ ★ R else True }}}.
   Proof.
-    iIntros (Φ) "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
+    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
     wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
     - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
       iModIntro. iApply ("HΦ" $! false). done.
@@ -73,8 +73,8 @@ Section proof.
   Lemma acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
   Proof.
-    iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "[- $Hl]"). iIntros ([]).
+    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
     - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
     - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
@@ -82,7 +82,7 @@ Section proof.
   Lemma release_spec γ lk R :
     {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}.
   Proof.
-    iIntros (Φ) "((Hlock & Hlocked & HR) & HΦ)".
+    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
     iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.

heap_lang/lib/ticket_lock.v

@@ -78,7 +78,7 @@ Section proof.
     heapN ⊥ N →
     {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
   Proof.
-    iIntros (HN Φ) "((#Hh & HR) & HΦ)". rewrite -wp_fupd /newlock /=.
+    iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
     iMod (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
@@ -91,7 +91,7 @@ Section proof.
   Lemma wait_loop_spec γ lk x R :
     {{{ issued γ lk x R }}} wait_loop #x lk {{{; #(), locked γ ★ R }}}.
   Proof.
-    iIntros (Φ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
+    iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
     iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -112,7 +112,7 @@ Section proof.
   Lemma acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
   Proof.
-    iIntros (ϕ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
+    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
@@ -131,8 +131,9 @@ Section proof.
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       iModIntro. wp_if.
-      iApply (wait_loop_spec γ (#lo, #ln)).
-      iFrame "HΦ". rewrite /issued; eauto 10.
+      iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+      + rewrite /issued; eauto 10.
+      + by iNext. 
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }
@@ -142,7 +143,7 @@ Section proof.
   Lemma release_spec γ lk R :
     {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}.
   Proof.
-    iIntros (Φ) "((Hl & Hγ & HR) & HΦ)".
+    iIntros (Φ) "(Hl & Hγ & HR) HΦ".
     iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
     iDestruct "Hγ" as (o) "Hγo".
     rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.

heap_lang/lifting.v

@@ -50,7 +50,7 @@ Lemma wp_alloc_pst E σ v :
   {{{ ▷ ownP σ }}} Alloc (of_val v) @ E
   {{{ l; LitV (LitLoc l), σ !! l = None ∧ ownP (<[l:=v]>σ) }}}.
 Proof.
-  iIntros (Φ) "[HP HΦ]".
+  iIntros (Φ) "HP HΦ".
   iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
@@ -61,7 +61,7 @@ Lemma wp_load_pst E σ l v :
   σ !! l = Some v →
   {{{ ▷ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{; v, ownP σ }}}.
 Proof.
-  intros ? Φ. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto.
+  intros ? Φ. apply (wp_lift_atomic_det_head_step' σ v σ); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -70,7 +70,7 @@ Lemma wp_store_pst E σ l v v' :
   {{{ ▷ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
   {{{; LitV LitUnit, ownP (<[l:=v]>σ) }}}.
 Proof.
-  intros. rewrite-(wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
+  intros. apply (wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -79,7 +79,7 @@ Lemma wp_cas_fail_pst E σ l v1 v2 v' :
   {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
   {{{; LitV $ LitBool false, ownP σ }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
+  intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -88,7 +88,7 @@ Lemma wp_cas_suc_pst E σ l v1 v2 :
   {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
   {{{; LitV $ LitBool true, ownP (<[l:=v2]>σ) }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
+  intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
     (<[l:=v2]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.

heap_lang/proofmode.v

@@ -25,7 +25,7 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
     (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
+  intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
@@ -39,7 +39,7 @@ Lemma tac_wp_load Δ Δ' E i l q v Φ :
   (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_load // -assoc -always_and_sep_l.
+  intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
@@ -54,7 +54,7 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   (Δ'' ⊢ Φ (LitV LitUnit)) →
   Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_store // -assoc -always_and_sep_l.
+  intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
@@ -68,7 +68,7 @@ Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_cas_fail // -assoc -always_and_sep_l.
+  intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
@@ -83,7 +83,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   (Δ'' ⊢ Φ (LitV (LitBool true))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros; subst. rewrite -wp_cas_suc // -assoc -always_and_sep_l.
+  intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.

program_logic/ectx_lifting.v

@@ -60,15 +60,15 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
-Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
+Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
   atomic e1 →
   head_reducible e1 σ1 →
   (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2) ⊢ WP e1 @ E {{ Φ }}.
+  {{{ ▷ ownP σ1 }}} e1 @ E {{{; v2, ownP σ2 }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
-    ?big_sepL_nil ?right_id; eauto.
+  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
+  rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :

program_logic/weakestpre.v

@@ -70,39 +70,39 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
 (* Texan triples *)
 Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
   (□ ∀ Φ,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
+      P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
   (□ ∀ Φ,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
+      P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  @  E  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
-  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
+  (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
     (at level 20,
      format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
-  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
+  (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
     (at level 20,
      format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : uPred_scope.
 
 Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e {{ Φ }})
+      P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e @ E {{ Φ }})
+      P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  @  E  {{{ x .. y ;  pat ,  Q } } }") : C_scope.
 Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
-  (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e {{ Φ }})
+  (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
-  (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e @ E {{ Φ }})
+  (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : C_scope.
 

tests/barrier_client.v

@@ -37,11 +37,12 @@ Section client.
   Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
   Proof.
     iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
-    wp_apply (newbarrier_spec N (y_inv 1 y) with "[- $Hh]"); first done.
+    wp_apply (newbarrier_spec N (y_inv 1 y) with "Hh"); first done.
     iIntros (l) "[Hr Hs]". wp_let.
     iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. iApply (signal_spec with "[- $Hs]"). iSplitL "Hy"; [|by eauto].
+      wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
+      iSplitR "Hy"; first by eauto.
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros (_ _) "_ !>"].

tests/joining_existentials.v

@@ -76,7 +76,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
 Proof.
   iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
-  wp_apply (newbarrier_spec N (barrier_res γ Φ) with "[- $Hh]"); auto.
+  wp_apply (newbarrier_spec N (barrier_res γ Φ) with "Hh"); auto.
   iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
   wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[- $Hh]").
@@ -85,7 +85,7 @@ Proof.
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
     iMod (own_update with "Hγ") as "Hx".
     { by apply (cmra_update_exclusive (Shot x)). }
-    iApply (signal_spec with "[- $Hs]"). iSplitR ""; last auto.
+    iApply (signal_spec with "[- $Hs]"); last auto.
     iExists x; auto.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
     iMod (recv_split with "Hr") as "[H1 H2]"; first done.