From b25fe256c52dd66717118957f869125c376ab7bc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 23 Feb 2020 23:15:01 +0100
Subject: [PATCH] Add lemma `twp_wp_step`.

---
 theories/program_logic/total_weakestpre.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 0f25045e7..5a34be327 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -253,6 +253,15 @@ Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
 Lemma twp_wand_r s E e Φ Ψ :
   WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
 Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
+
+Lemma twp_wp_step s E e P Φ :
+  TCEq (to_val e) None →
+  ▷ P -∗
+  WP e @ s; E [{ v, P ={E}=∗ Φ v }] -∗ WP e @ s; E {{ Φ }}.
+Proof.
+  iIntros (?) "HP Hwp".
+  iApply (wp_step_fupd _ _ E _ P with "[HP]"); [auto..|]. by iApply twp_wp.
+Qed.
 End twp.
 
 (** Proofmode class instances *)
-- 
GitLab