From adf3a991677a986cf8789897f2c2b40c13cf368c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 09:14:59 +0100
Subject: [PATCH] wp_value_pvs

---
 program_logic/weakestpre.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 137aa6adb..973c1eb94 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -206,6 +206,8 @@ 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_pvs E Q e v : to_val e = Some v → pvs E E (Q v) ⊑ wp E e Q.
+Proof. intros. rewrite -wp_pvs. rewrite -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 :
-- 
GitLab