From 818c9480bd4d61a0477ffdb144c2d0c57f8042ab Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 26 Jun 2020 12:42:07 +0200
Subject: [PATCH] remove 3-mask step-taking fupd notation

---
 theories/bi/ascii.v                   |  7 --
 theories/bi/notation.v                |  8 +--
 theories/bi/updates.v                 | 97 +++++++++++++--------------
 theories/program_logic/ectx_lifting.v |  2 +-
 theories/program_logic/lifting.v      |  2 +-
 theories/program_logic/weakestpre.v   |  2 +-
 6 files changed, 51 insertions(+), 67 deletions(-)

diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index b4c6d87ca..0f9559577 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -85,13 +85,6 @@ Notation "P ={ E }=* Q" := (P ={E}=âˆ— Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope
 .
 
-Notation "|={ E1 , E2 , E3 }|>=> Q" := (|={E1,E2,E3}â–·=> Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E1 , E2 , E3 }|>=* Q" := (P ={E1,E2,E3}â–·=âˆ— Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 } [ E2 ]|>=> Q" := (|={E1}[E2]â–·=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
-
 Notation "P ={ E1 } [ E2 ]|>=* Q" := (P ={E1}[E2]â–·=âˆ— Q)
   (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
 Notation "P ={ E1 } [ E2 ]|>=* Q" := (P ={E1}[E2]â–·=âˆ— Q)%I
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 6b2123c32..21813c140 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -93,12 +93,7 @@ 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 ']'").
+(** Step-taking updates *)
 Reserved Notation "|={ E1 } [ E2 ]â–·=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 } [ E2 ]â–·=>  Q").
@@ -112,6 +107,7 @@ Reserved Notation "P ={ E }â–·=âˆ— Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }â–·=âˆ—  Q ']'").
 
+(** Multi-step-taking updates *)
 Reserved Notation "|={ E1 } [ E2 ]â–·=>^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
    format "|={ E1 } [ E2 ]â–·=>^ n  Q").
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 98cead792..dfe7fb759 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -27,37 +27,32 @@ 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. *)
-(** These have three masks: one they start with, one that is active when the step
-    is taken, and one they and with.*)
-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 "P ={ E1 , E2 , E3 }â–·=âˆ— Q" := (P -âˆ— |={ E1,E2,E3 }â–·=> Q) (only parsing) : stdpp_scope.
-
-(** Often, the first and last mask are the same, so we just have two massk:
-    the "outer" one active at the beginning/end, and the "inner" one active
-    for each step. We avoid the "," here as that looks like a mask-changing update,
-    but this update really starts and ends at E1. *)
-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 "P ={ E1 } [ E2 ]â–·=âˆ— Q" := (P -âˆ— |={ E1 , E2, E1 }â–·=> Q) (only parsing) : stdpp_scope.
+(** These have two masks, but they are different than the two masks of a
+    mask-changing update: the first mask ("outer mask") holds at the beginning
+    and the end, the second mask ("inner mask") holds around each â–·. This is
+    also why we use a different notation than for the two masks of a
+    mask-changing updates. *)
+Notation "|={ Eo } [ Ei ]â–·=> Q" := (|={Eo,Ei}=> â–· |={Ei,Eo}=> Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]â–·=âˆ— Q" := (P -âˆ— |={Eo}[Ei]â–·=> Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]â–·=âˆ— Q" := (P -âˆ— |={Eo}[Ei]â–·=> Q) (only parsing) : stdpp_scope.
 
 Notation "|={ E }â–·=> Q" := (|={E}[E]â–·=> Q)%I : bi_scope.
 Notation "P ={ E }â–·=âˆ— Q" := (P ={E}[E]â–·=âˆ— Q)%I : bi_scope.
 Notation "P ={ E }â–·=âˆ— Q" := (P ={E}[E]â–·=âˆ— Q) : stdpp_scope.
 
 (** For the iterated version, in principle there are 4 masks:
-    "outer" and "inner" of [|={E1}[E2]â–·=>], as well as a potentially
+    "outer" and "inner" of [|={Eo}[Ei]â–·=>], as well as a potentially
     different "begin" and "end" mask. The latter can be obtained from
     this notation by adding normal mask-changing update modalities:
     [ |={Ebegin,Eouter}=> |={Eouter}[Einner]â–·=>^n |={Eouter,Eend}=> Q]
 *)
