diff --git a/theories/examples/par.v b/theories/examples/par.v
index 422a87cc1b40f679b3c60f84e75cc4108e4f022c..8083c39578b1fffceb7aa235ae7fe0f982528142 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -16,117 +16,216 @@ Axioms/rules for parallel composition
also requires unfolding
*)
+Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()));; #())%E
+ (at level 60) : expr_scope.
+(* Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()))%V;; #()) *)
+(* (at level 60) : val_scope. *)
+
+
Section rules.
Context `{!relocG Σ, !spawnG Σ}.
- Lemma par_r_1 e1 e2 t (A : lrel Σ) E :
- ↑ relocN ⊆ E →
- is_closed_expr [] e1 →
- (∀ i C, i ⤇ fill C e1 ={E}=∗ ∃ (v : val),
- i ⤇ fill C v ∗ REL t << (v, e2) @ E : A) -∗
- REL t << (e1 ||| e2)%V @ E : A.
+ Lemma par_l_2 e1 e2 t :
+ (WP e1 {{ _, True }}) -∗
+ (REL e2 << t : ()) -∗
+ REL (e1 ∥ e2) << t : ().
Proof.
- iIntros (??) "H".
- rel_rec_r. repeat rel_pure_r.
- rel_rec_r.
- repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
- repeat rel_pure_r. rel_fork_r i as "Hi".
- { simpl. eauto. }
- repeat rel_pure_r.
- tp_pure i _. tp_bind i e1.
- iMod ("H" with "Hi") as (v1) "[Hi H]".
- iSimpl in "Hi". tp_pure i _. tp_store i.
- Abort.
- (* rewrite refines_eq /refines_def. *)
- (* iIntros (Ï') "_". clear Ï'. *)
- (* iIntros (j K) "Hj". *)
- (* tp_bind j e2. *)
+ iIntros "He1 He2".
+ rel_pures_l. rel_rec_l.
+ rel_pures_l. rel_bind_l (spawn _).
+ iApply refines_wp_l.
+ pose (N:=nroot.@"par").
+ iApply (spawn_spec N (λ _, True)%I with "[He1]").
+ - wp_pures. wp_bind e1. iApply (wp_wand with "He1").
+ iIntros (?) "_"; by wp_pures.
+ - iNext. iIntros (l) "hndl". iSimpl.
+ rel_pures_l. rel_bind_l e2. rel_bind_r t.
+ iApply (refines_bind with "He2").
+ iIntros (? ?) "[% %]"; simplify_eq/=.
+ rel_pures_l.
+ rel_bind_l (spawn.join _).
+ iApply refines_wp_l.
+ iApply (join_spec with "hndl").
+ iNext. iIntros (?) "_". simpl.
+ rel_pures_l. by rel_values.
+ Qed.
- (* this one we can prove without unfolding *)
- Lemma par_unit_1 e A :
- (REL e << e : A) -∗
- REL (#() ||| e) << e : lrel_true.
+ Lemma par_l_2' Q K e1 e2 t :
+ (WP e1 {{ _, Q }}) -∗
+ (REL e2 << t : ()) -∗
+ (Q -∗ REL #() << fill K (#() : expr) : ()) -∗
+ REL (e1 ∥ e2) << fill K t : ().
Proof.
- iIntros "He".
- rel_pures_l. rel_rec_l. rel_pures_l.
- rel_bind_l (spawn _).
+ iIntros "He1 He2 Ht".
+ rel_pures_l. rel_rec_l.
+ rel_pures_l. rel_bind_l (spawn _).
iApply refines_wp_l.
pose (N:=nroot.@"par").
- iApply (spawn_spec N (λ v, True)%I).
- - by wp_pures.
+ iApply (spawn_spec N (λ _, Q)%I with "[He1]").
+ - wp_pures. wp_bind e1. iApply (wp_wand with "He1").
+ iIntros (?) "HQ"; by wp_pures.
- iNext. iIntros (l) "hndl". iSimpl.
- rel_pures_l. rel_bind_l e. rel_bind_r e.
- iApply (refines_bind with "He").
- iIntros (v v') "Hv". simpl.
+ rel_pures_l. rel_bind_l e2.
+ iApply (refines_bind with "He2").
+ iIntros (? ?) "[% %]"; simplify_eq/=.
rel_pures_l.
rel_bind_l (spawn.join _).
iApply refines_wp_l.
iApply (join_spec with "hndl").
- iNext. iIntros (?) "_". simpl.
- rel_pures_l. rel_values.
+ iNext. iIntros (?) "HQ". simpl.
+ rel_pures_l. by iApply "Ht".
+ Qed.
+
+ Lemma par_l_1 e1 e2 t :
+ (REL e1 << t : ()) -∗
+ (WP e2 {{ _, True }}) -∗
+ REL (e1 ∥ e2) << t : ().
+ Proof.
+ iIntros "He1 He2".
+ rel_pures_l. rel_rec_l.
+ rel_pures_l.
+ pose (N:=nroot.@"par").
+ rewrite refines_eq /refines_def. iIntros (j K) "#Hspec Hj".
+ iModIntro. wp_bind (spawn _).
+ iApply (spawn_spec N (λ _, j ⤇ fill K #())%I with "[He1 Hj]").
+ - wp_pures. wp_bind e1.
+ iMod ("He1" with "Hspec Hj") as "He1".
+ iApply (wp_wand with "He1").
+ iIntros (?) "P". wp_pures.
+ by iDestruct "P" as (v') "[Hj [-> ->]]".
+ - iNext. iIntros (l) "hndl". iSimpl.
+ wp_pures. wp_bind e2.
+ iApply (wp_wand with "He2"). iIntros (?) "_".
+ wp_pures.
+ wp_apply (join_spec with "hndl").
+ iIntros (?) "Hj". wp_pures. iExists #(). eauto with iFrame.
+ Qed.
+
+ Lemma par_l_1' Q K e1 e2 t :
+ (REL e1 << t : ()) -∗
+ (WP e2 {{ _, Q }}) -∗
+ (Q -∗ REL #() << fill K (#() : expr) : ()) -∗
+ REL (e1 ∥ e2) << fill K t : ().
+ Proof.
+ iIntros "He1 He2 Ht".
+ rel_pures_l. rel_rec_l.
+ rel_pures_l.
+ pose (N:=nroot.@"par").
+ rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj".
+ iModIntro. wp_bind (spawn _).
+ iApply (spawn_spec N (λ _, j ⤇ fill (K++K') #())%I with "[He1 Hj]").
+ - wp_pures. wp_bind e1.
+ rewrite -fill_app.
+ iMod ("He1" with "Hspec Hj") as "He1".
+ iApply (wp_wand with "He1").
+ iIntros (?) "P". wp_pures.
+ by iDestruct "P" as (v') "[Hj [-> ->]]".
+ - iNext. iIntros (l) "hndl". iSimpl.
+ wp_pures. wp_bind e2.
+ iApply (wp_wand with "He2"). iIntros (?) "HQ".
+ wp_pures.
+ wp_apply (join_spec with "hndl").
+ iIntros (?) "Hj".
+ iSpecialize ("Ht" with "HQ").
+ rewrite refines_eq /refines_def.
+ rewrite fill_app.
+ iMod ("Ht" with "Hspec Hj") as "Ht".
+ rewrite wp_value_inv. iMod "Ht" as (?) "[Ht [_ ->]]".
+ wp_pures. iExists #(). eauto with iFrame.
+ Qed.
+
+ (* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *)
+ (* ↑ relocN ⊆ E → *)
+ (* is_closed_expr [] e1 → *)
+ (* (∀ i C, i ⤇ fill C e1 ={E}=∗ ∃ (v : val), *)
+ (* i ⤇ fill C v ∗ REL t << (v, e2) @ E : A) -∗ *)
+ (* REL t << (e1 ||| e2)%V @ E : A. *)
+ (* Proof. *)
+ (* iIntros (??) "H". *)
+ (* rel_rec_r. repeat rel_pure_r. *)
+ (* rel_rec_r. *)
+ (* repeat rel_pure_r. rel_alloc_r c2 as "Hc2". *)
+ (* repeat rel_pure_r. rel_fork_r i as "Hi". *)
+ (* { simpl. eauto. } *)
+ (* repeat rel_pure_r. *)
+ (* tp_rec i. simpl. *)
+ (* tp_bind i e1. *)
+ (* iMod ("H" with "Hi") as (v1) "[Hi H]". *)
+ (* iSimpl in "Hi". tp_pure i (InjR v1). tp_store i. *)
+ (* Abort. *)
+ (* (* rewrite refines_eq /refines_def. *) *)
+ (* (* iIntros (Ï') "_". clear Ï'. *) *)
+ (* (* iIntros (j K) "Hj". *) *)
+ (* (* tp_bind j e2. *) *)
+
+ (* this one we can prove without unfolding *)
+ Lemma par_unit_1 e :
+ (REL e << e : ()) -∗
+ REL (#() ∥ e) << e : ().
+ Proof.
+ iIntros "He".
+ iApply (par_l_2 with "[] He").
+ by iApply wp_value.
Qed.
- Lemma par_unit_2 e A :
- (REL e << e : A) -∗
- REL e << (#() ||| e) : lrel_true.
+ Lemma par_unit_2 e :
+ (REL e << e : ()) -∗
+ REL e << (#() ∥ e) : ().
Proof.
- iIntros "H".
+ iIntros "He".
rel_pures_r. rel_rec_r. rel_pures_r. rel_rec_r.
rel_pures_r. rel_alloc_r c2 as "Hc2".
rel_pures_r. rel_fork_r i as "Hi".
rel_pures_r.
tp_rec i. simpl.
- tp_pure i _. tp_store i.
+ tp_pures i. tp_store i.
rel_bind_l e. rel_bind_r e.
- iApply (refines_bind with "H").
- iIntros (v v') "Hv". simpl.
- rel_pures_r.
+ iApply (refines_bind with "He").
+ iIntros (v v') "[-> ->]".
+ simpl. rel_pures_r.
rel_rec_r. rel_load_r. rel_pures_r.
rel_values.
Qed.
- Lemma par_comm e1 e2 (A B : lrel Σ) :
+ (* This proof is now simpler but it still requires unfolding the REL judgement *)
+ Lemma par_comm e1 e2 :
is_closed_expr [] e1 →
is_closed_expr [] e2 →
- (REL e1 << e1 : A) -∗
- (REL e2 << e2 : B) -∗
- REL (e2 ||| e1)%V << (e1 ||| e2)%V : lrel_true.
+ (REL e1 << e1 : ()) -∗
+ (REL e2 << e2 : ()) -∗
+ REL (e2 ∥ e1) << (e1 ∥ e2) : ().
Proof.
- iIntros (??) "He1 He2". rel_rec_r. repeat rel_pure_r.
- rel_rec_r.
- repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
- repeat rel_pure_r. rel_fork_r i as "Hi".
+ iIntros (??) "He1 He2". rel_pures_r.
+ rel_rec_r. rel_pures_r. rel_rec_r.
+ rel_pures_r. rel_alloc_r c2 as "Hc2".
+ rel_pures_r. rel_fork_r i as "Hi".
{ simpl. eauto. }
- repeat rel_pure_r.
- tp_rec i. simpl.
- rel_rec_l. repeat rel_pure_l.
- rewrite {3}refines_eq /refines_def.
- iIntros (j K) "#Hs Hj". iModIntro.
- tp_bind j e2.
- pose (C:=(AppRCtx (λ: "v2", let: "v1" := spawn.join #c2 in ("v1", "v2")) :: K)).
- fold C.
- pose (N:=nroot.@"par").
- wp_bind (spawn _).
- iApply (spawn_spec N with "[He2 Hj]").
- - wp_lam. rewrite refines_eq /refines_def.
- iMod ("He2" with "Hs Hj") as "He2".
- iAssumption.
- - iNext. iIntros (l) "l_hndl".
- wp_pures. wp_bind e1.
- rewrite refines_eq /refines_def.
+ tp_pure i (App _ _). simpl.
+ rel_pures_r.
+ rel_bind_r e2.
+ iApply refines_spec_ctx. iIntros "#Hs".
+ iApply (par_l_1' (i ⤇ (#c2 <- InjR (#();; #())))%I
+ with "He2 [He1 Hi]").
+ { rewrite refines_eq /refines_def.
tp_bind i e1.
- iMod ("He1" with "Hs Hi") as "He1".
- iApply (wp_wand with "He1").
- iIntros (v1). iDestruct 1 as (v2) "[Hi Hv]".
- wp_pures. wp_bind (spawn.join _).
- iApply (join_spec with "l_hndl").
- iNext. iIntros (w1). iDestruct 1 as (w2) "[Hj Hw]".
- unfold C. iSimpl in "Hi". iSimpl in "Hj".
- tp_pures i. tp_store i.
- tp_pures j.
- tp_rec j.
- tp_pures j. iApply fupd_wp. tp_load j.
- tp_pures j.
- iModIntro. wp_pures. iExists (v2, w2)%V. eauto.
+ iMod ("He1" with "Hs Hi") as "He1". simpl.
+ iApply (wp_wand with "He1"). iIntros (?).
+ iDestruct 1 as (?) "[Hi [-> ->]]". done. }
+ iIntros "Hi". simpl. rel_pures_r.
+ tp_pures i. tp_store i.
+ rel_rec_r. rel_load_r. rel_pures_r. rel_values.
+ Qed.
+
+ Lemma par_bot_2 e1 :
+ ⊢ REL bot #() << e1 ∥ bot #() : ().
+ Proof. rel_apply_l bot_l. Qed.
+
+ Lemma par_bot_1 e1 :
+ (WP e1 {{_ , True}}) -∗ (* TODO: what can we do about this assignment? *)
+ REL (e1 ∥ bot #()) << bot #() : ().
+ Proof.
+ iIntros "He1".
+ iApply (par_l_2 with "He1").
+ rel_apply_l bot_l.
Qed.
Lemma seq_par e1 e2 (A B : lrel Σ) :
diff --git a/theories/typing/types.v b/theories/typing/types.v
index c57ddcaa636025af4f904590153f6318c1f4c3fa..66e640ed7684f839f66bfc656db33ad98f7107ba 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -233,6 +233,7 @@ Lemma binop_bool_typed_safe (op : bin_op) (b1 b2 : bool) Ï„ :
binop_bool_res_type op = Some τ → is_Some (bin_op_eval op #b1 #b2).
Proof. destruct op; naive_solver. Qed.
+
Lemma unop_nat_typed_safe (op : un_op) (n : Z) Ï„ :
unop_nat_res_type op = Some τ → is_Some (un_op_eval op #n).
Proof. destruct op; simpl; eauto. Qed.
@@ -240,3 +241,24 @@ Proof. destruct op; simpl; eauto. Qed.
Lemma unop_bool_typed_safe (op : un_op) (b : bool) Ï„ :
unop_bool_res_type op = Some τ → is_Some (un_op_eval op #b).
Proof. destruct op; naive_solver. Qed.
+
+(* From stdpp Require Import fin_map_dom. *)
+
+(* Lemma typed_is_closed Γ e τ : *)
+(* Γ ⊢ₜ e : τ → is_closed_expr (elements (dom stringset Γ)) e *)
+(* with typed_is_closed_val v Ï„ : *)
+(* ⊢ᵥ v : τ → is_closed_val v. *)
+(* Proof. *)
+(* - inversion 1; simpl; try naive_solver. *)
+(* + destruct f as [|f], x as [|x]; simpl; first naive_solver. *)
+(* * specialize (typed_is_closed (<[x:=τ1]>Γ) e0 τ2 H0). *)
+(* revert typed_is_closed. rewrite dom_insert_L. *)
+(* admit. *)
+(* * admit. *)
+(* * admit. *)
+(* + specialize (typed_is_closed (⤉Γ) e0 τ0 H0). *)
+(* revert typed_is_closed. by rewrite dom_fmap_L. *)
+(* + admit. *)
+(* - inversion 1; simpl; try naive_solver. *)
+(* Admitted. *)
+