From 67325634192cc831657259aeeffe30d6e68858b1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 19 Apr 2018 16:19:36 +0200
Subject: [PATCH] more mask-related fancy update lemmas

---
 theories/bi/updates.v | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index e3496c94d..3faaf043c 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -224,23 +224,38 @@ Section fupd_derived.
   Qed.
   (** How to apply an arbitrary mask-changing view shift when having
       an arbitrary mask. *)
-  Lemma fupd_mask_frame E E1 E2 P :
-    E1 âŠ† E â†’ (|={E1,E2}=> P) -âˆ— (|={E,E2 âˆª (E âˆ– E1)}=> P).
+  Lemma fupd_mask_frame E E' E1 E2 P :
+    E1 âŠ† E â†’ E' = E2 âˆª (E âˆ– E1) â†’
+    (|={E1,E2}=> P) -âˆ— (|={E,E'}=> P).
   Proof.
-    intros ?. rewrite (fupd_mask_frame_r _ _ (E âˆ– E1)); last set_solver.
+    intros ? ->. rewrite (fupd_mask_frame_r _ _ (E âˆ– E1)); last set_solver.
     assert (E = E1 âˆª E âˆ– E1) as <-; last done.
     apply union_difference_L. done.
   Qed.
-  Lemma fupd_mask_frame_diff E E1 E2 P :
+  Lemma fupd_mask_frame_diff_open E E1 E2 P :
     (* E2 âŠ† E1 is needed bcause otherwise the [E âˆ– E2] could remove
        more invariants from E than it did from E1. *)
-    E2 âŠ† E1 â†’ E1 âŠ† E â†’ (|={E1,E1âˆ–E2}=> P) -âˆ— (|={E,Eâˆ–E2}=> P).
+    E1 âŠ† E â†’ E2 âŠ† E1 â†’ (|={E1,E1âˆ–E2}=> P) -âˆ— (|={E,Eâˆ–E2}=> P).
   Proof.
-    intros ? HE. rewrite (fupd_mask_frame E); last done.
+    intros HE ?. rewrite (fupd_mask_frame E); [|done..].
     assert (E1 âˆ– E2 âˆª E âˆ– E1 = E âˆ– E2) as <-; last done.
     apply (anti_symm (âŠ†)); first set_solver.
     rewrite {1}(union_difference_L _ _ HE). set_solver.
   Qed.
+  Lemma fupd_mask_frame_diff_close E E1 E2 P :
+    (* E2 âŠ† E1 is needed bcause otherwise the [E âˆ– E2] could remove
+       more invariants from E than it did from E1. *)
+    E1 âŠ† E â†’ E2 âŠ† E1 â†’ (|={E1âˆ–E2,E1}=> P) -âˆ— (|={Eâˆ–E2,E}=> P).
+  Proof.
+    intros HE ?. rewrite (fupd_mask_frame (E âˆ– E2)); [|set_solver..].
+    assert (E = E1 âˆª E âˆ– E2 âˆ– (E1 âˆ– E2)) as <-; last done.
+    apply (anti_symm (âŠ†)); last set_solver.
+    rewrite {1}(union_difference_L _ _ HE). set_solver.
+  Qed.
+
+  Lemma fupd_mask_same E E1 P :
+    E = E1 â†’ (|={E}=> P) -âˆ— (|={E,E1}=> P).
+  Proof. intros <-. done. Qed.
 
   Lemma fupd_sep E P Q : (|={E}=> P) âˆ— (|={E}=> Q) ={E}=âˆ— P âˆ— Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
-- 
GitLab