par.v 1.73 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
Definition par {X} : expr X :=
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7
  λ: "fs",
    let: "handle" := ^spawn (Fst '"fs") in
8
    let: "v2" := Snd '"fs" #() in
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10
    let: "v1" := ^join '"handle" in
    Pair '"v1" '"v2".
11
Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Ralf Jung's avatar
Ralf Jung committed
12
Infix "||" := Par : expr_scope.
13

Ralf Jung's avatar
Ralf Jung committed
14 15
Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
16
  WSubst x es H par par := do_wsubst_closed _ x es H _.
17
Global Opaque par.
18

19
Section proof.
20
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
21 22 23
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

24
Lemma par_spec (Ψ1 Ψ2 : val  iProp) e (f1 f2 : val) (Φ : val  iProp) :
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  heapN  N  to_val e = Some (f1,f2)%V 
26
  (heap_ctx heapN  WP f1 #() {{ Ψ1 }}  WP f2 #() {{ Ψ2 }} 
27
    v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V)
28
   WP par e {{ Φ }}.
29
Proof.
30
  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". rewrite /par. wp_value. wp_let. wp_proj.
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32 33 34
  wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
  iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
  iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
  wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
35
  iSpecialize ("HΦ" with "* -"); first by iSplitL "H1". by wp_let.
Ralf Jung's avatar
Ralf Jung committed
36
Qed.
37

Ralf Jung's avatar
Ralf Jung committed
38 39
Lemma wp_par (Ψ1 Ψ2 : val  iProp) (e1 e2 : expr []) (Φ : val  iProp) :
  heapN  N 
40
  (heap_ctx heapN  WP e1 {{ Ψ1 }}  WP e2 {{ Ψ2 }} 
41
    v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V)
42
   WP e1 || e2 {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
43
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  iIntros {?} "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  iFrame "Hh H". iSplitL "H1"; by wp_let.
Ralf Jung's avatar
Ralf Jung committed
46 47
Qed.
End proof.