Commit 0e48566f authored by Robbert Krebbers's avatar Robbert Krebbers

Notation for PairV.

parent bfdeefd3
Pipeline #261 passed with stage
...@@ -32,6 +32,7 @@ Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope. ...@@ -32,6 +32,7 @@ Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *) first. *)
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1 e1 x2 e2) (Match e0 x1 e1 x2 e2)
(e0, x1, e1, x2, e2 at level 200) : expr_scope. (e0, x1, e1, x2, e2 at level 200) : expr_scope.
......
...@@ -20,21 +20,21 @@ Context (heapN N : namespace). ...@@ -20,21 +20,21 @@ Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Lemma par_spec (Ψ1 Ψ2 : val iProp) e (f1 f2 : val) (Φ : val iProp) : Lemma par_spec (Ψ1 Ψ2 : val iProp) e (f1 f2 : val) (Φ : val iProp) :
heapN N to_val e = Some (PairV f1 f2) heapN N to_val e = Some (f1,f2)%V
(heap_ctx heapN #> f1 #() {{ Ψ1 }} #> f2 #() {{ Ψ2 }} (heap_ctx heapN #> f1 #() {{ Ψ1 }} #> f2 #() {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (PairV v1 v2)) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
#> par e {{ Φ }}. #> par e {{ Φ }}.
Proof. Proof.
intros. rewrite /par. intros. rewrite /par.
wp_focus e. etransitivity; last by eapply wp_value. wp_let. wp_focus e. etransitivity; last by eapply wp_value. wp_let.
(* FIXME: wp_proj should not spawn these goals. *) (* FIXME: wp_proj should not spawn these goals. *)
wp_proj; eauto using to_of_val. wp_proj; eauto using to_of_val.
(ewp eapply spawn_spec); eauto using to_of_val. ewp eapply spawn_spec; eauto using to_of_val.
apply sep_mono_r. apply sep_mono_r. apply sep_mono_r. apply sep_mono_r.
apply forall_intro=>h. apply wand_intro_l. wp_let. apply forall_intro=>h. apply wand_intro_l. wp_let.
wp_proj; eauto using to_of_val. wp_proj; eauto using to_of_val.
wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let. wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let.
(ewp eapply join_spec); eauto using to_of_val. apply sep_mono_r. ewp eapply join_spec; eauto using to_of_val. apply sep_mono_r.
apply forall_intro=>v1. apply wand_intro_l. wp_let. apply forall_intro=>v1. apply wand_intro_l. wp_let.
etransitivity; last by (eapply wp_value, to_val_Pair; eapply to_of_val). etransitivity; last by (eapply wp_value, to_val_Pair; eapply to_of_val).
rewrite (forall_elim v1) (forall_elim v2). rewrite assoc. rewrite (forall_elim v1) (forall_elim v2). rewrite assoc.
...@@ -44,7 +44,7 @@ Qed. ...@@ -44,7 +44,7 @@ Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) : Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) :
heapN N heapN N
(heap_ctx heapN #> e1 {{ Ψ1 }} #> e2 {{ Ψ2 }} (heap_ctx heapN #> e1 {{ Ψ1 }} #> e2 {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (PairV v1 v2)) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
#> ParV e1 e2 {{ Φ }}. #> ParV e1 e2 {{ Φ }}.
Proof. Proof.
intros. rewrite -par_spec //. apply sep_mono_r. intros. rewrite -par_spec //. apply sep_mono_r.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment