Allow framing in weakestpre.

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 →

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.