From 19cac1c982bcd2840eb39b33b357ad978d3b7496 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 27 Jan 2016 11:06:25 +0100 Subject: [PATCH] specialized lifting lemma for our language (well, really for all ectx-based languages) --- barrier/lifting.v | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/barrier/lifting.v b/barrier/lifting.v index 56dbe7131..367a4e17b 100644 --- a/barrier/lifting.v +++ b/barrier/lifting.v @@ -43,8 +43,6 @@ Qed. (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) -(* TODO RJ: There is probably a specialized version of the lifting - lemma that would be useful here. *) Lemma wp_alloc E σ v: ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v)) (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). @@ -140,3 +138,25 @@ Proof. apply sep_mono; last reflexivity. rewrite -wp_value'; reflexivity. Qed. + +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. -- GitLab