curry wp_fork

theories/heap_lang/lib/spawn.v

@@ -53,11 +53,11 @@ Proof.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { 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 with "Hf"); iIntros (v) "Hv".
+  wp_apply (wp_fork with "[Hf]").
+  - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
     iInv N as (v') "[Hl _]".
     wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
+  - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp Σ) l :

theories/heap_lang/lifting.v

@@ -104,18 +104,18 @@ Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
 Implicit Types σ : state.
 
-(** Base axioms for core primitives of the language: Stateless reductions *)
+(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
 Lemma wp_fork s E e Φ :
-  ▷ (Φ (LitV LitUnit) ∗ WP e @ s; ⊤ {{ _, True }}) ⊢ WP Fork e @ s; E {{ Φ }}.
+  ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
-  iIntros "[HΦ He]".
+  iIntros "He HΦ".
   iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
   iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
 Qed.
 Lemma twp_fork s E e Φ :
-  Φ (LitV LitUnit) ∗ WP e @ s; ⊤ [{ _, True }] ⊢ WP Fork e @ s; E [{ Φ }].
+  WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
-  iIntros "[HΦ He]".
+  iIntros "He HΦ".
   iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
   iIntros "!> /= {$He}". by iApply twp_value.
 Qed.