-Notation "|={ E1 } [ E2 ]â–·=>^ n Q" := (Nat.iter n (Î» P, |={E1}[E2]â–·=> P) Q)%I : bi_scope.
-Notation "P ={ E1 } [ E2 ]â–·=âˆ—^ n Q" := (P -âˆ— |={E1}[E2]â–·=>^n Q)%I : bi_scope.
-Notation "P ={ E1 } [ E2 ]â–·=âˆ—^ n Q" := (P -âˆ— |={E1}[E2]â–·=>^n Q) (only parsing) : stdpp_scope.
+Notation "|={ Eo } [ Ei ]â–·=>^ n Q" := (Nat.iter n (Î» P, |={Eo}[Ei]â–·=> P) Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]â–·=âˆ—^ n Q" := (P -âˆ— |={Eo}[Ei]â–·=>^n Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]â–·=âˆ—^ n Q" := (P -âˆ— |={Eo}[Ei]â–·=>^n Q) (only parsing) : stdpp_scope.
 
-Notation "|={ E1 }â–·=>^ n Q" := (|={E1}[E1]â–·=>^n Q)%I : bi_scope.
-Notation "P ={ E1 }â–·=âˆ—^ n Q" := (P ={E1}[E1]â–·=âˆ—^n Q)%I : bi_scope.
-Notation "P ={ E1 }â–·=âˆ—^ n Q" := (P ={E1}[E1]â–·=âˆ—^n Q) (only parsing) : stdpp_scope.
+Notation "|={ E }â–·=>^ n Q" := (|={E}[E]â–·=>^n Q)%I : bi_scope.
+Notation "P ={ E }â–·=âˆ—^ n Q" := (P ={E}[E]â–·=âˆ—^n Q)%I : bi_scope.
+Notation "P ={ E }â–·=âˆ—^ n Q" := (P ={E}[E]â–·=âˆ—^n Q) (only parsing) : stdpp_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
@@ -345,39 +340,39 @@ Section fupd_derived.
   Proof. by rewrite (big_opMS_commute _). Qed.
 
   (** Fancy updates that take a step derived rules. *)
-  Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}â–·=> P) -âˆ— (P -âˆ— Q) -âˆ— |={E1,E2,E3}â–·=> Q.
+  Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]â–·=> P) -âˆ— (P -âˆ— Q) -âˆ— |={Eo}[Ei]â–·=> 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 E3 Ef P :
-    E1 ## Ef â†’ E2 ## Ef â†’ (|={E1,E2,E3}â–·=> P) âŠ¢ |={E1 âˆª Ef,E2 âˆª Ef,E3 âˆª Ef}â–·=> P.
+  Lemma step_fupd_mask_frame_r Eo Ei Ef P :
+    Eo ## Ef â†’ Ei ## Ef â†’ (|={Eo}[Ei]â–·=> P) âŠ¢ |={Eo âˆª Ef}[Ei âˆª Ef]â–·=> P.
   Proof.
     intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
   Qed.
 
-  Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
-    F1 âŠ† F2 â†’ E1 âŠ† E2 â†’ (|={E1}[F2]â–·=> P) âŠ¢ |={E2}[F1]â–·=> P.
+  Lemma step_fupd_mask_mono Eo1 Eo2 Ei1 Ei2 P :
+    Ei2 âŠ† Ei1 â†’ Eo1 âŠ† Eo2 â†’ (|={Eo1}[Ei1]â–·=> P) âŠ¢ |={Eo2}[Ei2]â–·=> P.
   Proof.
