Commit a45a9d43 authored by Ralf Jung's avatar Ralf Jung

alternative definition of weakestpre matching the one on paper

parent fdd87a4f
Pipeline #364 failed with stage
......@@ -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
......
......@@ -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).
......
......@@ -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 :
......
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