Commit b90854c7 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize wp_fork to have an arbitrary post-condition.

parent ae64fb70
......@@ -30,7 +30,7 @@ Proof.
by rewrite -wp_let' //= ?to_of_val ?subst_empty.
Qed.
Lemma wp_skip E Q : (Q (LitV LitUnit)) wp E Skip Q.
Lemma wp_skip E Q : (Q (LitV LitUnit)) wp E Skip Q.
Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.
Lemma wp_le E (n1 n2 : Z) P Q :
......
......@@ -76,13 +76,12 @@ Proof.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
wp (Σ:=Σ) coPset_all e (λ _, True) wp E (Fork e) (λ v, v = LitV LitUnit).
Lemma wp_fork E e Q :
( Q (LitV LitUnit) wp (Σ:=Σ) coPset_all e (λ _, True)) wp E (Fork e) Q.
Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
apply later_mono, sep_intro_True_l; last done.
by rewrite -(wp_value _ _ (Lit _)) //; apply const_intro.
rewrite later_sep -(wp_value _ _ (Lit _)) //.
Qed.
(* For the lemmas involving substitution, we only derive a preliminary version.
......
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