From 93792f5c4cddd2a44344b5673bf0e8731f0b0b9b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 May 2016 21:31:02 +0200
Subject: [PATCH] Change notations of big_ops for upred.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Rationale: to make the code closer to what is on paper, I want the notations
to look like quantifiers, i.e. have a binder built-in. I thus introduced the
following notations:

  [★ map] k ↦ x ∈ m, P
  [★ set] x ∈ X, P

The good thing - contrary to the notations that we had before that required an
explicit lambda - is that type annotations of k and x are now not printed
making goals much easier to read.
---
 algebra/upred_big_op.v        | 99 +++++++++++++++++++++--------------
 algebra/upred_tactics.v       |  3 +-
 heap_lang/heap.v              |  2 +-
 heap_lang/lib/barrier/proof.v |  4 +-
 proofmode/coq_tactics.v       | 24 ++++-----
 5 files changed, 75 insertions(+), 57 deletions(-)

diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 6702eb075..d7b34262d 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -2,31 +2,44 @@ From iris.algebra Require Export upred list.
 From iris.prelude Require Import gmap fin_collections functions.
 Import uPred.
 
+(** We define the following big operators:
+
+- The operators [ [★] Ps ] and [ [∧] Ps ] fold [★] and [∧] over the list [Ps].
+  This operator is not a quantifier, so it binds strongly.
+- The operator [ [★ map] k ↦ x ∈ m, P ] asserts that [P] holds separately for
+  each [k ↦ x] in the map [m]. This operator is a quantifier, and thus has the
+  same precedence as [∀] and [∃].
+- The operator [ [★ set] x ∈ X, P ] asserts that [P] holds separately for each
+  [x] in the set [X]. This operator is a quantifier, and thus has the same
+  precedence as [∀] and [∃]. *)
+
 (** * Big ops over lists *)
 (* These are the basic building blocks for other big ops *)
-Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:=
+Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M :=
   match Ps with [] => True | P :: Ps => P ∧ uPred_big_and Ps end%I.
 Instance: Params (@uPred_big_and) 1.
-Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
+Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
 Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
   match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I.
 Instance: Params (@uPred_big_sep) 1.
-Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
+Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
 
 (** * Other big ops *)
 (** We use a type class to obtain overloaded notations *)
 Definition uPred_big_sepM {M} `{Countable K} {A}
     (m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
-  uPred_big_sep (curry Φ <$> map_to_list m).
+  [★] (curry Φ <$> map_to_list m).
 Instance: Params (@uPred_big_sepM) 6.
-Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ)
-  (at level 20, m at level 10, format "Π★{map  m }  Φ") : uPred_scope.
+Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
+  (at level 200, m at level 10, k, x at level 1, right associativity,
+   format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
 
 Definition uPred_big_sepS {M} `{Countable A}
-  (X : gset A) (Φ : A → uPred M) : uPred M := uPred_big_sep (Φ <$> elements X).
+  (X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <$> elements X).
 Instance: Params (@uPred_big_sepS) 5.
-Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
-  (at level 20, X at level 10, format "Π★{set  X }  Φ") : uPred_scope.
+Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
+  (at level 200, X at level 10, x at level 1, right associativity,
+   format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
 
 (** * Persistence of lists of uPreds *)
 Class PersistentL {M} (Ps : list (uPred M)) :=
@@ -70,26 +83,26 @@ Proof.
   - etrans; eauto.
 Qed.
 
-Lemma big_and_app Ps Qs : Π∧ (Ps ++ Qs) ⊣⊢ (Π∧ Ps ∧ Π∧ Qs).
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_app Ps Qs : Π★ (Ps ++ Qs) ⊣⊢ (Π★ Ps ★ Π★ Qs).
+Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ ([∧] Ps ∧ [∧] Qs).
+Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
+Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ ([★] Ps ★ [★] Qs).
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
 
-Lemma big_and_contains Ps Qs : Qs `contains` Ps → Π∧ Ps ⊢ Π∧ Qs.
+Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs.
 Proof.
   intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
 Qed.
-Lemma big_sep_contains Ps Qs : Qs `contains` Ps → Π★ Ps ⊢ Π★ Qs.
+Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [★] Ps ⊢ [★] Qs.
 Proof.
   intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
 Qed.
 
-Lemma big_sep_and Ps : Π★ Ps ⊢ Π∧ Ps.
+Lemma big_sep_and Ps : [★] Ps ⊢ [∧] Ps.
 Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
 
-Lemma big_and_elem_of Ps P : P ∈ Ps → Π∧ Ps ⊢ P.
+Lemma big_and_elem_of Ps P : P ∈ Ps → [∧] Ps ⊢ P.
 Proof. induction 1; simpl; auto with I. Qed.
-Lemma big_sep_elem_of Ps P : P ∈ Ps → Π★ Ps ⊢ P.
+Lemma big_sep_elem_of Ps P : P ∈ Ps → [★] Ps ⊢ P.
 Proof. induction 1; simpl; auto with I. Qed.
 
 (** ** Big ops over finite maps *)
@@ -100,16 +113,16 @@ Section gmap.
 
   Lemma big_sepM_mono Φ Ψ m1 m2 :
     m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
-    Π★{map m1} Φ ⊢ Π★{map m2} Ψ.
+    ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
   Proof.
-    intros HX HΦ. trans (Π★{map m2} Φ)%I.
+    intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
     - by apply big_sep_contains, fmap_contains, map_to_list_contains.
     - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
       apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
   Qed.
   Lemma big_sepM_proper Φ Ψ m1 m2 :
     m1 ≡ m2 → (∀ x k, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
-    Π★{map m1} Φ ⊣⊢ Π★{map m2} Ψ.
+    ([★ map] k ↦ x ∈ m1, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
   Proof.
     (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
     File "./algebra/upred_big_op.v", line 114, characters 4-131:
@@ -134,28 +147,32 @@ Section gmap.
            (uPred_big_sepM (M:=M) m).
   Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
 
-  Lemma big_sepM_empty Φ : Π★{map ∅} Φ ⊣⊢ True.
+  Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
   Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
   Lemma big_sepM_insert Φ (m : gmap K A) i x :
-    m !! i = None → Π★{map <[i:=x]> m} Φ ⊣⊢ (Φ i x ★ Π★{map m} Φ).
+    m !! i = None →
+    ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ m, Φ k y).
   Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
   Lemma big_sepM_delete Φ (m : gmap K A) i x :
-    m !! i = Some x → Π★{map m} Φ ⊣⊢ (Φ i x ★ Π★{map delete i m} Φ).
+    m !! i = Some x →
+    ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y).
   Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed.
-  Lemma big_sepM_singleton Φ i x : Π★{map {[i := x]}} Φ ⊣⊢ (Φ i x).
+  Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
   Proof.
     rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
     by rewrite big_sepM_empty right_id.
   Qed.
 
   Lemma big_sepM_sepM Φ Ψ m :
-    Π★{map m} (λ i x, Φ i x ★ Ψ i x) ⊣⊢ (Π★{map m} Φ ★ Π★{map m} Ψ).
+       ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
+    ⊣⊢ (([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x)).
   Proof.
     rewrite /uPred_big_sepM.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
     by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
   Qed.
-  Lemma big_sepM_later Φ m : ▷ Π★{map m} Φ ⊣⊢ Π★{map m} (λ i x, ▷ Φ i x).
+  Lemma big_sepM_later Φ m :
+    (▷ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
   Proof.
     rewrite /uPred_big_sepM.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
@@ -170,15 +187,17 @@ Section gset.
   Implicit Types Φ : A → uPred M.
 
   Lemma big_sepS_mono Φ Ψ X Y :
-    Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → Π★{set X} Φ ⊢ Π★{set Y} Ψ.
+    Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) →
+    ([★ set] x ∈ X, Φ x) ⊢ ([★ set] x ∈ Y, Ψ x).
   Proof.
-    intros HX HΦ. trans (Π★{set Y} Φ)%I.
+    intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I.
     - by apply big_sep_contains, fmap_contains, elements_contains.
     - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
       apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
   Qed.
   Lemma big_sepS_proper Φ Ψ X Y :
-    X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) → Π★{set X} Φ ⊣⊢ Π★{set Y} Ψ.
+    X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) →
+    ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x).
   Proof.
     intros [??] ?; apply (anti_symm (⊢)); apply big_sepS_mono;
       eauto using equiv_entails, equiv_entails_sym.
