par.v 1.72 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 :=
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

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

18 19 20 21
(* Notice that this allows us to strip a later *after* the two Ψ have been
   brought together.  That is strictly stronger than first stripping a later
   and then merging them, as demonstrated by [tests/joining_existentials.v].
   This is why these are not Texan triples. *)
22
Lemma par_spec (Ψ1 Ψ2 : val  iProp Σ) e (f1 f2 : val) (Φ : val  iProp Σ) :
23
  to_val e = Some (f1,f2)%V 
24 25 26
  WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
  (  v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V) -
  WP par e {{ Φ }}.
27
Proof.
28
  iIntros (?) "Hf1 Hf2 HΦ".
29
  rewrite /par. wp_value. wp_let. wp_proj.
30
  wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
31
  iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
Ralf Jung's avatar
Ralf Jung committed
33
  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
34
  iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Ralf Jung's avatar
Ralf Jung committed
35
Qed.
36

37 38
Lemma wp_par (Ψ1 Ψ2 : val  iProp Σ)
    (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val  iProp Σ) :
39 40 41
  WP e1 {{ Ψ1 }} - WP e2 {{ Ψ2 }} -
  ( v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V) -
  WP e1 ||| e2 {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
42
Proof.
43 44
  iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); try wp_done.
  by wp_let. by wp_let. auto.
Ralf Jung's avatar
Ralf Jung committed
45 46
Qed.
End proof.