Write `wp_strong_mono` in a curried way.

theories/program_logic/weakestpre.v

@@ -213,9 +213,9 @@ Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
 
 Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
   s1 ⊑ s2 → E1 ⊆ E2 →
-  (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ s1; E1 {{ Φ }} ⊢ WP e @ s2; E2 {{ Ψ }}.
+  WP e @ s1; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 {{ Ψ }}.
 Proof.
-  iIntros (? HE) "[HΦ H]". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
+  iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
@@ -224,9 +224,9 @@ Proof.
   iModIntro. iSplit; [by destruct s1, s2|]. iNext. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "($ & H & Hefs)".
   iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
-  - by iApply ("IH" with "[] HΦ").
+  - iApply ("IH" with "[//] H HΦ").
   - iApply (big_sepL_impl with "[$Hefs]"); iIntros "!#" (k ef _) "H".
-    by iApply ("IH" with "[] [] H").
+    by iApply ("IH" with "[] H").
 Qed.
 
 Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
@@ -236,7 +236,7 @@ Proof.
   iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
-Proof. iIntros "H". iApply (wp_strong_mono s s E); try iFrame; auto. Qed.
+Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
 
 Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
@@ -263,8 +263,8 @@ Proof.
   iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
-  iMod "HR". iModIntro. iApply (wp_strong_mono s s E2); [done..|].
-  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
+  iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
+  iIntros (v) "H". by iApply "H".
 Qed.
 
 Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
@@ -300,17 +300,17 @@ Qed.
 (** * Derived rules *)
 Lemma wp_mono s E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros (HΦ) "H"; iApply (wp_strong_mono s s E E); auto.
-  iIntros "{$H}" (v) "?". by iApply HΦ.
+  iIntros (HΦ) "H"; iApply (wp_strong_mono with "H"); auto.
+  iIntros (v) "?". by iApply HΦ.
 Qed.
 Lemma wp_stuck_mono s1 s2 E e Φ :
   s1 ⊑ s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
-Proof. iIntros (?) "H". iApply (wp_strong_mono s1 s2); auto with iFrame. Qed.
+Proof. iIntros (?) "H". iApply (wp_strong_mono with "H"); auto. Qed.
 Lemma wp_stuck_weaken s E e Φ :
   WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
 Proof. apply wp_stuck_mono. by destruct s. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
-Proof. iIntros (?) "H"; iApply (wp_strong_mono s s E1 E2); auto. iFrame; eauto. Qed.
+Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
 Global Instance wp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
@@ -324,9 +324,9 @@ Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono s s E E _ Φ); try iFrame; eauto. Qed.
+Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono s s E E _ Φ); try iFrame; eauto. Qed.
+Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 
 Lemma wp_frame_step_l s E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
@@ -352,8 +352,8 @@ Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qe
 Lemma wp_wand s E e Φ Ψ :
   WP e @ s; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros "Hwp H". iApply (wp_strong_mono s s E); auto.
-  iIntros "{$Hwp}" (?) "?". by iApply "H".
+  iIntros "Hwp H". iApply (wp_strong_mono with "Hwp"); auto.
+  iIntros (?) "?". by iApply "H".
 Qed.
 Lemma wp_wand_l s E e Φ Ψ :
   (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.