par.v 1.74 KB
Newer Older
1 2
From iris.heap_lang Require Export heap spawn.
From iris.heap_lang Require Import wp_tactics notation.
Ralf Jung's avatar
Ralf Jung committed
3
Import uPred.
4 5

Definition par : val :=
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 12
Notation Par e1 e2 := (^par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Notation ParV e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
13 14
(* We want both par and par^ to print like this. *)
Infix "||" := ParV : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
15
Infix "||" := Par : expr_scope.
16 17

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

22
Lemma par_spec (Ψ1 Ψ2 : val  iProp) e (f1 f2 : val) (Φ : val  iProp) :
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  heapN  N  to_val e = Some (f1,f2)%V 
24
  (heap_ctx heapN  WP f1 #() {{ Ψ1 }}  WP f2 #() {{ Ψ2 }} 
25
    v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V)
26
   WP par e {{ Φ }}.
27
Proof.
28 29 30 31
  intros. rewrite /par. ewp (by eapply wp_value). wp_let. wp_proj.
  ewp (eapply spawn_spec; wp_done).
  apply sep_mono_r, sep_mono_r.
  apply forall_intro=>h. apply wand_intro_l. wp_let. wp_proj.
32
  wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let.
33 34
  ewp (by eapply join_spec).
  apply sep_mono_r, forall_intro=>v1; apply wand_intro_l.
35
  rewrite (forall_elim v1) (forall_elim v2). rewrite assoc wand_elim_r.
36
  wp_let. apply wp_value; wp_done.
Ralf Jung's avatar
Ralf Jung committed
37
Qed.
38

Ralf Jung's avatar
Ralf Jung committed
39 40
Lemma wp_par (Ψ1 Ψ2 : val  iProp) (e1 e2 : expr []) (Φ : val  iProp) :
  heapN  N 
41
  (heap_ctx heapN  WP e1 {{ Ψ1 }}  WP e2 {{ Ψ2 }} 
42
    v1 v2, Ψ1 v1  Ψ2 v2 -  Φ (v1,v2)%V)
43
   WP ParV e1 e2 {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
44
Proof.
45
  intros. rewrite -par_spec //. repeat apply sep_mono; done || by wp_seq.
Ralf Jung's avatar
Ralf Jung committed
46 47
Qed.
End proof.