Mononicity of step taking fancy updates.

theories/base_logic/lib/fancy_updates.v

@@ -217,6 +217,9 @@ Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
 Section step_fupd.
 Context `{invG Σ}.
 
+Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2}▷=> Q.
+Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
+
 Lemma step_fupd_mask_frame_r E1 E2 Ef P :
   E1 ⊥ Ef → E2 ⊥ Ef → (|={E1,E2}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}▷=> P.
 Proof.

theories/program_logic/ectx_lifting.v

@@ -38,8 +38,8 @@ Lemma wp_lift_pure_head_step {E E' Φ} e1 :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto.
-  iMod "H". iModIntro. iNext. iMod "H". iModIntro.
-  iIntros (????). iApply "H". eauto.
+  iApply (step_fupd_wand with "H"); iIntros "H".
+  iIntros (????). iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step {E Φ} e1 :
@@ -67,8 +67,7 @@ Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iNext; iIntros (v2 σ2 efs) "%".
-  iMod ("H" $! v2 σ2 efs with "[#]") as "(% & $ & $)"=>//; subst.
-  by iApply big_sepL_nil.
+  iMod ("H" $! v2 σ2 efs with "[#]") as "(% & $ & $)"=>//; subst; auto.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :

theories/program_logic/lifting.v

@@ -65,8 +65,7 @@ Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
 Proof.
   iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
   { by intros; eapply Hpuredet. }
-  (* TODO: Can we make this nicer? iNext for fupd, for example, could help. *)
-  iMod "H". iModIntro. iNext. iMod "H". iModIntro.
+  iApply (step_fupd_wand with "H"); iIntros "H".
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.