lifting.v 13.1 KB
 Ralf Jung committed Jan 27, 2016 1 ``````Require Import prelude.gmap iris.lifting. `````` Ralf Jung committed Jan 27, 2016 2 ``````Require Export iris.weakestpre barrier.parameter. `````` Ralf Jung committed Jan 26, 2016 3 4 ``````Import uPred. `````` Ralf Jung committed Jan 26, 2016 5 6 7 ``````(* TODO RJ: Figure out a way to to always use our Σ. *) (** Bind. *) `````` Ralf Jung committed Jan 30, 2016 8 ``````Lemma wp_bind {E e} K Q : `````` Ralf Jung committed Jan 27, 2016 9 `````` wp (Σ:=Σ) E e (λ v, wp (Σ:=Σ) E (fill K (v2e v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q. `````` Ralf Jung committed Jan 26, 2016 10 11 12 13 ``````Proof. by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx. Qed. `````` Ralf Jung committed Jan 30, 2016 14 ``````(** Base axioms for core primitives of the language: Stateful reductions. *) `````` Ralf Jung committed Jan 26, 2016 15 16 17 18 19 20 21 22 23 24 `````` Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 : E1 ⊆ E2 → to_val e1 = None → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ef = None ∧ φ e2 σ2) → pvs E2 E1 (ownP (Σ:=Σ) σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP (Σ:=Σ) σ2) -★ pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q)) ⊑ wp (Σ:=Σ) E2 e1 Q. Proof. intros ? He Hsafe Hstep. `````` Ralf Jung committed Jan 26, 2016 25 `````` (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *) `````` Ralf Jung committed Jan 26, 2016 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` etransitivity; last eapply wp_lift_step with (σ2 := σ1) (φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first. - intros e2 σ2 ef Hstep'%prim_ectx_step; last done. by apply Hstep. - destruct Hsafe as (e' & σ' & ? & ?). do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); eassumption. - done. - eassumption. - apply pvs_mono. apply sep_mono; first done. apply later_mono. apply forall_mono=>e2. apply forall_mono=>σ2. apply forall_intro=>ef. apply wand_intro_l. rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ. rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r. apply pvs_mono. rewrite right_id. done. Qed. `````` Ralf Jung committed Jan 26, 2016 43 44 45 `````` (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) `````` Ralf Jung committed Jan 30, 2016 46 ``````Lemma wp_alloc_pst E σ e v Q : `````` Ralf Jung committed Jan 27, 2016 47 `````` e2v e = Some v → `````` Ralf Jung committed Jan 30, 2016 48 49 `````` (ownP (Σ:=Σ) σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ) -★ Q (LocV l))) ⊑ wp (Σ:=Σ) E (Alloc e) Q. `````` Ralf Jung committed Jan 26, 2016 50 ``````Proof. `````` Ralf Jung committed Jan 27, 2016 51 `````` (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *) `````` Ralf Jung committed Jan 27, 2016 52 `````` intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 53 `````` (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None); `````` Ralf Jung committed Jan 26, 2016 54 `````` last first. `````` Ralf Jung committed Jan 26, 2016 55 `````` - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done. `````` Ralf Jung committed Jan 27, 2016 56 `````` rewrite Hv in Hvl. inversion_clear Hvl. `````` Ralf Jung committed Jan 26, 2016 57 `````` eexists; split_ands; done. `````` Ralf Jung committed Jan 27, 2016 58 `````` - set (l := fresh \$ dom (gset loc) σ). `````` Ralf Jung committed Jan 27, 2016 59 `````` exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first done. `````` Ralf Jung committed Jan 27, 2016 60 `````` apply (not_elem_of_dom (D := gset loc)). apply is_fresh. `````` Ralf Jung committed Jan 26, 2016 61 62 `````` - reflexivity. - reflexivity. `````` Ralf Jung committed Jan 30, 2016 63 `````` - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono. `````` Ralf Jung committed Jan 26, 2016 64 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 30, 2016 65 66 `````` apply wand_intro_l. rewrite -pvs_intro. rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` Ralf Jung committed Jan 26, 2016 67 `````` apply const_elim_l. intros [l [-> [-> Hl]]]. `````` Ralf Jung committed Jan 30, 2016 68 `````` rewrite (forall_elim l). eapply const_intro_l; first eexact Hl. `````` Ralf Jung committed Jan 30, 2016 69 70 `````` rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r. rewrite -wp_value'; done. `````` Ralf Jung committed Jan 27, 2016 71 ``````Qed. `````` Ralf Jung committed Jan 26, 2016 72 `````` `````` Ralf Jung committed Jan 30, 2016 73 ``````Lemma wp_load_pst E σ l v Q : `````` Ralf Jung committed Jan 26, 2016 74 `````` σ !! l = Some v → `````` Ralf Jung committed Jan 30, 2016 75 `````` (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q v)) ⊑ wp (Σ:=Σ) E (Load (Loc l)) Q. `````` Ralf Jung committed Jan 26, 2016 76 77 ``````Proof. intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 78 79 80 `````` (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first. - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}. rewrite Hlookup. case=>->. done. `````` Ralf Jung committed Jan 27, 2016 81 `````` - do 3 eexists. econstructor; eassumption. `````` Ralf Jung committed Jan 26, 2016 82 83 `````` - reflexivity. - reflexivity. `````` Ralf Jung committed Jan 30, 2016 84 85 `````` - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono. `````` Ralf Jung committed Jan 26, 2016 86 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 30, 2016 87 88 `````` apply wand_intro_l. rewrite -pvs_intro. rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` Ralf Jung committed Jan 26, 2016 89 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 30, 2016 90 `````` by rewrite wand_elim_r -wp_value. `````` Ralf Jung committed Jan 26, 2016 91 92 ``````Qed. `````` Ralf Jung committed Jan 30, 2016 93 ``````Lemma wp_store_pst E σ l e v v' Q : `````` Ralf Jung committed Jan 27, 2016 94 `````` e2v e = Some v → `````` Ralf Jung committed Jan 26, 2016 95 `````` σ !! l = Some v' → `````` Ralf Jung committed Jan 30, 2016 96 `````` (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp (Σ:=Σ) E (Store (Loc l) e) Q. `````` Ralf Jung committed Jan 26, 2016 97 ``````Proof. `````` Ralf Jung committed Jan 27, 2016 98 `````` intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 99 100 `````` (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first. - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}. `````` Ralf Jung committed Jan 27, 2016 101 102 `````` rewrite Hvl in Hv. inversion_clear Hv. done. - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption. `````` Ralf Jung committed Jan 26, 2016 103 104 `````` - reflexivity. - reflexivity. `````` Ralf Jung committed Jan 30, 2016 105 106 `````` - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono. `````` Ralf Jung committed Jan 26, 2016 107 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 30, 2016 108 109 `````` apply wand_intro_l. rewrite -pvs_intro. rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` Ralf Jung committed Jan 26, 2016 110 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 30, 2016 111 `````` by rewrite wand_elim_r -wp_value'. `````` Ralf Jung committed Jan 26, 2016 112 ``````Qed. `````` Ralf Jung committed Jan 26, 2016 113 `````` `````` Ralf Jung committed Jan 30, 2016 114 ``````Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q : `````` Ralf Jung committed Jan 29, 2016 115 116 `````` e2v e1 = Some v1 → e2v e2 = Some v2 → σ !! l = Some v' → v' <> v1 → `````` Ralf Jung committed Jan 30, 2016 117 `````` (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q. `````` Ralf Jung committed Jan 29, 2016 118 119 120 121 122 123 124 125 126 127 ``````Proof. intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ', e' = LitFalse ∧ σ' = σ); last first. - intros e2' σ2' ef Hstep. inversion_clear Hstep; first done. (* FIXME this rewriting is rather ugly. *) exfalso. rewrite Hvl in Hv1. case:Hv1=>?; subst v1. rewrite Hlookup in H. case:H=>?; subst v'. done. - do 3 eexists. eapply CasFailS; eassumption. - reflexivity. - reflexivity. `````` Ralf Jung committed Jan 30, 2016 128 129 `````` - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono. `````` Ralf Jung committed Jan 29, 2016 130 `````` apply forall_intro=>e2'. apply forall_intro=>σ2'. `````` Ralf Jung committed Jan 30, 2016 131 132 `````` apply wand_intro_l. rewrite -pvs_intro. rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` Ralf Jung committed Jan 29, 2016 133 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 30, 2016 134 `````` by rewrite wand_elim_r -wp_value'. `````` Ralf Jung committed Jan 29, 2016 135 136 ``````Qed. `````` Ralf Jung committed Jan 30, 2016 137 ``````Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q : `````` Ralf Jung committed Jan 29, 2016 138 139 `````` e2v e1 = Some v1 → e2v e2 = Some v2 → σ !! l = Some v1 → `````` Ralf Jung committed Jan 30, 2016 140 `````` (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q. `````` Ralf Jung committed Jan 29, 2016 141 142 143 144 145 146 147 148 149 150 151 152 ``````Proof. intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first. - intros e2' σ2' ef Hstep. move:H. inversion_clear Hstep=>H. (* FIXME this rewriting is rather ugly. *) + exfalso. rewrite H in Hlookup. case:Hlookup=>?; subst vl. rewrite Hvl in Hv1. case:Hv1=>?; subst v1. done. + rewrite H in Hlookup. case:Hlookup=>?; subst v1. rewrite Hl in Hv2. case:Hv2=>?; subst v2. done. - do 3 eexists. eapply CasSucS; eassumption. - reflexivity. - reflexivity. `````` Ralf Jung committed Jan 30, 2016 153 154 `````` - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono. `````` Ralf Jung committed Jan 29, 2016 155 `````` apply forall_intro=>e2'. apply forall_intro=>σ2'. `````` Ralf Jung committed Jan 30, 2016 156 157 `````` apply wand_intro_l. rewrite -pvs_intro. rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` Ralf Jung committed Jan 29, 2016 158 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 30, 2016 159 `````` by rewrite wand_elim_r -wp_value'. `````` Ralf Jung committed Jan 29, 2016 160 161 ``````Qed. `````` Ralf Jung committed Jan 26, 2016 162 163 164 ``````(** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e : `````` Ralf Jung committed Jan 27, 2016 165 `````` ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ v, ■(v = LitUnitV)). `````` Ralf Jung committed Jan 26, 2016 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 ``````Proof. etransitivity; last eapply wp_lift_pure_step with (φ := λ e' ef, e' = LitUnit ∧ ef = Some e); last first. - intros σ1 e2 σ2 ef Hstep%prim_ectx_step; last first. { do 3 eexists. eapply ForkS. } inversion_clear Hstep. done. - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); []. eapply ForkS. - reflexivity. - apply later_mono. apply forall_intro=>e2. apply forall_intro=>ef. apply impl_intro_l. apply const_elim_l. intros [-> ->]. (* FIXME RJ This is ridicolous. *) transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I; first by rewrite left_id. apply sep_mono; last reflexivity. `````` Ralf Jung committed Jan 27, 2016 184 185 `````` rewrite -wp_value'; last reflexivity. by apply const_intro. `````` Ralf Jung committed Jan 26, 2016 186 ``````Qed. `````` 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 `````` Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 : to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ ef = None ∧ φ e2) → (▷ ∀ e2, ■ φ e2 → wp (Σ:=Σ) E e2 Q) ⊑ wp (Σ:=Σ) E e1 Q. Proof. intros He Hsafe Hstep. (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *) etransitivity; last eapply wp_lift_pure_step with (φ0 := λ e' ef, ef = None ∧ φ e'); last first. - intros σ1 e2 σ2 ef Hstep'%prim_ectx_step; last done. by apply Hstep. - intros σ1. destruct (Hsafe σ1) as (e' & σ' & ? & ?). do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); eassumption. - done. - apply later_mono. apply forall_mono=>e2. apply forall_intro=>ef. apply impl_intro_l. apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ. rewrite impl_elim_r. rewrite right_id. done. Qed. `````` Ralf Jung committed Jan 27, 2016 209 `````` `````` Ralf Jung committed Jan 30, 2016 210 211 212 ``````Lemma wp_rec E ef e v Q : e2v e = Some v → ▷wp (Σ:=Σ) E ef.[Rec ef, e /] Q ⊑ wp (Σ:=Σ) E (App (Rec ef) e) Q. `````` Ralf Jung committed Jan 27, 2016 213 214 ``````Proof. etransitivity; last eapply wp_lift_pure_step with `````` Ralf Jung committed Jan 30, 2016 215 `````` (φ := λ e', e' = ef.[Rec ef, e /]); last first. `````` Ralf Jung committed Jan 27, 2016 216 `````` - intros ? ? ? ? Hstep. inversion_clear Hstep. done. `````` Ralf Jung committed Jan 30, 2016 217 `````` - intros ?. do 3 eexists. eapply BetaS; eassumption. `````` Ralf Jung committed Jan 27, 2016 218 219 220 221 222 `````` - reflexivity. - apply later_mono, forall_intro=>e2. apply impl_intro_l. apply const_elim_l=>->. done. Qed. `````` Ralf Jung committed Jan 30, 2016 223 224 225 ``````Lemma wp_lam E ef e v Q : e2v e = Some v → ▷wp (Σ:=Σ) E ef.[e/] Q ⊑ wp (Σ:=Σ) E (App (Lam ef) e) Q. `````` Ralf Jung committed Jan 27, 2016 226 ``````Proof. `````` Ralf Jung committed Jan 30, 2016 227 `````` intros Hv. rewrite -wp_rec; last eassumption. `````` Ralf Jung committed Jan 27, 2016 228 229 230 231 232 `````` (* RJ: This pulls in functional extensionality. If that bothers us, we have to talk to the Autosubst guys. *) by asimpl. Qed. `````` Ralf Jung committed Jan 27, 2016 233 234 ``````Lemma wp_plus n1 n2 E Q : ▷Q (LitNatV (n1 + n2)) ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q. `````` Ralf Jung committed Jan 27, 2016 235 236 237 238 239 240 241 242 ``````Proof. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = LitNat (n1 + n2)); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; done. - intros ?. do 3 eexists. econstructor. - reflexivity. - apply later_mono, forall_intro=>e2. apply impl_intro_l. apply const_elim_l=>->. `````` Ralf Jung committed Jan 30, 2016 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 `````` rewrite -wp_value'; last reflexivity; done. Qed. Lemma wp_le_true n1 n2 E Q : n1 ≤ n2 → ▷Q LitTrueV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q. Proof. intros Hle. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = LitTrue); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; first done. exfalso. eapply le_not_gt with (n := n1); eassumption. - intros ?. do 3 eexists. econstructor; done. - reflexivity. - apply later_mono, forall_intro=>e2. apply impl_intro_l. apply const_elim_l=>->. rewrite -wp_value'; last reflexivity; done. Qed. Lemma wp_le_false n1 n2 E Q : `````` Ralf Jung committed Jan 30, 2016 262 `````` ~(n1 ≤ n2) → `````` Ralf Jung committed Jan 30, 2016 263 264 265 266 267 `````` ▷Q LitFalseV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q. Proof. intros Hle. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = LitFalse); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; last done. `````` Ralf Jung committed Jan 30, 2016 268 269 `````` exfalso. omega. - intros ?. do 3 eexists. econstructor; omega. `````` Ralf Jung committed Jan 30, 2016 270 271 272 `````` - reflexivity. - apply later_mono, forall_intro=>e2. apply impl_intro_l. apply const_elim_l=>->. `````` Ralf Jung committed Jan 27, 2016 273 274 `````` rewrite -wp_value'; last reflexivity; done. Qed. `````` Ralf Jung committed Jan 29, 2016 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 `````` Lemma wp_fst e1 v1 e2 v2 E Q : e2v e1 = Some v1 → e2v e2 = Some v2 → ▷Q v1 ⊑ wp (Σ:=Σ) E (Fst (Pair e1 e2)) Q. Proof. intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = e1); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep. done. - intros ?. do 3 eexists. econstructor; eassumption. - reflexivity. - apply later_mono, forall_intro=>e2'. apply impl_intro_l. apply const_elim_l=>->. rewrite -wp_value'; last eassumption; done. Qed. Lemma wp_snd e1 v1 e2 v2 E Q : e2v e1 = Some v1 → e2v e2 = Some v2 → ▷Q v2 ⊑ wp (Σ:=Σ) E (Snd (Pair e1 e2)) Q. Proof. intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = e2); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; done. - intros ?. do 3 eexists. econstructor; eassumption. - reflexivity. - apply later_mono, forall_intro=>e2'. apply impl_intro_l. apply const_elim_l=>->. rewrite -wp_value'; last eassumption; done. Qed. Lemma wp_case_inl e0 v0 e1 e2 E Q : e2v e0 = Some v0 → `````` Ralf Jung committed Jan 30, 2016 306 `````` ▷wp (Σ:=Σ) E e1.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q. `````` Ralf Jung committed Jan 29, 2016 307 308 309 310 311 312 313 314 315 316 317 318 ``````Proof. intros Hv0. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = e1.[e0/]); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; done. - intros ?. do 3 eexists. econstructor; eassumption. - reflexivity. - apply later_mono, forall_intro=>e1'. apply impl_intro_l. by apply const_elim_l=>->. Qed. Lemma wp_case_inr e0 v0 e1 e2 E Q : e2v e0 = Some v0 → `````` Ralf Jung committed Jan 30, 2016 319 `````` ▷wp (Σ:=Σ) E e2.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q. `````` Ralf Jung committed Jan 29, 2016 320 321 322 323 324 325 326 327 328 ``````Proof. intros Hv0. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = e2.[e0/]); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; done. - intros ?. do 3 eexists. econstructor; eassumption. - reflexivity. - apply later_mono, forall_intro=>e2'. apply impl_intro_l. by apply const_elim_l=>->. Qed. `````` Ralf Jung committed Jan 30, 2016 329 330 331 332 333 334 `````` (** Some stateless axioms that incorporate bind *) Lemma wp_let e1 e2 E Q : wp (Σ:=Σ) E e1 (λ v, ▷wp (Σ:=Σ) E (e2.[v2e v/]) Q) ⊑ wp (Σ:=Σ) E (Let e1 e2) Q. Proof. `````` Ralf Jung committed Jan 30, 2016 335 `````` rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v. `````` Ralf Jung committed Jan 30, 2016 336 337 `````` rewrite -wp_lam //. by rewrite v2v. Qed.``````