From b90854c7e7415a4baee131406e1d89c682e1df79 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Feb 2016 21:30:52 +0100
Subject: [PATCH] Generalize wp_fork to have an arbitrary post-condition.

---
 heap_lang/derived.v | 2 +-
 heap_lang/lifting.v | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 3d2a02b29..b834c31fa 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -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 :
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 918810a61..289a24ae7 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -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.
-- 
GitLab