From 2d0a5475af38801a22c60332b2aa7cd044deb3b3 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 30 Jan 2016 10:49:29 +0100 Subject: [PATCH] state the lifting lemmas slightly differently --- barrier/lifting.v | 87 +++++++++++++++++++++-------------------------- barrier/tests.v | 26 +++++++------- modures/logic.v | 10 ++++++ 3 files changed, 63 insertions(+), 60 deletions(-) diff --git a/barrier/lifting.v b/barrier/lifting.v index a3812a05..50ea486f 100644 --- a/barrier/lifting.v +++ b/barrier/lifting.v @@ -45,10 +45,10 @@ Qed. (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) -Lemma wp_alloc_pst E σ e v: +Lemma wp_alloc_pst E σ e v Q : e2v e = Some v → - ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc e) - (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). + (ownP (Σ:=Σ) σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ) -★ Q (LocV l))) + ⊑ wp (Σ:=Σ) E (Alloc e) Q. Proof. (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *) intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ) @@ -62,21 +62,19 @@ Proof. apply (not_elem_of_dom (D := gset loc)). apply is_fresh. - reflexivity. - reflexivity. - - (* RJ FIXME I am sure there is a better way to invoke right_id, but I could not find it. *) - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). - apply sep_mono; first done. rewrite -later_intro. + - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono. apply forall_intro=>e2. apply forall_intro=>σ2. - apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. + apply wand_intro_l. rewrite -pvs_intro. + rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l. intros [l [-> [-> Hl]]]. - rewrite -wp_value'; last reflexivity. - erewrite <-exist_intro with (a := l). apply and_intro. - + by apply const_intro. - + done. + rewrite (forall_elim _ l). eapply const_intro_l; first eexact Hl. + rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r. + rewrite -wp_value'; done. Qed. -Lemma wp_load_pst E σ l v: +Lemma wp_load_pst E σ l v Q : σ !! l = Some v → - ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Load (Loc l)) (λ v', ■(v' = v) ∧ ownP (Σ:=Σ) σ). + (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q v)) ⊑ wp (Σ:=Σ) E (Load (Loc l)) Q. Proof. intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first. @@ -85,21 +83,19 @@ Proof. - do 3 eexists. econstructor; eassumption. - reflexivity. - reflexivity. - - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). - apply sep_mono; first done. rewrite -later_intro. + - rewrite -pvs_intro. + apply sep_mono; first done. apply later_mono. apply forall_intro=>e2. apply forall_intro=>σ2. - apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. + apply wand_intro_l. rewrite -pvs_intro. + rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l. intros [-> ->]. - rewrite -wp_value. apply and_intro. - + by apply const_intro. - + done. + by rewrite wand_elim_r -wp_value. Qed. -Lemma wp_store_pst E σ l e v v': +Lemma wp_store_pst E σ l e v v' Q : e2v e = Some v → σ !! l = Some v' → - ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) e) - (λ v', ■(v' = LitUnitV) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). + (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp (Σ:=Σ) E (Store (Loc l) e) Q. Proof. intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first. @@ -108,21 +104,19 @@ Proof. - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption. - reflexivity. - reflexivity. - - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). - apply sep_mono; first done. rewrite -later_intro. + - rewrite -pvs_intro. + apply sep_mono; first done. apply later_mono. apply forall_intro=>e2. apply forall_intro=>σ2. - apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. + apply wand_intro_l. rewrite -pvs_intro. + rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l. intros [-> ->]. - rewrite -wp_value'; last reflexivity. apply and_intro. - + by apply const_intro. - + done. + by rewrite wand_elim_r -wp_value'. Qed. -Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' : +Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q : e2v e1 = Some v1 → e2v e2 = Some v2 → σ !! l = Some v' → v' <> v1 → - ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) - (λ v', ■(v' = LitFalseV) ∧ ownP (Σ:=Σ) σ). + (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q. Proof. intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ', e' = LitFalse ∧ σ' = σ); last first. @@ -133,21 +127,19 @@ Proof. - do 3 eexists. eapply CasFailS; eassumption. - reflexivity. - reflexivity. - - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). - apply sep_mono; first done. rewrite -later_intro. + - rewrite -pvs_intro. + apply sep_mono; first done. apply later_mono. apply forall_intro=>e2'. apply forall_intro=>σ2'. - apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. + apply wand_intro_l. rewrite -pvs_intro. + rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l. intros [-> ->]. - rewrite -wp_value'; last reflexivity. apply and_intro. - + by apply const_intro. - + done. + by rewrite wand_elim_r -wp_value'. Qed. -Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 : +Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q : e2v e1 = Some v1 → e2v e2 = Some v2 → σ !! l = Some v1 → - ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) - (λ v', ■(v' = LitTrueV) ∧ ownP (Σ:=Σ) (<[l:=v2]>σ)). + (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q. Proof. intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first. @@ -160,14 +152,13 @@ Proof. - do 3 eexists. eapply CasSucS; eassumption. - reflexivity. - reflexivity. - - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). - apply sep_mono; first done. rewrite -later_intro. + - rewrite -pvs_intro. + apply sep_mono; first done. apply later_mono. apply forall_intro=>e2'. apply forall_intro=>σ2'. - apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. + apply wand_intro_l. rewrite -pvs_intro. + rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l. intros [-> ->]. - rewrite -wp_value'; last reflexivity. apply and_intro. - + by apply const_intro. - + done. + by rewrite wand_elim_r -wp_value'. Qed. (** Base axioms for core primitives of the language: Stateless reductions *) @@ -218,7 +209,7 @@ Proof. rewrite right_id. done. Qed. -Lemma wp_rec' E e v Q : +Lemma wp_rec E e v Q : ▷wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q. Proof. etransitivity; last eapply wp_lift_pure_step with @@ -233,7 +224,7 @@ Qed. Lemma wp_lam E e v Q : ▷wp (Σ:=Σ) E (e.[v2e v/]) Q ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q. Proof. - rewrite -wp_rec'. + rewrite -wp_rec. (* RJ: This pulls in functional extensionality. If that bothers us, we have to talk to the Autosubst guys. *) by asimpl. diff --git a/barrier/tests.v b/barrier/tests.v index 08992f51..4c0c3d86 100644 --- a/barrier/tests.v +++ b/barrier/tests.v @@ -37,25 +37,27 @@ Module LiftingTests. Goal ∀ σ E, (ownP (Σ:=Σ) σ) ⊑ (wp (Σ:=Σ) E e (λ v, ■(v = LitNatV 2))). Proof. move=> σ E. rewrite /e. - rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_mono. - { eapply wp_alloc_pst; done. } - move=>v; apply exist_elim=>l. apply const_elim_l; move=>[-> _] {v}. + rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_alloc_pst; last done. + apply sep_intro_True_r; first done. + rewrite -later_intro. apply forall_intro=>l. + apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_. rewrite -wp_lam -later_intro. asimpl. rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) (PlusLCtx EmptyCtx _)) (Load (Loc _)))). - rewrite -wp_mono. - { eapply wp_load_pst. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *) - move=>v; apply const_elim_l; move=>-> {v}. + rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first. + { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *) + rewrite -later_intro. apply wand_intro_l. rewrite right_id. rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))). rewrite -wp_plus -later_intro. rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))). - rewrite -wp_mono. - { eapply wp_store_pst; first reflexivity. apply: lookup_insert. } - move=>v; apply const_elim_l; move=>-> {v}. + rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first. + { apply: lookup_insert. } + { reflexivity. } + rewrite -later_intro. apply wand_intro_l. rewrite right_id. rewrite -wp_lam -later_intro. asimpl. - rewrite -wp_mono. - { eapply wp_load_pst. apply: lookup_insert. } - move=>v; apply const_elim_l; move=>-> {v}. + rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first. + { apply: lookup_insert. } + rewrite -later_intro. apply wand_intro_l. rewrite right_id. by apply const_intro. Qed. End LiftingTests. diff --git a/modures/logic.v b/modures/logic.v index 3f31b923..51aba5c3 100644 --- a/modures/logic.v +++ b/modures/logic.v @@ -616,6 +616,16 @@ Proof. intros ->; apply sep_elim_l. Qed. Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R. Proof. intros ->; apply sep_elim_r. Qed. Hint Resolve sep_elim_l' sep_elim_r'. +Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q). +Proof. + intros HP HQ. etransitivity; last (eapply sep_mono; eassumption). + by rewrite left_id. +Qed. +Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q). +Proof. + intros HP HQ. etransitivity; last (eapply sep_mono; eassumption). + by rewrite right_id. +Qed. Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R). Proof. rewrite (commutative _); apply wand_intro_r. Qed. Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q. -- GitLab