@@ -197,44 +216,44 @@ Section gset.
     Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X).
   Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
 
-  Lemma big_sepS_empty Φ : Π★{set ∅} Φ ⊣⊢ True.
+  Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True.
   Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
 
   Lemma big_sepS_insert Φ X x :
-    x ∉ X → Π★{set {[ x ]} ∪ X} Φ ⊣⊢ (Φ x ★ Π★{set X} Φ).
+    x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y).
   Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
   Lemma big_sepS_insert' (Ψ : A → uPred M → uPred M) Φ X x P :
     x ∉ X →
-    Π★{set {[ x ]} ∪ X} (λ y, Ψ y (<[x:=P]> Φ y))
-    ⊣⊢ (Ψ x P ★ Π★{set X} (λ y, Ψ y (Φ y))).
+       ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=P]> Φ y))
+    ⊣⊢ (Ψ x P ★ [★ set] y ∈ X, Ψ y (Φ y)).
   Proof.
     intros. rewrite big_sepS_insert // fn_lookup_insert.
     apply sep_proper, big_sepS_proper; auto=> y ??.
     by rewrite fn_lookup_insert_ne; last set_solver.
   Qed.
   Lemma big_sepS_insert'' Φ X x P :
-    x ∉ X → Π★{set {[ x ]} ∪ X} (<[x:=P]> Φ) ⊣⊢ (P ★ Π★{set X} Φ).
+    x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
   Proof. apply (big_sepS_insert' (λ y, id)). Qed.
 
   Lemma big_sepS_delete Φ X x :
-    x ∈ X → Π★{set X} Φ ⊣⊢ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ).
+    x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y).
   Proof.
     intros. rewrite -big_sepS_insert; last set_solver.
     by rewrite -union_difference_L; last set_solver.
   Qed.
 
-  Lemma big_sepS_singleton Φ x : Π★{set {[ x ]}} Φ ⊣⊢ (Φ x).
+  Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
   Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
 
   Lemma big_sepS_sepS Φ Ψ X :
-    Π★{set X} (λ x, Φ x ★ Ψ x) ⊣⊢ (Π★{set X} Φ ★ Π★{set X} Ψ).
+    ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ (([★ set] y ∈ X, Φ y) ★ [★ set] y ∈ X, Ψ y).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
     by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
   Qed.
 