-    intros ??. rewrite -(emp_sep (|={E1}[F2]â–·=> P)%I).
-    rewrite (fupd_intro_mask E2 E1 emp%I) //.
-    rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
-    rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
-    rewrite (fupd_intro_mask F2 F1 (|={_,_}=> emp)%I) //.
+    intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]â–·=> P)%I).
+    rewrite (fupd_intro_mask Eo2 Eo1 emp%I) //.
+    rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
+    rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
+    rewrite (fupd_intro_mask Ei1 Ei2 (|={_,_}=> emp)%I) //.
     rewrite fupd_frame_r. f_equiv.
     rewrite [X in (X âˆ— _)%I]later_intro -later_sep. f_equiv.
-    rewrite fupd_frame_r -(fupd_trans F1 F2 E2). f_equiv.
-    rewrite fupd_frame_l -(fupd_trans F2 E1 E2). f_equiv.
+    rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
+    rewrite fupd_frame_l -(fupd_trans Ei1 Eo1 Eo2). f_equiv.
     by rewrite fupd_frame_r left_id.
   Qed.
 
-  Lemma step_fupd_intro E1 E2 P : E2 âŠ† E1 â†’ â–· P -âˆ— |={E1}[E2]â–·=> P.
-  Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
+  Lemma step_fupd_intro Ei Eo P : Ei âŠ† Eo â†’ â–· P -âˆ— |={Eo}[Ei]â–·=> P.
+  Proof. intros. by rewrite -(step_fupd_mask_mono Ei _ Ei _) // -!fupd_intro. Qed.
 
-  Lemma step_fupd_frame_l E1 E2 R Q :
-    (R âˆ— |={E1}[E2]â–·=> Q) -âˆ— |={E1}[E2]â–·=> (R âˆ— Q).
+  Lemma step_fupd_frame_l Eo Ei R Q :
+    (R âˆ— |={Eo}[Ei]â–·=> Q) -âˆ— |={Eo}[Ei]â–·=> (R âˆ— Q).
   Proof.
     rewrite fupd_frame_l.
     apply fupd_mono.
@@ -385,21 +380,21 @@ Section fupd_derived.
     by apply later_mono, fupd_mono.
   Qed.
 
-  Lemma step_fupd_fupd E E' P : (|={E}[E']â–·=> P) âŠ£âŠ¢ (|={E}[E']â–·=> |={E}=> P).
+  Lemma step_fupd_fupd Eo Ei P : (|={Eo}[Ei]â–·=> P) âŠ£âŠ¢ (|={Eo}[Ei]â–·=> |={Eo}=> P).
   Proof.
     apply (anti_symm (âŠ¢)).
     - by rewrite -fupd_intro.
     - by rewrite fupd_trans.
   Qed.
 
-  Lemma step_fupdN_mono E1 E2 n P Q :
-    (P âŠ¢ Q) â†’ (|={E1}[E2]â–·=>^n P) âŠ¢ (|={E1}[E2]â–·=>^n Q).
+  Lemma step_fupdN_mono Eo Ei n P Q :
+    (P âŠ¢ Q) â†’ (|={Eo}[Ei]â–·=>^n P) âŠ¢ (|={Eo}[Ei]â–·=>^n Q).
   Proof.
     intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
   Qed.
 
-  Lemma step_fupdN_wand E1 E2 n P Q :
-    (|={E1}[E2]â–·=>^n P) -âˆ— (P -âˆ— Q) -âˆ— (|={E1}[E2]â–·=>^n Q).
+  Lemma step_fupdN_wand Eo Ei n P Q :
+    (|={Eo}[Ei]â–·=>^n P) -âˆ— (P -âˆ— Q) -âˆ— (|={Eo}[Ei]â–·=>^n Q).
   Proof.
     apply wand_intro_l. induction n as [|n IH]=> /=.
     { by rewrite wand_elim_l. }
@@ -414,8 +409,8 @@ Section fupd_derived.
       rewrite -step_fupd_fupd //.
   Qed.
 
-  Lemma step_fupdN_frame_l E1 E2 n R Q :
-    (R âˆ— |={E1}[E2]â–·=>^n Q) -âˆ— |={E1}[E2]â–·=>^n (R âˆ— Q).
+  Lemma step_fupdN_frame_l Eo Ei n R Q :
+    (R âˆ— |={Eo}[Ei]â–·=>^n Q) -âˆ— |={Eo}[Ei]â–·=>^n (R âˆ— Q).
   Proof.
     induction n as [|n IH]; simpl; [done|].
     rewrite step_fupd_frame_l IH //=.
@@ -486,13 +481,13 @@ Section fupd_derived.
       (|={E}=> âˆ€ x, Î¦ x) âŠ£âŠ¢ (âˆ€ x, |={E}=> Î¦ x).
     Proof. by apply fupd_plain_forall. Qed.
 
-    Lemma step_fupd_plain E E' P `{!Plain P} : (|={E}[E']â–·=> P) ={E}=âˆ— â–· â—‡ P.
+    Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]â–·=> P) ={Eo}=âˆ— â–· â—‡ P.
     Proof.
