par.v 2.08 KB
Newer Older
1
2
From heap_lang Require Export heap spawn.
From heap_lang Require Import wp_tactics notation.
Ralf Jung's avatar
Ralf Jung committed
3
Import uPred.
4
5
6
7
8
9

Definition par : val :=
  λ: "f1" "f2", let: "handle" := ^spawn '"f1" in
                let: "v2" := '"f2" #() in
                let: "v1" := ^join '"handle" in
                Pair '"v1" '"v2".
Ralf Jung's avatar
Ralf Jung committed
10
Notation Par e1 e2 := (^par (λ: <>, e1) (λ: <>, e2))%E.
11
12
13
Notation ParV e1 e2 := (par (λ: <>, e1) (λ: <>, e2))%E.
(* We want both par and par^ to print like this. *)
Infix "||" := ParV : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
14
Infix "||" := Par : expr_scope.
15
16
17
18
19
20

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

Ralf Jung's avatar
Ralf Jung committed
21
22
23
24
Lemma par_spec (Ψ1 Ψ2 : val  iProp) e1 e2 (f1 f2 : val) (Φ : val  iProp) :
  heapN  N  to_val e1 = Some f1  to_val e2 = Some f2 
  (* TODO like in spawn.v -- wp about e or f? *)
  (heap_ctx heapN  #> e1 #() {{ Ψ1 }}  #> e2 #() {{ Ψ2 }} 
25
    v1 v2, Ψ1 v1  Ψ2 v2 - Φ (PairV v1 v2))
Ralf Jung's avatar
Ralf Jung committed
26
   #> par e1 e2 {{ Φ }}.
27
Proof.
Ralf Jung's avatar
Ralf Jung committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
  intros. rewrite /par.
  wp_focus e1. etransitivity; last by eapply wp_value. wp_let.
  wp_focus e2. etransitivity; last by eapply wp_value. wp_let.
  (ewp eapply spawn_spec); eauto using to_of_val.
  apply sep_mono_r. rewrite (of_to_val e1) //. apply sep_mono_r.
  apply forall_intro=>h. apply wand_intro_l. wp_let.
  wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. rewrite (of_to_val e2) //.
  apply wp_mono=>v2. wp_let.
  (ewp eapply join_spec); eauto using to_of_val. apply sep_mono_r.
  apply forall_intro=>v1. apply wand_intro_l. wp_let.
  etransitivity; last by (eapply wp_value, to_val_Pair; eapply to_of_val).
  rewrite (forall_elim v1) (forall_elim v2). rewrite assoc.
  eapply wand_apply_r'; done.
Qed.
42

Ralf Jung's avatar
Ralf Jung committed
43
44
45
46
Lemma wp_par (Ψ1 Ψ2 : val  iProp) (e1 e2 : expr []) (Φ : val  iProp) :
  heapN  N 
  (heap_ctx heapN  #> e1 {{ Ψ1 }}  #> e2 {{ Ψ2 }} 
    v1 v2, Ψ1 v1  Ψ2 v2 - Φ (PairV v1 v2))
47
   #> ParV e1 e2 {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
48
Proof.
49
  intros. rewrite -par_spec //. apply sep_mono_r.
Ralf Jung's avatar
Ralf Jung committed
50
51
52
53
  apply sep_mono; last apply sep_mono_l; by wp_seq.
Qed.

End proof.