par.v 1.76 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.
3
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
4
Import uPred.
5

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

8
Definition par : val :=
9 10 11
  λ: "e1" "e2",
    let: "handle" := spawn "e1" in
    let: "v2" := "e2" #() in
12
    let: "v1" := join "handle" in
13
    ("v1", "v2").
14
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
15 16
(* Not a value itself, but with *unlocked* value lambdas. *)
Local Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
17

18
Section proof.
19
Local Set Default Proof Using "Type*".
20
Context `{!heapG Σ, !spawnG Σ}.
21

22 23 24 25
(* 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. *)
26
Lemma par_spec (Ψ1 Ψ2 : val  iProp Σ) (f1 f2 : val) (Φ : val  iProp Σ) :
27 28
  WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
  (  v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V) -
29
  WP par f1 f2 {{ Φ }}.
30
Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
31
  iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
32
  wp_apply (spawn_spec parN with "Hf1").
33 34
  iIntros (l) "Hl". wp_let. wp_bind (f2 _).
  wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
Ralf Jung's avatar
Ralf Jung committed
35
  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
36
  iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
Ralf Jung's avatar
Ralf Jung committed
37
Qed.
38

39
Lemma wp_par (Ψ1 Ψ2 : val  iProp Σ) (e1 e2 : expr) (Φ : val  iProp Σ) :
40 41
  WP e1 {{ Ψ1 }} - WP e2 {{ Ψ2 }} -
  ( v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V) -
Ralf Jung's avatar
Ralf Jung committed
42
  WP (e1 ||| e2)%V {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
43
Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
44 45
  iIntros "H1 H2 H".
  wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
Ralf Jung's avatar
Ralf Jung committed
46 47
Qed.
End proof.