Commit 4e2dfc4e authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of overlapping notations for Par.

Par is now defined as an expression of type [∀ X, expr X] (instead of a
value) and we prove that it is stable under weakening and substitution.
parent 5e2e8693
Pipeline #496 failed with stage
......@@ -4,12 +4,12 @@ From iris.heap_lang Require Import wp_tactics substitution notation.
Definition Assert {X} (e : expr X) : expr X :=
if: e then #() else #0 #0. (* #0 #0 is unsafe *)
Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
WExpr H e er WExpr H (Assert e) (Assert er) := _.
Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
WSubst x es H e er WSubst x es H (Assert e) (Assert er) | 1.
WSubst x es H e er WSubst x es H (Assert e) (Assert er).
Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
WExpr H e er WExpr H (Assert e) (Assert er) | 1.
Proof. intros; red. by rewrite /Assert /wexpr -/wexpr; f_equal/=. Qed.
Typeclasses Opaque Assert.
Lemma wp_assert {Σ} (Φ : val iProp heap_lang Σ) :
Φ #() WP Assert #true {{ Φ }}.
......
......@@ -2,18 +2,20 @@ From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
Definition par : val :=
Definition par {X} : expr X :=
λ: "fs",
let: "handle" := ^spawn (Fst '"fs") in
let: "v2" := Snd '"fs" #() in
let: "v1" := ^join '"handle" in
Pair '"v1" '"v2".
Notation Par e1 e2 := (^par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Notation ParV e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
(* We want both par and par^ to print like this. *)
Infix "||" := ParV : expr_scope.
Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Infix "||" := Par : expr_scope.
Instance do_wexpr_assert {X Y} (H : X `included` Y) : WExpr H par par := _.
Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) :
WSubst x es H par par := do_wsubst_closed _ x es H _.
Typeclasses Opaque par.
Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
Context (heapN N : namespace).
......@@ -25,19 +27,19 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP par e {{ Φ }}.
Proof.
iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". wp_value. wp_let. wp_proj.
iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". rewrite /par. wp_value. wp_let. wp_proj.
wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
iSpecialize "HΦ" "-"; first by iSplitL "H1". wp_let. by iPvsIntro.
iSpecialize "HΦ" "-"; first by iSplitL "H1". by wp_let.
Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) :
heapN N
(heap_ctx heapN WP e1 {{ Ψ1 }} WP e2 {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP ParV e1 e2 {{ Φ }}.
WP e1 || e2 {{ Φ }}.
Proof.
iIntros {?} "(#Hh&H1&H2&H)". iApply par_spec; auto.
iFrame "Hh H". iSplitL "H1"; by wp_let.
......
......@@ -85,6 +85,13 @@ Class WSubst {X Y} (x : string) (es : expr []) H (e : expr X) (er : expr Y) :=
do_wsubst : wsubst x es H e = er.
Hint Mode WSubst + + + + + + - : typeclass_instances.
Lemma do_wsubst_closed (e: {X}, expr X) {X Y} x es (H : X `included` x :: Y) :
( X, WExpr (included_nil X) e e) WSubst x es H e e.
Proof.
rewrite /WSubst /WExpr=> He. rewrite -(He X) wsubst_wexpr'.
by rewrite (wsubst_closed _ _ _ _ _ (included_nil _)); last set_solver.
Qed.
(* Variables *)
Lemma do_wsubst_var_eq {X Y x es} {H : X `included` x :: Y} `{VarBound x X} er :
WExpr (included_nil _) es er WSubst x es H (Var x) er.
......
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