par.v 1.52 KB
Newer Older
1
From iris.heap_lang Require Export spawn.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.heap_lang Require Import proofmode notation.
Ralf Jung's avatar
Ralf Jung committed
3
Import uPred.
4

5 6
Definition parN : namespace := nroot .@ "par".

7
Definition par : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  λ: "fs",
9 10 11
    let: "handle" := spawn (Fst "fs") in
    let: "v2" := Snd "fs" #() in
    let: "v1" := join "handle" in
12
    ("v1", "v2").
13
Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
14
Global Opaque par.
15

16
Section proof.
17
Context `{!heapG Σ, !spawnG Σ}.
18

19
Lemma par_spec (Ψ1 Ψ2 : val  iProp Σ) e (f1 f2 : val) (Φ : val  iProp Σ) :
20
  to_val e = Some (f1,f2)%V 
21
  (heap_ctx  WP f1 #() {{ Ψ1 }}  WP f2 #() {{ Ψ2 }} 
Ralf Jung's avatar
Ralf Jung committed
22
     v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V)
23
   WP par e {{ Φ }}.
24
Proof.
25
  iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
26
  rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
27
  wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
Ralf Jung's avatar
Ralf Jung committed
28
  iNext. iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
29
  iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
Ralf Jung's avatar
Ralf Jung committed
30
  wp_apply join_spec; iFrame "Hl". iNext. iIntros (w) "H1".
31
  iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Ralf Jung's avatar
Ralf Jung committed
32
Qed.
33

34 35
Lemma wp_par (Ψ1 Ψ2 : val  iProp Σ)
    (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val  iProp Σ) :
36
  (heap_ctx  WP e1 {{ Ψ1 }}  WP e2 {{ Ψ2 }} 
37
    v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V)
38
   WP e1 || e2 {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
39
Proof.
40
  iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  iFrame "Hh H". iSplitL "H1"; by wp_let.
Ralf Jung's avatar
Ralf Jung committed
42 43
Qed.
End proof.