-  Lemma big_sepS_later Φ X : ▷ Π★{set X} Φ ⊣⊢ Π★{set X} (λ x, ▷ Φ x).
+  Lemma big_sepS_later Φ X : (▷ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
@@ -243,9 +262,9 @@ Section gset.
 End gset.
 
 (** ** Persistence *)
-Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP (Π∧ Ps).
+Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP ([∧] Ps).
 Proof. induction 1; apply _. Qed.
-Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP (Π★ Ps).
+Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([★] Ps).
 Proof. induction 1; apply _. Qed.
 
 Global Instance nil_persistent : PersistentL (@nil (uPred M)).
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 3d8757115..7c8d74f5a 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -22,8 +22,7 @@ Module uPred_reflection. Section uPred_reflection.
     | ESep e1 e2 => flatten e1 ++ flatten e2
     end.
 
-  Notation eval_list Σ l :=
-    (uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
+  Notation eval_list Σ l := ([★] ((λ n, from_option True%I (Σ !! n)) <$> l))%I.
   Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
   Proof.
     induction e as [| |e1 IH1 e2 IH2];
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 5de7c10d8..cd105a28b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -98,7 +98,7 @@ Section heap.
   (** Allocation *)
   Lemma heap_alloc N E σ :
     authG heap_lang Σ heapR → nclose N ⊆ E →
-    ownP σ ⊢ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} (λ l v, l ↦ v)).
+    ownP σ ⊢ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ [★ map] l↦v ∈ σ, l ↦ v).
   Proof.
     intros. rewrite -{1}(from_to_heap σ). etrans.
     { rewrite [ownP _]later_intro.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index f091da42a..99a9f6ed0 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -28,7 +28,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition ress (P : iProp) (I : gset gname) : iProp :=
   (∃ Ψ : gname → iProp,
-    ▷ (P -★ Π★{set I} Ψ) ★ Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I.
+    ▷ (P -★ [★ set] i ∈ I, Ψ i) ★ [★ set] i ∈ I, saved_prop_own i (Ψ i))%I.
 
 Coercion state_to_val (s : state) : val :=
   match s with State Low _ => #0 | State High _ => #1 end.
@@ -159,7 +159,7 @@ Proof.
     iSplit; [iPureIntro; by eauto using wait_step|].
     iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
     iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
-    iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I with "[HΨ]" as "[HΨ HΨ']".
+    iAssert (▷ Ψ i ★ ▷ [★ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
     { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
     iSplitL "HΨ' Hl Hsp"; [iNext|].
     + rewrite {2}/barrier_inv /=; iFrame "Hl".
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 3e2a5691f..2caf70d7f 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -25,7 +25,7 @@ Record envs_wf {M} (Δ : envs M) := {
 }.
 
 Coercion of_envs {M} (Δ : envs M) : uPred M :=
-  (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+  (■ envs_wf Δ ★ □ [∧] env_persistent Δ ★ [★] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 
 Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
@@ -102,7 +102,7 @@ Implicit Types Δ : envs M.
 Implicit Types P Q : uPred M.
 
 Lemma of_envs_def Δ :
-  of_envs Δ = (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+  of_envs Δ = (■ envs_wf Δ ★ □ [∧] env_persistent Δ ★ [★] env_spatial Δ)%I.
 Proof. done. Qed.
 
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
@@ -120,12 +120,12 @@ Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
-    ecancel [□ Π∧ _; □ P; Π★ _]%I; apply const_intro.
+    ecancel [□ [∧] _; □ P; [★] _]%I; apply const_intro.
     destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=.
-    ecancel [□ Π∧ _; P; Π★ _]%I; apply const_intro.
+    ecancel [□ [∧] _; P; [★] _]%I; apply const_intro.
     destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh.
 Qed.
@@ -158,7 +158,7 @@ Lemma envs_lookup_delete_sound' Δ Δ' i p P :
   envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ (P ★ Δ')%I.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
 
-Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ (□?p Π★ Γ -★ Δ').
+Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ (□?p [★] Γ -★ Δ').
 Proof.
   rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -182,7 +182,7 @@ Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ (□?p Π★ Γ -★ Δ')%I.
+  envs_delete i p Δ ⊢ (□?p [★] Γ -★ Δ')%I.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -206,11 +206,11 @@ Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ (□?p P ★ (□?p Π★ Γ -★ Δ'))%I.
+  Δ ⊢ (□?p P ★ (□?p [★] Γ -★ Δ'))%I.
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ (□?q Π★ Γ -★ Δ')%I.
+  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ (□?q [★] Γ -★ Δ')%I.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -219,7 +219,7 @@ Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ (□?p P ★ (□?q Π★ Γ -★ Δ'))%I.
+  Δ ⊢ (□?p P ★ (□?q [★] Γ -★ Δ'))%I.
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_split_sound Δ lr js Δ1 Δ2 :
@@ -228,21 +228,21 @@ Proof.
   rewrite /envs_split /of_envs=> ?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
   rewrite (env_split_perm Γs) // big_sep_app {1}always_sep_dup'.
-  destruct lr; simplify_eq/=; cancel [□ Π∧ Γp; □ Π∧ Γp; Π★ Γs1; Π★ Γs2]%I;
+  destruct lr; simplify_eq/=; cancel [□ [∧] Γp; □ [∧] Γp; [★] Γs1; [★] Γs2]%I;
     destruct Hwf; apply sep_intro_True_l; apply const_intro; constructor;
       naive_solver eauto using env_split_wf_1, env_split_wf_2,
       env_split_fresh_1, env_split_fresh_2.
 Qed.
 
 Lemma envs_clear_spatial_sound Δ :
-  Δ ⊢ (envs_clear_spatial Δ ★ Π★ env_spatial Δ)%I.
+  Δ ⊢ (envs_clear_spatial Δ ★ [★] env_spatial Δ)%I.
 Proof.
   rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
   rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
   destruct Hwf; constructor; simpl; auto using Enil_wf.
 Qed.
 
-Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ ⊣⊢ (Π★ Γ -★ Q).
+Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ ⊣⊢ ([★] Γ -★ Q).
 Proof.
   revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
   by rewrite IH wand_curry (comm uPred_sep).
-- 
GitLab