From 59ebd81e2b2ffc09d3b83de85333de5ae9d4e74e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 13 Jun 2018 10:49:42 +0200
Subject: [PATCH] Mask-changing updates that take a step.

---
 theories/bi/notation.v                |  6 ++++++
 theories/bi/updates.v                 | 14 +++++++++-----
 theories/program_logic/ectx_lifting.v |  2 +-
 theories/program_logic/lifting.v      |  2 +-
 theories/program_logic/weakestpre.v   |  2 +-
 5 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 426076425..0b463ceea 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -69,6 +69,12 @@ Reserved Notation "P ={ E }=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }=∗  Q ']'").
 
+Reserved Notation "|={ E1 , E2 , E3 }â–·=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 , E3 }â–·=>  Q").
+Reserved Notation "P ={ E1 , E2 , E3 }▷=∗ Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "'[' P  '/' ={ E1 , E2 , E3 }▷=∗  Q ']'").
 Reserved Notation "|={ E1 , E2 }â–·=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }â–·=>  Q").
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 60e1346e2..75aa5770e 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -25,11 +25,15 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I : bi_scope.
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
 
 (** Fancy updates that take a step. *)
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I : bi_scope.
+Notation "|={ E1 , E2 , E3 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E3}=> Q))%I : bi_scope.
+Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P -∗ |={ E1,E2,E3 }▷=> Q)%I : bi_scope.
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2,E1}â–·=> Q)%I : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_scope.
 Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
 Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
 
+
+
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
@@ -277,15 +281,15 @@ Section fupd_derived.
   Qed.
 
   (** Fancy updates that take a step derived rules. *)
-  Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2}▷=> Q.
+  Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2,E3}▷=> Q.
   Proof.
     apply wand_intro_l.
     by rewrite (later_intro (P -∗ Q)%I) fupd_frame_l -later_sep fupd_frame_l
                wand_elim_l.
   Qed.
 
-  Lemma step_fupd_mask_frame_r E1 E2 Ef P :
-    E1 ## Ef → E2 ## Ef → (|={E1,E2}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}▷=> P.
+  Lemma step_fupd_mask_frame_r E1 E2 E3 Ef P :
+    E1 ## Ef → E2 ## Ef → (|={E1,E2,E3}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef,E3 ∪ Ef}▷=> P.
   Proof.
     intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
   Qed.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 0aeb171a4..419f8365e 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -18,7 +18,7 @@ Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 2c59398ba..0abcd876d 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -15,7 +15,7 @@ Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 54ff92eb8..bf585cc9c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -32,7 +32,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
      state_interp σ1 ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
+     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,∅,E}▷=∗
        state_interp σ2 ∗ wp E e2 Φ ∗
        [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
-- 
GitLab