From 84c052353ff3ccc90c684b812289b83284750950 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Mar 2017 10:05:29 +0100
Subject: [PATCH] Mononicity of step taking fancy updates.

---
 theories/base_logic/lib/fancy_updates.v | 3 +++
 theories/program_logic/ectx_lifting.v   | 7 +++----
 theories/program_logic/lifting.v        | 3 +--
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 1e643d387..0f26e334b 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/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.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 64a1ce2dc..fbe2fd51d 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/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 :
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 0b6c2dc41..5474416d1 100644
--- a/theories/program_logic/lifting.v
+++ b/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.
-- 
GitLab