From b0d9c1a2c9d21efc12e6c3f3215de8a3df05ccd3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 21 Nov 2016 15:47:00 +0100
Subject: [PATCH] simplify proof of step_fupd_mask_mono
---
base_logic/lib/fancy_updates.v | 8 +++-----
1 file changed, 3 insertions(+), 5 deletions(-)
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 87a5bb15a..5f1836dc3 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -217,11 +217,9 @@ Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
Proof.
iIntros (??) "HP".
- iAssert (|={E2,E1}â–·=> True)%I as "HE".
- { iApply fupd_mono. apply later_intro. by iApply fupd_intro_mask. }
- iAssert (|={F2,F1}â–·=> True)%I as "HF".
- { iApply fupd_mono. apply later_intro. by iApply fupd_intro_mask. }
- iMod "HE". iMod "HP". iMod "HF". iModIntro. iNext. iMod "HF". iMod "HP". by iMod "HE".
+ iMod (fupd_intro_mask') as "HM1"; first fast_done. iMod "HP".
+ iMod (fupd_intro_mask') as "HM2"; first fast_done. iModIntro.
+ iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
Qed.
End step_fupd.
--
GitLab