Commit 4c3cbc71 authored by Ralf Jung's avatar Ralf Jung

wakestpre: swap wp_value and wp_value'

The rationale is that, just like the always lemmas about uPred and the frame-preserving updates for maps and iprdos, the versions with the ' are the "more specific" versions, hard-coding more assumptions in the shape of their conclusion.
parent 461bd9f0
......@@ -81,7 +81,7 @@ Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
apply later_mono, sep_intro_True_l; last done.
by rewrite -(wp_value' _ _ (Lit _)) //; apply const_intro.
by rewrite -(wp_value _ _ (Lit _)) //; apply const_intro.
Qed.
(* For the lemmas involving substitution, we only derive a preliminary version.
......@@ -100,7 +100,7 @@ Lemma wp_un_op E op l l' Q :
Q (LitV l') wp E (UnOp op (Lit l)) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
?right_id -?wp_value' //; intros; inv_step; eauto.
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
Lemma wp_bin_op E op l1 l2 l' Q :
......@@ -108,7 +108,7 @@ Lemma wp_bin_op E op l1 l2 l' Q :
Q (LitV l') wp E (BinOp op (Lit l1) (Lit l2)) Q.
Proof.
intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
?right_id -?wp_value' //; intros; inv_step; eauto.
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
Lemma wp_if_true E e1 e2 Q : wp E e1 Q wp E (If (Lit $ LitBool true) e1 e2) Q.
......@@ -128,7 +128,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
Q v1 wp E (Fst $ Pair e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
?right_id -?wp_value' //; intros; inv_step; eauto.
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
Lemma wp_snd E e1 v1 e2 v2 Q :
......@@ -136,7 +136,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
Q v2 wp E (Snd $ Pair e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
?right_id -?wp_value' //; intros; inv_step; eauto.
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
......
......@@ -47,7 +47,7 @@ Module LiftingTests.
{ by rewrite lookup_insert. }
{ done. }
rewrite -later_intro. apply wand_intro_l. rewrite right_id.
rewrite -wp_seq -wp_value -later_intro.
rewrite -wp_seq -wp_value' -later_intro.
rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
{ by rewrite lookup_insert. }
rewrite -later_intro. apply wand_intro_l. rewrite right_id.
......@@ -69,7 +69,7 @@ Module LiftingTests.
rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?.
(* first need to do the rec to get a later *)
rewrite -(wp_bindi (AppLCtx _)) /=.
rewrite -wp_rec // =>-/=; rewrite -wp_value' //=.
rewrite -wp_rec // =>-/=; rewrite -wp_value //=.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
rewrite ->(later_intro (Q _)).
rewrite -!later_and; apply later_mono.
......@@ -83,7 +83,7 @@ Module LiftingTests.
by rewrite left_id impl_elim_l.
- assert (n1 = n2 - 1) as -> by omega.
rewrite -wp_if_false -!later_intro.
by rewrite -wp_value' // and_elim_r.
by rewrite -wp_value // and_elim_r.
Qed.
Lemma Pred_spec n E Q : Q (LitV (n - 1)) wp E (Pred 'n)%L Q.
......
......@@ -33,7 +33,7 @@ Lemma ht_val E v :
{{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
Proof.
apply (always_intro _ _), impl_intro_l.
by rewrite -wp_value; apply const_intro.
by rewrite -wp_value'; apply const_intro.
Qed.
Lemma ht_vs E P P' Q Q' e :
((P ={E}=> P') {{ P' }} e @ E {{ Q' }} v, Q' v ={E}=> Q v)
......
......@@ -68,7 +68,7 @@ Proof.
by repeat apply and_intro; try apply const_intro.
* apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
rewrite -(of_to_val e2 v) // -wp_value.
rewrite -(of_to_val e2 v) // -wp_value'; [].
rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
Qed.
......
......@@ -75,7 +75,7 @@ Proof.
apply const_elim_l=>-[v2' [Hv ?]] /=.
rewrite -pvs_intro.
rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
by rewrite left_id wand_elim_r -(wp_value' _ _ e2' v2').
by rewrite left_id wand_elim_r -(wp_value _ _ e2' v2').
Qed.
Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
......
......@@ -105,7 +105,7 @@ Lemma wp_step_inv E Ef Q e k n σ r rf :
wp_go (E Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Lemma wp_value E Q v : Q v wp E (of_val v) Q.
Lemma wp_value' E Q v : Q v wp E (of_val v) Q.
Proof. by constructor; apply pvs_intro. Qed.
Lemma pvs_wp E e Q : pvs E E (wp E e Q) wp E e Q.
Proof.
......@@ -204,8 +204,8 @@ Global Instance wp_mono' E e :
Proof. by intros Q Q' ?; apply wp_mono. Qed.
Lemma wp_strip_pvs E e P Q : P wp E e Q pvs E E P wp E e Q.
Proof. move=>->. by rewrite pvs_wp. Qed.
Lemma wp_value' E Q e v : to_val e = Some v Q v wp E e Q.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
Lemma wp_value E Q e v : to_val e = Some v Q v wp E e Q.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
Lemma wp_frame_l E e Q R : (R wp E e Q) wp E e (λ v, R Q v).
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
Lemma wp_frame_later_l E e Q R :
......
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