From a45a9d439437f5826dddb4c78d93d47050fe70ba Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Mar 2016 13:08:29 +0100
Subject: [PATCH] alternative definition of weakestpre matching the one on
 paper

---
 _CoqProject             | 1 +
 algebra/cofe.v          | 4 +++-
 program_logic/lifting.v | 2 +-
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 7fa23825d..0cbaa47d1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -64,6 +64,7 @@ program_logic/viewshifts.v
 program_logic/wsat.v
 program_logic/ownership.v
 program_logic/weakestpre.v
+program_logic/weakestpre_fix.v
 program_logic/pviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
diff --git a/algebra/cofe.v b/algebra/cofe.v
index a6ef44bd4..14941ef14 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -252,9 +252,11 @@ Infix "-n>" := cofe_mor (at level 45, right associativity).
 Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
   Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
 
-(** Identity and composition *)
+(** Identity and composition and constant function *)
 Definition cid {A} : A -n> A := CofeMor id.
 Instance: Params (@cid) 1.
+Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x).
+Instance: Params (@cconst) 2.
 
 Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index edade4d96..b14d26623 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -15,7 +15,7 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
-Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, ■ True)))%I.
+Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
 
 Lemma wp_lift_step E1 E2
     (φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 σ1 :
-- 
GitLab