diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v index 6702eb0755ddfd4e704aa1666096ab915761091e..d7b34262da498364bfded8084a267913295f7897 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 3d8757115c3bf6ba14147d2dc9241b707bea5e97..7c8d74f5a0c063bd8cc5cc994bad2bf28dc271c3 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 5de7c10d8b5def0132ea3448e80534e2ee72279d..cd105a28bf67803704b5c32d1214a8d1c2c3f811 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 f091da42adcecec4510121640252b3d0fd974cb1..99a9f6ed0c522497923afe636fb922e87bb30ad0 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 3e2a5691fa06ebefb3659cc557568ff53101de44..2caf70d7f6f8b745ef438d4eee4ef91c9d17f74d 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).