Commit 75dd9e14 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/curry-fork' into 'master'

curry wp_fork

See merge request FP/iris-coq!180
parents f5109e7c 9d80e031
......@@ -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 :
......
......@@ -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.
......
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