-      rewrite -(fupd_plain_mask _ E' (â–· â—‡ P)%I).
+      rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)%I).
       apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
     Qed.
 
-    Lemma step_fupdN_plain E E' n P `{!Plain P} : (|={E}[E']â–·=>^n P) ={E}=âˆ— â–·^n â—‡ P.
+    Lemma step_fupdN_plain Eo Ei n P `{!Plain P} : (|={Eo}[Ei]â–·=>^n P) ={Eo}=âˆ— â–·^n â—‡ P.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
@@ -502,16 +497,16 @@ Section fupd_derived.
         * by rewrite except_0_later.
     Qed.
 
-    Lemma step_fupd_plain_forall E1 E2 {A} (Î¦ : A â†’ PROP) `{!âˆ€ x, Plain (Î¦ x)} :
-      E2 âŠ† E1 â†’
-      (|={E1}[E2]â–·=> âˆ€ x, Î¦ x) âŠ£âŠ¢ (âˆ€ x, |={E1}[E2]â–·=> Î¦ x).
+    Lemma step_fupd_plain_forall Eo Ei {A} (Î¦ : A â†’ PROP) `{!âˆ€ x, Plain (Î¦ x)} :
+      Ei âŠ† Eo â†’
+      (|={Eo}[Ei]â–·=> âˆ€ x, Î¦ x) âŠ£âŠ¢ (âˆ€ x, |={Eo}[Ei]â–·=> Î¦ x).
     Proof.
       intros. apply (anti_symm _).
       { apply forall_intro=> x. by rewrite (forall_elim x). }
-      trans (âˆ€ x, |={E1}=> â–· â—‡ Î¦ x)%I.
+      trans (âˆ€ x, |={Eo}=> â–· â—‡ Î¦ x)%I.
       { apply forall_mono=> x. by rewrite step_fupd_plain. }
       rewrite -fupd_plain_forall'. apply fupd_elim.
-      rewrite -(fupd_except_0 E2 E1) -step_fupd_intro //.
+      rewrite -(fupd_except_0 Ei Eo) -step_fupd_intro //.
       by rewrite -later_forall -except_0_forall.
     Qed.
   End fupd_plainly_derived.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index f2d08c695..7af252db4 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -19,7 +19,7 @@ Lemma wp_lift_head_step_fupd {s E Î¦} e1 :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1 Îº Îºs n, state_interp Ïƒ1 (Îº ++ Îºs) n ={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 Îºs (length efs + n) âˆ—
       WP e2 @ s; E {{ Î¦ }} âˆ—
       [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ fork_post }})
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 5d895d6ec..9a2d292e4 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_step_fupd s E Î¦ e1 :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1 Îº Îºs n, state_interp Ïƒ1 (Îº ++ Îºs) n ={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 Îºs (length efs + n) âˆ—
       WP e2 @ s; E {{ Î¦ }} âˆ—
       [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ fork_post }})
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f5ed45646..ec4ab9f47 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -32,7 +32,7 @@ Definition wp_pre `{!irisG Î› Î£} (s : stuckness)
   | None => âˆ€ Ïƒ1 Îº Îºs n,
      state_interp Ïƒ1 (Îº ++ Îºs) n ={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 Îºs (length efs + n) âˆ—
          wp E e2 Î¦ âˆ—
          [âˆ— list] i â†¦ ef âˆˆ efs, wp âŠ¤ ef fork_post
-- 
GitLab