From f5f09abbc57559867600273567b247df74a3ceee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 22:46:19 +0200
Subject: [PATCH] Allow framing in weakestpre.

---
 program_logic/hoare.v  | 6 ++----
 proofmode/weakestpre.v | 3 +++
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 38178d219..c0d87d3e0 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -96,13 +96,11 @@ Qed.
 
 Lemma ht_frame_l E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ v, R ★ Φ v }}.
-Proof.
-  iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
-Qed.
+Proof. iIntros "#Hwp ! [$ HP]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_r E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ v, Φ v ★ R }}.
-Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
+Proof. iIntros "#Hwp ! [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 30ebfd256..2e60cd40e 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -8,6 +8,9 @@ Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
+Global Instance frame_wp E e R Φ Ψ :
+  (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 Global Instance fsa_split_wp E e Φ :
   FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
 Proof. split. done. apply _. Qed.
-- 
GitLab