Commit 461bd9f0 authored by Ralf Jung's avatar Ralf Jung

heap_lang: rename lifting lemmas so that the final forms do not have a prime

parent fd3aa446
......@@ -15,18 +15,18 @@ Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E x ef e v Q :
Lemma wp_lam' E x ef e v Q :
to_val e = Some v wp E (subst ef x v) Q wp E (App (Lam x ef) e) Q.
Proof. intros. by rewrite -wp_rec ?subst_empty. Qed.
Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed.
Lemma wp_let E x e1 e2 v Q :
Lemma wp_let' E x e1 e2 v Q :
to_val e1 = Some v wp E (subst e2 x v) Q wp E (Let x e1 e2) Q.
Proof. apply wp_lam. Qed.
Proof. apply wp_lam'. Qed.
Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, wp E e2 Q) wp E (Seq e1 e2) Q.
Proof.
rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
by rewrite -wp_let //= ?to_of_val ?subst_empty.
by rewrite -wp_let' //= ?to_of_val ?subst_empty.
Qed.
Lemma wp_le E (n1 n2 : Z) P Q :
......
......@@ -84,7 +84,9 @@ Proof.
by rewrite -(wp_value' _ _ (Lit _)) //; apply const_intro.
Qed.
Lemma wp_rec E f x e1 e2 v Q :
(* For the lemmas involving substitution, we only derive a preliminary version.
The final version is defined in substitution.v. *)
Lemma wp_rec' E f x e1 e2 v Q :
to_val e2 = Some v
wp E (subst (subst e1 f (RecV f x e1)) x v) Q wp E (App (Rec f x e1) e2) Q.
Proof.
......@@ -137,7 +139,7 @@ Proof.
?right_id -?wp_value' //; intros; inv_step; eauto.
Qed.
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
to_val e0 = Some v0
wp E (subst e1 x1 v0) Q wp E (Case (InjL e0) x1 e1 x2 e2) Q.
Proof.
......@@ -145,7 +147,7 @@ Proof.
(subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
Qed.
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Q :
to_val e0 = Some v0
wp E (subst e2 x2 v0) Q wp E (Case (InjR e0) x1 e1 x2 e2) Q.
Proof.
......
......@@ -120,32 +120,32 @@ Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ.
Hint Resolve to_of_val.
Lemma wp_rec' E e1 f x erec e2 v Q :
Lemma wp_rec E e1 f x erec e2 v Q :
e1 = Rec f x erec
to_val e2 = Some v
wp E (gsubst (gsubst erec f e1) x e2) Q wp E (App e1 e2) Q.
Proof.
intros -> <-%of_to_val.
rewrite (gsubst_correct _ _ (RecV _ _ _)) gsubst_correct.
by apply wp_rec.
by apply wp_rec'.
Qed.
Lemma wp_lam' E x ef e v Q :
Lemma wp_lam E x ef e v Q :
to_val e = Some v wp E (gsubst ef x e) Q wp E (App (Lam x ef) e) Q.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam. Qed.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam'. Qed.
Lemma wp_let' E x e1 e2 v Q :
Lemma wp_let E x e1 e2 v Q :
to_val e1 = Some v wp E (gsubst e2 x e1) Q wp E (Let x e1 e2) Q.
Proof. apply wp_lam'. Qed.
Proof. apply wp_lam. Qed.
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
to_val e0 = Some v0
wp E (gsubst e1 x1 e0) Q wp E (Case (InjL e0) x1 e1 x2 e2) Q.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl. Qed.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl'. Qed.
Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Q :
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
to_val e0 = Some v0
wp E (gsubst e2 x2 e0) Q wp E (Case (InjR e0) x1 e1 x2 e2) Q.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr. Qed.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr'. Qed.
End wp.
......@@ -69,12 +69,12 @@ 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.
(* Go on *)
rewrite -wp_let' //= -later_intro.
rewrite -wp_let //= -later_intro.
rewrite -(wp_bindi (LetCtx _ _)) -wp_bin_op //= -wp_let' //= -!later_intro.
rewrite -(wp_bindi (IfCtx _ _)) /=.
apply wp_lt=> ?.
......@@ -88,7 +88,7 @@ Module LiftingTests.
Lemma Pred_spec n E Q : Q (LitV (n - 1)) wp E (Pred 'n)%L Q.
Proof.
rewrite -wp_lam' //=.
rewrite -wp_lam //=.
rewrite -(wp_bindi (IfCtx _ _)) /=.
apply later_mono, wp_le=> Hn.
- rewrite -wp_if_true.
......
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