diff --git a/base_logic/big_op.v b/base_logic/big_op.v index 214c9e69eff422cfbaf4ebdda81be5bfd433f0db..23542229613fda42a284613117da04610a417f18 100644 --- a/base_logic/big_op.v +++ b/base_logic/big_op.v @@ -23,7 +23,7 @@ Section cmra. intros _. by apply HP. Qed. - Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ★ Q)%I → ✓{n} P. + Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ∗ Q)%I → ✓{n} P. Proof. unseal. intros HPQ n' x ??. destruct (HPQ n' x) as (x1&x2&->&?&?); auto. @@ -84,25 +84,25 @@ Arguments uPredR : clear implicits. Arguments uPredUR : clear implicits. (* Notations *) -Notation "'[★]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope. +Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope. -Notation "'[★' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P)) +Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P)) (at level 200, l at level 10, k, x at level 1, right associativity, - format "[★ list ] k ↦ x ∈ l , P") : uPred_scope. -Notation "'[★' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P)) + format "[∗ list ] k ↦ x ∈ l , P") : uPred_scope. +Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P)) (at level 200, l at level 10, x at level 1, right associativity, - format "[★ list ] x ∈ l , P") : uPred_scope. + format "[∗ list ] x ∈ l , P") : uPred_scope. -Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P)) +Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) 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. -Notation "'[★' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P)) + format "[∗ map ] k ↦ x ∈ m , P") : uPred_scope. +Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P)) (at level 200, m at level 10, x at level 1, right associativity, - format "[★ map ] x ∈ m , P") : uPred_scope. + format "[∗ map ] x ∈ m , P") : uPred_scope. -Notation "'[★' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P)) +Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P)) (at level 200, X at level 10, x at level 1, right associativity, - format "[★ set ] x ∈ X , P") : uPred_scope. + format "[∗ set ] x ∈ X , P") : uPred_scope. (** * Persistence and timelessness of lists of uPreds *) Class PersistentL {M} (Ps : list (uPred M)) := @@ -123,16 +123,16 @@ Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. -Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs. +Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs. Proof. by rewrite big_op_app. 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. apply uPred_included. by apply: big_op_contains. Qed. -Lemma big_sep_elem_of Ps P : P ∈ Ps → [★] Ps ⊢ P. +Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P. Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. (** ** Persistence *) -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)). @@ -159,7 +159,7 @@ Proof. Qed. (** ** Timelessness *) -Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([★] Ps). +Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps). Proof. induction 1; apply _. Qed. Global Instance nil_timeless : TimelessL (@nil (uPred M)). @@ -191,25 +191,25 @@ Section list. Implicit Types l : list A. Implicit Types Φ Ψ : nat → A → uPred M. - Lemma big_sepL_nil Φ : ([★ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. + Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ True. Proof. done. Qed. Lemma big_sepL_cons Φ x l : - ([★ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ★ [★ list] k↦y ∈ l, Φ (S k) y. + ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y. Proof. by rewrite big_opL_cons. Qed. - Lemma big_sepL_singleton Φ x : ([★ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. + Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x. Proof. by rewrite big_opL_singleton. Qed. Lemma big_sepL_app Φ l1 l2 : - ([★ list] k↦y ∈ l1 ++ l2, Φ k y) - ⊣⊢ ([★ list] k↦y ∈ l1, Φ k y) ★ ([★ list] k↦y ∈ l2, Φ (length l1 + k) y). + ([∗ list] k↦y ∈ l1 ++ l2, Φ k y) + ⊣⊢ ([∗ list] k↦y ∈ l1, Φ k y) ∗ ([∗ list] k↦y ∈ l2, Φ (length l1 + k) y). Proof. by rewrite big_opL_app. Qed. Lemma big_sepL_mono Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → - ([★ list] k ↦ y ∈ l, Φ k y) ⊢ [★ list] k ↦ y ∈ l, Ψ k y. + ([∗ list] k ↦ y ∈ l, Φ k y) ⊢ [∗ list] k ↦ y ∈ l, Ψ k y. Proof. apply big_opL_forall; apply _. Qed. Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → - ([★ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([★ list] k ↦ y ∈ l, Ψ k y). + ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y). Proof. apply big_opL_proper. Qed. Global Instance big_sepL_mono' l : @@ -218,37 +218,37 @@ Section list. Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Lemma big_sepL_lookup Φ l i x : - l !! i = Some x → ([★ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. + l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x. Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed. Lemma big_sepL_elem_of (Φ : A → uPred M) l x : - x ∈ l → ([★ list] y ∈ l, Φ y) ⊢ Φ x. + x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x. Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed. Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l : - ([★ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([★ list] k↦y ∈ l, Φ k (f y)). + ([∗ list] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)). Proof. by rewrite big_opL_fmap. Qed. Lemma big_sepL_sepL Φ Ψ l : - ([★ list] k↦x ∈ l, Φ k x ★ Ψ k x) - ⊣⊢ ([★ list] k↦x ∈ l, Φ k x) ★ ([★ list] k↦x ∈ l, Ψ k x). + ([∗ list] k↦x ∈ l, Φ k x ∗ Ψ k x) + ⊣⊢ ([∗ list] k↦x ∈ l, Φ k x) ∗ ([∗ list] k↦x ∈ l, Ψ k x). Proof. by rewrite big_opL_opL. Qed. Lemma big_sepL_later Φ l : - ▷ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, ▷ Φ k x). + ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x). Proof. apply (big_opL_commute _). Qed. Lemma big_sepL_always Φ l : - (□ [★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □ Φ k x). + (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x). Proof. apply (big_opL_commute _). Qed. Lemma big_sepL_always_if p Φ l : - □?p ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □?p Φ k x). + □?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x). Proof. apply (big_opL_commute _). Qed. Lemma big_sepL_forall Φ l : (∀ k x, PersistentP (Φ k x)) → - ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, l !! k = Some x → Φ k x). + ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, l !! k = Some x → Φ k x). Proof. intros HΦ. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. @@ -261,8 +261,8 @@ Section list. Qed. Lemma big_sepL_impl Φ Ψ l : - □ (∀ k x, l !! k = Some x → Φ k x → Ψ k x) ∧ ([★ list] k↦x ∈ l, Φ k x) - ⊢ [★ list] k↦x ∈ l, Ψ k x. + □ (∀ k x, l !! k = Some x → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x) + ⊢ [∗ list] k↦x ∈ l, Ψ k x. Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. setoid_rewrite always_impl; setoid_rewrite always_pure. @@ -271,16 +271,16 @@ Section list. Qed. Global Instance big_sepL_nil_persistent Φ : - PersistentP ([★ list] k↦x ∈ [], Φ k x). + PersistentP ([∗ list] k↦x ∈ [], Φ k x). Proof. rewrite /big_opL. apply _. Qed. Global Instance big_sepL_persistent Φ l : - (∀ k x, PersistentP (Φ k x)) → PersistentP ([★ list] k↦x ∈ l, Φ k x). + (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x). Proof. rewrite /big_opL. apply _. Qed. Global Instance big_sepL_nil_timeless Φ : - TimelessP ([★ list] k↦x ∈ [], Φ k x). + TimelessP ([∗ list] k↦x ∈ [], Φ k x). Proof. rewrite /big_opL. apply _. Qed. Global Instance big_sepL_timeless Φ l : - (∀ k x, TimelessP (Φ k x)) → TimelessP ([★ list] k↦x ∈ l, Φ k x). + (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x). Proof. rewrite /big_opL. apply _. Qed. End list. @@ -293,16 +293,16 @@ Section gmap. Lemma big_sepM_mono Φ Ψ m1 m2 : m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → - ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x. + ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x. Proof. - intros Hm HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I. + intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I. - apply uPred_included. apply: big_op_contains. by apply fmap_contains, map_to_list_contains. - apply big_opM_forall; apply _ || auto. Qed. Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → - ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x). + ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x). Proof. apply big_opM_proper. Qed. Global Instance big_sepM_mono' m : @@ -310,66 +310,66 @@ Section gmap. (big_opM (M:=uPredUR M) m). Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. - Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. + Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. Proof. by rewrite big_opM_empty. Qed. Lemma big_sepM_insert Φ m i x : m !! i = None → - ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y. + ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y. Proof. apply: big_opM_insert. Qed. Lemma big_sepM_delete Φ m i x : m !! i = Some x → - ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y. + ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. Proof. apply: big_opM_delete. Qed. Lemma big_sepM_lookup Φ m i x : - m !! i = Some x → ([★ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. + m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. - Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. + Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. Proof. by rewrite big_opM_singleton. Qed. Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m : - ([★ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)). + ([∗ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)). Proof. by rewrite big_opM_fmap. Qed. Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y : m !! i = Some x → - ([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k). + ([∗ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([∗ map] k↦_ ∈ m, Φ k). Proof. apply: big_opM_insert_override. Qed. Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b : m !! i = None → - ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k)) - ⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)). + ([∗ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k)) + ⊣⊢ (Ψ i x b ∗ [∗ map] k↦y ∈ m, Ψ k y (f k)). Proof. apply: big_opM_fn_insert. Qed. Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P : m !! i = None → - ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k). + ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k). Proof. apply: big_opM_fn_insert'. Qed. Lemma big_sepM_sepM Φ Ψ m : - ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x) - ⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x). + ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) + ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). Proof. apply: big_opM_opM. Qed. Lemma big_sepM_later Φ m : - ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). + ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x). Proof. apply (big_opM_commute _). Qed. Lemma big_sepM_always Φ m : - (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x). + (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x). Proof. apply (big_opM_commute _). Qed. Lemma big_sepM_always_if p Φ m : - □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x). + □?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x). Proof. apply (big_opM_commute _). Qed. Lemma big_sepM_forall Φ m : (∀ k x, PersistentP (Φ k x)) → - ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, m !! k = Some x → Φ k x). + ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, m !! k = Some x → Φ k x). Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. @@ -385,8 +385,8 @@ Section gmap. Qed. Lemma big_sepM_impl Φ Ψ m : - □ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([★ map] k↦x ∈ m, Φ k x) - ⊢ [★ map] k↦x ∈ m, Ψ k x. + □ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x) + ⊢ [∗ map] k↦x ∈ m, Ψ k x. Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. setoid_rewrite always_impl; setoid_rewrite always_pure. @@ -395,16 +395,16 @@ Section gmap. Qed. Global Instance big_sepM_empty_persistent Φ : - PersistentP ([★ map] k↦x ∈ ∅, Φ k x). + PersistentP ([∗ map] k↦x ∈ ∅, Φ k x). Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. Global Instance big_sepM_persistent Φ m : - (∀ k x, PersistentP (Φ k x)) → PersistentP ([★ map] k↦x ∈ m, Φ k x). + (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x). Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed. Global Instance big_sepM_nil_timeless Φ : - TimelessP ([★ map] k↦x ∈ ∅, Φ k x). + TimelessP ([∗ map] k↦x ∈ ∅, Φ k x). Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. Global Instance big_sepM_timeless Φ m : - (∀ k x, TimelessP (Φ k x)) → TimelessP ([★ map] k↦x ∈ m, Φ k x). + (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x). Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed. End gmap. @@ -417,65 +417,65 @@ Section gset. Lemma big_sepS_mono Φ Ψ X Y : Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → - ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x. + ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x. Proof. - intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I. + intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I. - apply uPred_included. apply: big_op_contains. by apply fmap_contains, elements_contains. - apply big_opS_forall; apply _ || auto. Qed. Lemma big_sepS_proper Φ Ψ X : (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → - ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ X, Ψ x). + ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x). Proof. apply: big_opS_proper. Qed. Global Instance big_sepS_mono' X : Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X). Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. - Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True. + Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True. Proof. by rewrite big_opS_empty. Qed. Lemma big_sepS_insert Φ X x : - x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y). + x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y). Proof. apply: big_opS_insert. Qed. Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b : x ∉ X → - ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) - ⊣⊢ (Ψ x b ★ [★ set] y ∈ X, Ψ y (f y)). + ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) + ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)). Proof. apply: big_opS_fn_insert. Qed. Lemma big_sepS_fn_insert' Φ X x P : - x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y). + x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). Proof. apply: big_opS_fn_insert'. Qed. Lemma big_sepS_delete Φ X x : - x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y. + x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. Proof. apply: big_opS_delete. Qed. - Lemma big_sepS_elem_of Φ X x : x ∈ X → ([★ set] y ∈ X, Φ y) ⊢ Φ x. + Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x. Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. - Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. + Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. Proof. apply: big_opS_singleton. Qed. Lemma big_sepS_sepS Φ Ψ X : - ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y). + ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y). Proof. apply: big_opS_opS. Qed. - Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). + Lemma big_sepS_later Φ X : ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y). Proof. apply (big_opS_commute _). Qed. - Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y). + Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y). Proof. apply (big_opS_commute _). Qed. Lemma big_sepS_always_if q Φ X : - □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y). + □?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y). Proof. apply (big_opS_commute _). Qed. Lemma big_sepS_forall Φ X : - (∀ x, PersistentP (Φ x)) → ([★ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ■ (x ∈ X) → Φ x). + (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ■ (x ∈ X) → Φ x). Proof. intros. apply (anti_symm _). { apply forall_intro=> x. @@ -489,7 +489,7 @@ Section gset. Qed. Lemma big_sepS_impl Φ Ψ X : - □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x. + □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x. Proof. rewrite always_and_sep_l always_forall. setoid_rewrite always_impl; setoid_rewrite always_pure. @@ -497,15 +497,15 @@ Section gset. by rewrite -always_wand_impl always_elim wand_elim_l. Qed. - Global Instance big_sepS_empty_persistent Φ : PersistentP ([★ set] x ∈ ∅, Φ x). + Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x). Proof. rewrite /big_opS elements_empty. apply _. Qed. Global Instance big_sepS_persistent Φ X : - (∀ x, PersistentP (Φ x)) → PersistentP ([★ set] x ∈ X, Φ x). + (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x). Proof. rewrite /big_opS. apply _. Qed. - Global Instance big_sepS_nil_timeless Φ : TimelessP ([★ set] x ∈ ∅, Φ x). + Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x). Proof. rewrite /big_opS elements_empty. apply _. Qed. Global Instance big_sepS_timeless Φ X : - (∀ x, TimelessP (Φ x)) → TimelessP ([★ set] x ∈ X, Φ x). + (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x). Proof. rewrite /big_opS. apply _. Qed. End gset. End big_op. diff --git a/base_logic/derived.v b/base_logic/derived.v index 5432b0b1e677cc5bb253f615801b46b43c7a19f3..5d1483a7efa8f0dfdc31034ded8a77f4f98e1beb 100644 --- a/base_logic/derived.v +++ b/base_logic/derived.v @@ -297,16 +297,16 @@ Qed. (* Derived BI Stuff *) Hint Resolve sep_mono. -Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ★ P' ⊢ Q ★ P'. +Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'. Proof. by intros; apply sep_mono. Qed. -Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ★ P' ⊢ P ★ Q'. +Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'. Proof. by apply sep_mono. Qed. Global Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_sep M). Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed. Global Instance sep_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_sep M). Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed. -Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -★ P') ⊢ Q -★ Q'. +Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -∗ P') ⊢ Q -∗ Q'. Proof. intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'. Qed. @@ -327,67 +327,67 @@ Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M). Proof. intros P; apply (anti_symm _); auto using True_sep_1, True_sep_2. Qed. Global Instance sep_True : RightId (⊣⊢) True%I (@uPred_sep M). Proof. by intros P; rewrite comm left_id. Qed. -Lemma sep_elim_l P Q : P ★ Q ⊢ P. +Lemma sep_elim_l P Q : P ∗ Q ⊢ P. Proof. by rewrite (True_intro Q) right_id. Qed. -Lemma sep_elim_r P Q : P ★ Q ⊢ Q. -Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed. -Lemma sep_elim_l' P Q R : (P ⊢ R) → P ★ Q ⊢ R. +Lemma sep_elim_r P Q : P ∗ Q ⊢ Q. +Proof. by rewrite (comm (∗))%I; apply sep_elim_l. Qed. +Lemma sep_elim_l' P Q R : (P ⊢ R) → P ∗ Q ⊢ R. Proof. intros ->; apply sep_elim_l. Qed. -Lemma sep_elim_r' P Q R : (Q ⊢ R) → P ★ Q ⊢ R. +Lemma sep_elim_r' P Q R : (Q ⊢ R) → P ∗ Q ⊢ R. Proof. intros ->; apply sep_elim_r. Qed. Hint Resolve sep_elim_l' sep_elim_r'. -Lemma sep_intro_True_l P Q R : (True ⊢ P) → (R ⊢ Q) → R ⊢ P ★ Q. +Lemma sep_intro_True_l P Q R : (True ⊢ P) → (R ⊢ Q) → R ⊢ P ∗ Q. Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed. -Lemma sep_intro_True_r P Q R : (R ⊢ P) → (True ⊢ Q) → R ⊢ P ★ Q. +Lemma sep_intro_True_r P Q R : (R ⊢ P) → (True ⊢ Q) → R ⊢ P ∗ Q. Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed. -Lemma sep_elim_True_l P Q R : (True ⊢ P) → (P ★ R ⊢ Q) → R ⊢ Q. +Lemma sep_elim_True_l P Q R : (True ⊢ P) → (P ∗ R ⊢ Q) → R ⊢ Q. Proof. by intros HP; rewrite -HP left_id. Qed. -Lemma sep_elim_True_r P Q R : (True ⊢ P) → (R ★ P ⊢ Q) → R ⊢ Q. +Lemma sep_elim_True_r P Q R : (True ⊢ P) → (R ∗ P ⊢ Q) → R ⊢ Q. Proof. by intros HP; rewrite -HP right_id. Qed. -Lemma wand_intro_l P Q R : (Q ★ P ⊢ R) → P ⊢ Q -★ R. +Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R. Proof. rewrite comm; apply wand_intro_r. Qed. -Lemma wand_elim_l P Q : (P -★ Q) ★ P ⊢ Q. +Lemma wand_elim_l P Q : (P -∗ Q) ∗ P ⊢ Q. Proof. by apply wand_elim_l'. Qed. -Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q. +Lemma wand_elim_r P Q : P ∗ (P -∗ Q) ⊢ Q. Proof. rewrite (comm _ P); apply wand_elim_l. Qed. -Lemma wand_elim_r' P Q R : (Q ⊢ P -★ R) → P ★ Q ⊢ R. +Lemma wand_elim_r' P Q R : (Q ⊢ P -∗ R) → P ∗ Q ⊢ R. Proof. intros ->; apply wand_elim_r. Qed. -Lemma wand_apply P Q R S : (P ⊢ Q -★ R) → (S ⊢ P ★ Q) → S ⊢ R. +Lemma wand_apply P Q R S : (P ⊢ Q -∗ R) → (S ⊢ P ∗ Q) → S ⊢ R. Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed. -Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R. +Lemma wand_frame_l P Q R : (Q -∗ R) ⊢ P ∗ Q -∗ P ∗ R. Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed. -Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P. +Lemma wand_frame_r P Q R : (Q -∗ R) ⊢ Q ∗ P -∗ R ∗ P. Proof. - apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc. + apply wand_intro_l. rewrite ![(_ ∗ P)%I]comm -assoc. apply sep_mono_r, wand_elim_r. Qed. -Lemma wand_diag P : (P -★ P) ⊣⊢ True. +Lemma wand_diag P : (P -∗ P) ⊣⊢ True. Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed. -Lemma wand_True P : (True -★ P) ⊣⊢ P. +Lemma wand_True P : (True -∗ P) ⊣⊢ P. Proof. apply (anti_symm _); last by auto using wand_intro_l. eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r. Qed. -Lemma wand_entails P Q : (True ⊢ P -★ Q) → P ⊢ Q. +Lemma wand_entails P Q : (True ⊢ P -∗ Q) → P ⊢ Q. Proof. intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r. Qed. -Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ P -★ Q. +Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ P -∗ Q. Proof. auto using wand_intro_l. Qed. -Lemma wand_curry P Q R : (P -★ Q -★ R) ⊣⊢ (P ★ Q -★ R). +Lemma wand_curry P Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R). Proof. apply (anti_symm _). - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r. - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r. Qed. -Lemma sep_and P Q : (P ★ Q) ⊢ (P ∧ Q). +Lemma sep_and P Q : (P ∗ Q) ⊢ (P ∧ Q). Proof. auto. Qed. -Lemma impl_wand P Q : (P → Q) ⊢ P -★ Q. +Lemma impl_wand P Q : (P → Q) ⊢ P -∗ Q. Proof. apply wand_intro_r, impl_elim with P; auto. Qed. -Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ■ φ ★ Q ⊢ R. +Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ■ φ ∗ Q ⊢ R. Proof. intros; apply pure_elim with φ; eauto. Qed. -Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ★ ■ φ ⊢ R. +Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ∗ ■ φ ⊢ R. Proof. intros; apply pure_elim with φ; eauto. Qed. Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M). @@ -395,29 +395,29 @@ Proof. intros P; apply (anti_symm _); auto. Qed. Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M). Proof. intros P; apply (anti_symm _); auto. Qed. -Lemma sep_and_l P Q R : P ★ (Q ∧ R) ⊢ (P ★ Q) ∧ (P ★ R). +Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R). Proof. auto. Qed. -Lemma sep_and_r P Q R : (P ∧ Q) ★ R ⊢ (P ★ R) ∧ (Q ★ R). +Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R). Proof. auto. Qed. -Lemma sep_or_l P Q R : P ★ (Q ∨ R) ⊣⊢ (P ★ Q) ∨ (P ★ R). +Lemma sep_or_l P Q R : P ∗ (Q ∨ R) ⊣⊢ (P ∗ Q) ∨ (P ∗ R). Proof. apply (anti_symm (⊢)); last by eauto 8. apply wand_elim_r', or_elim; apply wand_intro_l; auto. Qed. -Lemma sep_or_r P Q R : (P ∨ Q) ★ R ⊣⊢ (P ★ R) ∨ (Q ★ R). +Lemma sep_or_r P Q R : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R). Proof. by rewrite -!(comm _ R) sep_or_l. Qed. -Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ★ (∃ a, Ψ a) ⊣⊢ ∃ a, P ★ Ψ a. +Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ∗ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∗ Ψ a. Proof. intros; apply (anti_symm (⊢)). - apply wand_elim_r', exist_elim=>a. apply wand_intro_l. by rewrite -(exist_intro a). - apply exist_elim=> a; apply sep_mono; auto using exist_intro. Qed. -Lemma sep_exist_r {A} (Φ: A → uPred M) Q: (∃ a, Φ a) ★ Q ⊣⊢ ∃ a, Φ a ★ Q. +Lemma sep_exist_r {A} (Φ: A → uPred M) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q. Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed. -Lemma sep_forall_l {A} P (Ψ : A → uPred M) : P ★ (∀ a, Ψ a) ⊢ ∀ a, P ★ Ψ a. +Lemma sep_forall_l {A} P (Ψ : A → uPred M) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a. Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. -Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ★ Q ⊢ ∀ a, Φ a ★ Q. +Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q. Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. (* Always derived *) @@ -460,28 +460,28 @@ Proof. rewrite -(internal_eq_refl a) always_pure; auto. Qed. -Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ★ Q). +Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q). Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed. -Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ★ Q. +Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q. Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed. -Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ★ □ Q. +Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q. Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed. -Lemma always_sep P Q : □ (P ★ Q) ⊣⊢ □ P ★ □ Q. +Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q. Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed. -Lemma always_sep_dup' P : □ P ⊣⊢ □ P ★ □ P. +Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P. Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed. -Lemma always_wand P Q : □ (P -★ Q) ⊢ □ P -★ □ Q. +Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q. Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed. -Lemma always_wand_impl P Q : □ (P -★ Q) ⊣⊢ □ (P → Q). +Lemma always_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q). Proof. apply (anti_symm (⊢)); [|by rewrite -impl_wand]. apply always_intro', impl_intro_r. by rewrite always_and_sep_l' always_elim wand_elim_l. Qed. -Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P. +Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P. Proof. intros; rewrite -always_and_sep_l'; auto. Qed. -Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ★ □ Q. +Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q. Proof. intros; rewrite -always_and_sep_r'; auto. Qed. (* Later derived *) @@ -520,7 +520,7 @@ Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q. Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed. Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q. Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed. -Lemma later_wand P Q : ▷ (P -★ Q) ⊢ ▷ P -★ ▷ Q. +Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q. Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed. Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q. Proof. by rewrite /uPred_iff later_and !later_impl. Qed. @@ -547,7 +547,7 @@ Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q. Proof. destruct p; simpl; auto using always_or. Qed. Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a. Proof. destruct p; simpl; auto using always_exist. Qed. -Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ □?p P ★ □?p Q. +Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q. Proof. destruct p; simpl; auto using always_sep. Qed. Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P. Proof. destruct p; simpl; auto using always_later. Qed. @@ -577,7 +577,7 @@ Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q. Proof. rewrite /uPred_except_0. apply (anti_symm _); auto. Qed. Lemma except_0_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q. Proof. by rewrite /uPred_except_0 or_and_l. Qed. -Lemma except_0_sep P Q : ◇ (P ★ Q) ⊣⊢ ◇ P ★ ◇ Q. +Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q. Proof. rewrite /uPred_except_0. apply (anti_symm _). - apply or_elim; last by auto. @@ -594,9 +594,9 @@ Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P. Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed. Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P. Proof. destruct p; simpl; auto using except_0_always. Qed. -Lemma except_0_frame_l P Q : P ★ ◇ Q ⊢ ◇ (P ★ Q). +Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q). Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed. -Lemma except_0_frame_r P Q : ◇ P ★ Q ⊢ ◇ (P ★ Q). +Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q). Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed. (* Own and valid derived *) @@ -622,13 +622,13 @@ Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. -Lemma bupd_frame_l R Q : (R ★ |==> Q) ==★ R ★ Q. +Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q. Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed. -Lemma bupd_wand_l P Q : (P -★ Q) ★ (|==> P) ==★ Q. +Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ==∗ Q. Proof. by rewrite bupd_frame_l wand_elim_l. Qed. -Lemma bupd_wand_r P Q : (|==> P) ★ (P -★ Q) ==★ Q. +Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ==∗ Q. Proof. by rewrite bupd_frame_r wand_elim_r. Qed. -Lemma bupd_sep P Q : (|==> P) ★ (|==> Q) ==★ P ★ Q. +Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q. Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed. Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y. Proof. @@ -661,9 +661,9 @@ Proof. rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto. by rewrite assoc (comm _ _ P) -assoc !impl_elim_r. Qed. -Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q). +Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∗ Q). Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed. -Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q). +Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -∗ Q). Proof. rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle. apply or_mono, wand_intro_l; first done. @@ -715,7 +715,7 @@ Global Instance or_persistent P Q : PersistentP P → PersistentP Q → PersistentP (P ∨ Q). Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed. Global Instance sep_persistent P Q : - PersistentP P → PersistentP Q → PersistentP (P ★ Q). + PersistentP P → PersistentP Q → PersistentP (P ∗ Q). Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed. Global Instance forall_persistent {A} (Ψ : A → uPred M) : (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x). @@ -744,15 +744,15 @@ Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P. Proof. destruct p; simpl; auto using always_always. Qed. Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q. Proof. rewrite -(always_always P); apply always_intro'. Qed. -Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ★ Q. +Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q. Proof. by rewrite -(always_always P) always_and_sep_l'. Qed. -Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ★ Q. +Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q. Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed. -Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ★ P. +Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ∗ P. Proof. by rewrite -(always_always P) -always_sep_dup'. Qed. -Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ★ P. +Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P. Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed. -Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q. +Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q. Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed. End derived. End uPred_derived. diff --git a/base_logic/double_negation.v b/base_logic/double_negation.v index 123d5b83164d7215b95cf40426105133fe933694..e73d0d078b5527b42375e43f06413deb1f88d96b 100644 --- a/base_logic/double_negation.v +++ b/base_logic/double_negation.v @@ -13,14 +13,14 @@ Notation "▷^ n P" := (uPred_laterN n P) format "▷^ n P") : uPred_scope. Definition uPred_nnupd {M} (P: uPred M) : uPred M := - ∀ n, (P -★ ▷^n False) -★ ▷^n False. + ∀ n, (P -∗ ▷^n False) -∗ ▷^n False. Notation "|=n=> Q" := (uPred_nnupd Q) (at level 99, Q at level 200, format "|=n=> Q") : uPred_scope. Notation "P =n=> Q" := (P ⊢ |=n=> Q) (at level 99, Q at level 200, only parsing) : C_scope. -Notation "P =n=★ Q" := (P -★ |=n=> Q)%I - (at level 99, Q at level 200, format "P =n=★ Q") : uPred_scope. +Notation "P =n=∗ Q" := (P -∗ |=n=> Q)%I + (at level 99, Q at level 200, format "P =n=∗ Q") : uPred_scope. (* Our goal is to prove that: (1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris @@ -62,9 +62,9 @@ Qed. are used throughout Iris hold for nnupd. In fact, the first three properties that follow hold for any - modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation + modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation here is slightly different, because nnupd is of the form - ∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly. + ∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly. *) @@ -77,7 +77,7 @@ Proof. rewrite /uPred_nnupd (forall_elim n). apply wand_elim_r. Qed. -Lemma nnupd_frame_r P R : (|=n=> P) ★ R =n=> P ★ R. +Lemma nnupd_frame_r P R : (|=n=> P) ∗ R =n=> P ∗ R. Proof. apply forall_intro=>n. apply wand_intro_r. rewrite (comm _ P) -wand_curry. @@ -106,7 +106,7 @@ Qed. (* However, the transitivity property seems to be much harder to prove. This is surprising, because transitivity does hold for - modalities of the form (- -★ Q) -★ Q. What goes wrong when we quantify + modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify now over n? *) @@ -115,7 +115,7 @@ Proof. rewrite /uPred_nnupd. apply forall_intro=>a. apply wand_intro_l. rewrite (forall_elim a). - rewrite (nnupd_intro (P -★ _)). + rewrite (nnupd_intro (P -∗ _)). rewrite /uPred_nnupd. (* Oops -- the exponents of the later modality don't match up! *) Abort. @@ -123,9 +123,9 @@ Abort. (* Instead, we will need to prove this in the model. We start by showing that nnupd is the limit of a the following sequence: - (- -★ False) - ★ False, - (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, - (- -★ ▷^2 False) - ★ ▷^2 False ∧ (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, + (- -∗ False) - ∗ False, + (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False, + (- -∗ ▷^2 False) - ∗ ▷^2 False ∧ (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False, ... Then, it is easy enough to show that each of the uPreds in this sequence @@ -134,7 +134,7 @@ Abort. (* The definition of the sequence above: *) Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M := - ((P -★ ▷^k False) -★ ▷^k False) ∧ + ((P -∗ ▷^k False) -∗ ▷^k False) ∧ match k with O => True | S k' => uPred_nnupd_k k' P @@ -155,7 +155,7 @@ Proof. rewrite (forall_elim (S k)) //=. Qed. -Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ★ (P -★ (▷^n False)) ⊢ (▷^n False))%I. +Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ∗ (P -∗ (▷^n False)) ⊢ (▷^n False))%I. Proof. induction k. - inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l. @@ -165,10 +165,10 @@ Proof. Qed. Lemma nnupd_k_unfold k P: - (|=n=>_(S k) P) ⊣⊢ ((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P). + (|=n=>_(S k) P) ⊣⊢ ((P -∗ (▷^(S k) False)) -∗ (▷^(S k) False)) ∧ (|=n=>_k P). Proof. done. Qed. Lemma nnupd_k_unfold' k P n x: - (|=n=>_(S k) P)%I n x ↔ (((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x. + (|=n=>_(S k) P)%I n x ↔ (((P -∗ (▷^(S k) False)) -∗ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x. Proof. done. Qed. Lemma nnupd_k_weaken k P: (|=n=>_(S k) P) ⊢ |=n=>_k P. @@ -238,13 +238,13 @@ Proof. revert P. induction k; intros P. - rewrite //= ?right_id. apply wand_intro_l. - rewrite {1}(nnupd_k_intro 0 (P -★ False)%I) //= ?right_id. apply wand_elim_r. + rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r. - rewrite {2}(nnupd_k_unfold k P). apply and_intro. * rewrite (nnupd_k_unfold k P). rewrite and_elim_l. rewrite nnupd_k_unfold. rewrite and_elim_l. apply wand_intro_l. - rewrite {1}(nnupd_k_intro (S k) (P -★ ▷^(S k) (False)%I)). + rewrite {1}(nnupd_k_intro (S k) (P -∗ ▷^(S k) (False)%I)). rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r. * do 2 rewrite nnupd_k_weaken //. Qed. diff --git a/base_logic/lib/auth.v b/base_logic/lib/auth.v index fd0ab02fabbd9b4e2ce1f34b90aa466292f5be39..4e7e758397fd1fbdcca9ee46580f565fc14de1d9 100644 --- a/base_logic/lib/auth.v +++ b/base_logic/lib/auth.v @@ -21,7 +21,7 @@ Section definitions. Definition auth_own (a : A) : iProp Σ := own γ (◯ a). Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ := - (∃ t, own γ (● f t) ★ φ t)%I. + (∃ t, own γ (● f t) ∗ φ t)%I. Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ := inv N (auth_inv f φ). @@ -69,7 +69,7 @@ Section auth. Implicit Types t u : T. Implicit Types γ : gname. - Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b. + Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ∗ auth_own γ b. Proof. by rewrite /auth_own -own_op auth_frag_op. Qed. Global Instance from_sep_auth_own γ a b1 b2 : @@ -92,7 +92,7 @@ Section auth. Proof. intros a1 a2. apply auth_own_mono. Qed. Lemma auth_alloc_strong N E t (G : gset gname) : - ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). + ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. iIntros (?) "Hφ". rewrite /auth_own /auth_ctx. iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done. @@ -103,19 +103,19 @@ Section auth. Qed. Lemma auth_alloc N E t : - ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). + ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. iIntros (?) "Hφ". iMod (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto. Qed. - Lemma auth_empty γ : True ==★ auth_own γ ∅. + Lemma auth_empty γ : True ==∗ auth_own γ ∅. Proof. by rewrite /auth_own -own_empty. Qed. Lemma auth_acc E γ a : - ▷ auth_inv γ f φ ★ auth_own γ a ={E}=★ ∃ t, - ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, - ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b. + ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t, + ■ (a ≼ f t) ∗ ▷ φ t ∗ ∀ u b, + ■ ((f t, a) ~l~> (f u, b)) ∗ ▷ φ u ={E}=∗ ▷ auth_inv γ f φ ∗ auth_own γ b. Proof. iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own. iDestruct "Hinv" as (t) "[>Hγa Hφ]". @@ -129,9 +129,9 @@ Section auth. Lemma auth_open E N γ a : nclose N ⊆ E → - auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=★ ∃ t, - ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, - ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b. + auth_ctx γ N f φ ∗ auth_own γ a ={E,E∖N}=∗ ∃ t, + ■ (a ≼ f t) ∗ ▷ φ t ∗ ∀ u b, + ■ ((f t, a) ~l~> (f u, b)) ∗ ▷ φ u ={E∖N,E}=∗ auth_own γ b. Proof. iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose". (* The following is essentially a very trivial composition of the accessors diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v index a55d1c8a994617f53fa854a6ca8bf5f2210e64f2..6079a03e4943b601e48d54ba6e52007e5045ccf0 100644 --- a/base_logic/lib/boxes.v +++ b/base_logic/lib/boxes.v @@ -22,15 +22,15 @@ Section box_defs. own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))). Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ := - (∃ b, box_own_auth γ (● Excl' b) ★ box_own_prop γ P ★ if b then P else True)%I. + (∃ b, box_own_auth γ (● Excl' b) ∗ box_own_prop γ P ∗ if b then P else True)%I. Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ := inv N (slice_inv γ P). Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ := (∃ Φ : slice_name → iProp Σ, - ▷ (P ≡ [★ map] γ ↦ b ∈ f, Φ γ) ★ - [★ map] γ ↦ b ∈ f, box_own_auth γ (◯ Excl' b) ★ box_own_prop γ (Φ γ) ★ + ▷ (P ≡ [∗ map] γ ↦ b ∈ f, Φ γ) ∗ + [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯ Excl' b) ∗ box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I. End box_defs. @@ -55,22 +55,22 @@ Global Instance slice_persistent γ P : PersistentP (slice N γ P). Proof. apply _. Qed. Lemma box_own_auth_agree γ b1 b2 : - box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2. + box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2. Proof. rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_l. by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete. Qed. Lemma box_own_auth_update γ b1 b2 b3 : - box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) - ==★ box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3). + box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) + ==∗ box_own_auth γ (● Excl' b3) ∗ box_own_auth γ (◯ Excl' b3). Proof. rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done. by apply auth_update, option_local_update, exclusive_local_update. Qed. Lemma box_own_agree γ Q1 Q2 : - (box_own_prop γ Q1 ★ box_own_prop γ Q2) ⊢ ▷ (Q1 ≡ Q2). + (box_own_prop γ Q1 ∗ box_own_prop γ Q2) ⊢ ▷ (Q1 ≡ Q2). Proof. rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r. rewrite option_validI /= agree_validI agree_equivI later_equivI /=. @@ -86,8 +86,8 @@ Proof. Qed. Lemma box_insert f P Q : - ▷ box N f P ={N}=★ ∃ γ, f !! γ = None ★ - slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). + ▷ box N f P ={N}=∗ ∃ γ, f !! γ = None ∗ + slice N γ Q ∗ ▷ box N (<[γ:=false]> f) (Q ∗ P). Proof. iDestruct 1 as (Φ) "[#HeqP Hf]". iMod (own_alloc_strong (● Excl' false ⋅ ◯ Excl' false, @@ -100,17 +100,17 @@ Proof. iModIntro; iExists γ; repeat iSplit; auto. iNext. iExists (<[γ:=Q]> Φ); iSplit. - iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'. - - rewrite (big_sepM_fn_insert (λ _ _ P', _ ★ _ _ P' ★ _ _ (_ _ P')))%I //. + - rewrite (big_sepM_fn_insert (λ _ _ P', _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //. iFrame; eauto. Qed. Lemma box_delete f P Q γ : f !! γ = Some false → - slice N γ Q ★ ▷ box N f P ={N}=★ ∃ P', - ▷ ▷ (P ≡ (Q ★ P')) ★ ▷ box N (delete γ f) P'. + slice N γ Q ∗ ▷ box N f P ={N}=∗ ∃ P', + ▷ ▷ (P ≡ (Q ∗ P')) ∗ ▷ box N (delete γ f) P'. Proof. iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". - iExists ([★ map] γ'↦_ ∈ delete γ f, Φ γ')%I. + iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I. iInv N as (b) "(Hγ & #HγQ &_)" "Hclose". iApply fupd_trans_frame; iFrame "Hclose"; iModIntro; iNext. iDestruct (big_sepM_delete _ f _ false with "Hf") @@ -125,7 +125,7 @@ Qed. Lemma box_fill f γ P Q : f !! γ = Some false → - slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=★ ▷ box N (<[γ:=true]> f) P. + slice N γ Q ∗ ▷ Q ∗ ▷ box N f P ={N}=∗ ▷ box N (<[γ:=true]> f) P. Proof. iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]". iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose". @@ -143,7 +143,7 @@ Qed. Lemma box_empty f P Q γ : f !! γ = Some true → - slice N γ Q ★ ▷ box N f P ={N}=★ ▷ Q ★ ▷ box N (<[γ:=false]> f) P. + slice N γ Q ∗ ▷ box N f P ={N}=∗ ▷ Q ∗ ▷ box N (<[γ:=false]> f) P. Proof. iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose". @@ -160,7 +160,7 @@ Proof. iFrame; eauto. Qed. -Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=★ box N (const true <\$> f) P. +Lemma box_fill_all f P Q : box N f P ∗ ▷ P ={N}=∗ box N (const true <\$> f) P. Proof. iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iExists Φ; iSplitR; first by rewrite big_sepM_fmap. @@ -177,11 +177,11 @@ Qed. Lemma box_empty_all f P Q : map_Forall (λ _, (true =)) f → - box N f P ={N}=★ ▷ P ★ box N (const false <\$> f) P. + box N f P ={N}=∗ ▷ P ∗ box N (const false <\$> f) P. Proof. iDestruct 1 as (Φ) "[#HeqP Hf]". - iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★ - box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]". + iAssert ([∗ map] γ↦b ∈ f, ▷ Φ γ ∗ box_own_auth γ (◯ Excl' false) ∗ + box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]". { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf". iAlways; iIntros (γ b ?) "(Hγ' & #\$ & #\$)". assert (true = b) as <- by eauto. diff --git a/base_logic/lib/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v index 1cbdefa77769f0dc45d9edd2da1025993578f343..4c618527be796ba54b1b2dea4007b8f5c6bcf3c9 100644 --- a/base_logic/lib/cancelable_invariants.v +++ b/base_logic/lib/cancelable_invariants.v @@ -32,19 +32,19 @@ Section proofs. Proof. rewrite /cinv; apply _. Qed. Lemma cinv_own_op γ q1 q2 : - cinv_own γ q1 ★ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2). + cinv_own γ q1 ∗ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2). Proof. by rewrite /cinv_own own_op. Qed. - Lemma cinv_own_half γ q : cinv_own γ (q/2) ★ cinv_own γ (q/2) ⊣⊢ cinv_own γ q. + Lemma cinv_own_half γ q : cinv_own γ (q/2) ∗ cinv_own γ (q/2) ⊣⊢ cinv_own γ q. Proof. by rewrite cinv_own_op Qp_div_2. Qed. - Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ★ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp. + Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ∗ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp. Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed. - Lemma cinv_own_1_l γ q : cinv_own γ 1 ★ cinv_own γ q ⊢ False. + Lemma cinv_own_1_l γ q : cinv_own γ 1 ∗ cinv_own γ q ⊢ False. Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed. - Lemma cinv_alloc E N P : ▷ P ={E}=★ ∃ γ, cinv N γ P ★ cinv_own γ 1. + Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1. Proof. rewrite /cinv /cinv_own. iIntros "HP". iMod (own_alloc 1%Qp) as (γ) "H1"; first done. @@ -52,7 +52,7 @@ Section proofs. Qed. Lemma cinv_cancel E N γ P : - nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=★ ▷ P. + nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=∗ ▷ P. Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto. @@ -61,7 +61,7 @@ Section proofs. Lemma cinv_open E N γ p P : nclose N ⊆ E → - cinv N γ P ⊢ cinv_own γ p ={E,E∖N}=★ ▷ P ★ cinv_own γ p ★ (▷ P ={E∖N,E}=★ True). + cinv N γ P ⊢ cinv_own γ p ={E,E∖N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖N,E}=∗ True). Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose". diff --git a/base_logic/lib/counter_examples.v b/base_logic/lib/counter_examples.v index 5ea06663330915152d6f25361124af35384fff25..a70bb01e7d697fabf3a1d3f9c7fd289816178758 100644 --- a/base_logic/lib/counter_examples.v +++ b/base_logic/lib/counter_examples.v @@ -13,13 +13,13 @@ Module savedprop. Section savedprop. Context (sprop : Type) (saved : sprop → iProp → iProp). Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P). Hypothesis sprop_alloc_dep : - ∀ (P : sprop → iProp), True ==★ (∃ i, saved i (P i)). + ∀ (P : sprop → iProp), True ==∗ (∃ i, saved i (P i)). Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q). (** A bad recursive reference: "Assertion with name [i] does not hold" *) - Definition A (i : sprop) : iProp := ∃ P, ¬ P ★ saved i P. + Definition A (i : sprop) : iProp := ∃ P, ¬ P ∗ saved i P. - Lemma A_alloc : True ==★ ∃ i, saved i (A i). + Lemma A_alloc : True ==∗ ∃ i, saved i (A i). Proof. by apply sprop_alloc_dep. Qed. Lemma saved_NA i : saved i (A i) ⊢ ¬ A i. @@ -63,7 +63,7 @@ Module inv. Section inv. Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P. Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q. Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P. - Hypothesis fupd_frame_l : ∀ E P Q, P ★ fupd E Q ⊢ fupd E (P ★ Q). + Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q). Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P. (** We have invariants *) @@ -71,7 +71,7 @@ Module inv. Section inv. Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P). Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P). Hypothesis inv_open : - ∀ i P Q R, (P ★ Q ⊢ fupd M0 (P ★ R)) → (inv i P ★ Q ⊢ fupd M1 R). + ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R). (* We have tokens for a little "two-state STS": [start] -> [finish]. state. [start] also asserts the exact state; it is only ever owned by the @@ -88,15 +88,15 @@ Module inv. Section inv. Hypothesis sts_alloc : True ⊢ fupd M0 (∃ γ, start γ). Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ). - Hypothesis finished_not_start : ∀ γ, start γ ★ finished γ ⊢ False. + Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False. - Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ. + Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ. (** We assume that we cannot update to false. *) Hypothesis consistency : ¬ (True ⊢ fupd M1 False). (** Some general lemmas and proof mode compatibility. *) - Lemma inv_open' i P R : inv i P ★ (P -★ fupd M0 (P ★ fupd M1 R)) ⊢ fupd M1 R. + Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R. Proof. iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first. { iSplit; first done. iExact "HP". } @@ -110,7 +110,7 @@ Module inv. Section inv. intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono. Qed. - Lemma fupd_frame_r E P Q : (fupd E P ★ Q) ⊢ fupd E (P ★ Q). + Lemma fupd_frame_r E P Q : (fupd E P ∗ Q) ⊢ fupd E (P ∗ Q). Proof. by rewrite comm fupd_frame_l comm. Qed. Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q). @@ -130,18 +130,18 @@ Module inv. Section inv. (** Now to the actual counterexample. We start with a weird form of saved propositions. *) Definition saved (γ : gname) (P : iProp) : iProp := - ∃ i, inv i (start γ ∨ (finished γ ★ □ P)). + ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)). Global Instance saved_persistent γ P : PersistentP (saved γ P) := _. Lemma saved_alloc (P : gname → iProp) : True ⊢ fupd M1 (∃ γ, saved γ (P γ)). Proof. iIntros "". iMod (sts_alloc) as (γ) "Hs". - iMod (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi". + iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi". { auto. } iApply fupd_intro. by iExists γ, i. Qed. - Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ fupd M1 (□ Q). + Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q). Proof. iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". iApply (inv_open' i). iSplit; first done. @@ -162,8 +162,8 @@ Module inv. Section inv. Qed. (** And now we tie a bad knot. *) - Notation "¬ P" := (□ (P -★ fupd M1 False))%I : uPred_scope. - Definition A i : iProp := ∃ P, ¬P ★ saved i P. + Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope. + Definition A i : iProp := ∃ P, ¬P ∗ saved i P. Global Instance A_persistent i : PersistentP (A i) := _. Lemma A_alloc : True ⊢ fupd M1 (∃ i, saved i (A i)). diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v index ba0c131ac78032d31e2ed6195d10b25e62bb488f..87a5bb15ade78392a833c4e1e1ba208fbf5a6b36 100644 --- a/base_logic/lib/fancy_updates.v +++ b/base_logic/lib/fancy_updates.v @@ -9,7 +9,7 @@ Import uPred. Program Definition fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ := - (wsat ★ ownE E1 ==★ ◇ (wsat ★ ownE E2 ★ P))%I. + (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I. Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed. Definition fupd := proj1_sig fupd_aux. Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux. @@ -19,19 +19,19 @@ Instance: Params (@fupd) 4. Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) (at level 99, E1, E2 at level 50, Q at level 200, format "|={ E1 , E2 }=> Q") : uPred_scope. -Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I +Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I (at level 99, E1,E2 at level 50, Q at level 200, - format "P ={ E1 , E2 }=★ Q") : uPred_scope. -Notation "P ={ E1 , E2 }=★ Q" := (P ⊢ |={E1,E2}=> Q) + format "P ={ E1 , E2 }=∗ Q") : uPred_scope. +Notation "P ={ E1 , E2 }=∗ Q" := (P ⊢ |={E1,E2}=> Q) (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope. Notation "|={ E }=> Q" := (fupd E E Q) (at level 99, E at level 50, Q at level 200, format "|={ E }=> Q") : uPred_scope. -Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I +Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I (at level 99, E at level 50, Q at level 200, - format "P ={ E }=★ Q") : uPred_scope. -Notation "P ={ E }=★ Q" := (P ⊢ |={E}=> Q) + format "P ={ E }=∗ Q") : uPred_scope. +Notation "P ={ E }=∗ Q" := (P ⊢ |={E}=> Q) (at level 99, E at level 50, Q at level 200, only parsing) : C_scope. Section fupd. @@ -50,26 +50,26 @@ Proof. by iIntros "\$ (\$ & \$ & HE) !> !> [\$ \$] !> !>" . Qed. -Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=★ P. +Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P. Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed. -Lemma bupd_fupd E P : (|==> P) ={E}=★ P. +Lemma bupd_fupd E P : (|==> P) ={E}=∗ P. Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [\$ \$] !> !>". Qed. -Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=★ Q. +Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=∗ Q. Proof. rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP". Qed. -Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=★ P. +Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=∗ P. Proof. rewrite fupd_eq /fupd_def. iIntros "HP HwE". iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame. Qed. Lemma fupd_mask_frame_r' E1 E2 Ef P : - E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=★ P. + E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P. Proof. intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)". iMod ("Hvs" with "[Hw HE1]") as ">(\$ & HE2 & HP)"; first by iFrame. @@ -77,7 +77,7 @@ Proof. iIntros "!> !>". by iApply "HP". Qed. -Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q. +Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q. Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP \$]". Qed. (** * Derived rules *) @@ -87,50 +87,50 @@ Global Instance fupd_flip_mono' E1 E2 : Proper (flip (⊢) ==> flip (⊢)) (@fupd Σ _ E1 E2). Proof. intros P Q; apply fupd_mono. Qed. -Lemma fupd_intro E P : P ={E}=★ P. +Lemma fupd_intro E P : P ={E}=∗ P. Proof. iIntros "HP". by iApply bupd_fupd. Qed. Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True. Proof. exact: fupd_intro_mask. Qed. -Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=★ P. +Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P. Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed. -Lemma fupd_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=★ P ★ Q. +Lemma fupd_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ={E1,E2}=∗ P ∗ Q. Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed. -Lemma fupd_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=★ Q. +Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q. Proof. by rewrite fupd_frame_l wand_elim_l. Qed. -Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=★ Q. +Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q. Proof. by rewrite fupd_frame_r wand_elim_r. Qed. Lemma fupd_trans_frame E1 E2 E3 P Q : - ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=★ P. + ((Q ={E2,E3}=∗ True) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P. Proof. rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r. by rewrite fupd_frame_r left_id fupd_trans. Qed. Lemma fupd_mask_frame_r E1 E2 Ef P : - E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=★ P. + E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P. Proof. iIntros (?) "H". iApply fupd_mask_frame_r'; auto. iApply fupd_wand_r; iFrame "H"; eauto. Qed. -Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=★ P. +Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=∗ P. Proof. intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r. Qed. -Lemma fupd_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=★ P ★ Q. +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. Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) : - ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=★ [★ map] k↦x ∈ m, Φ k x. + ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x. Proof. - apply (big_opM_forall (λ P Q, P ={E}=★ Q)); auto using fupd_intro. + apply (big_opM_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep. Qed. Lemma fupd_big_sepS `{Countable A} E (Φ : A → iProp Σ) X : - ([★ set] x ∈ X, |={E}=> Φ x) ={E}=★ [★ set] x ∈ X, Φ x. + ([∗ set] x ∈ X, |={E}=> Φ x) ={E}=∗ [∗ set] x ∈ X, Φ x. Proof. - apply (big_opS_forall (λ P Q, P ={E}=★ Q)); auto using fupd_intro. + apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep. Qed. End fupd. @@ -193,15 +193,15 @@ Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) => Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> (▷ |={E2,E1}=> Q))%I (at level 99, E1, E2 at level 50, Q at level 200, format "|={ E1 , E2 }▷=> Q") : uPred_scope. -Notation "P ={ E1 , E2 }▷=★ Q" := (P -★ |={ E1 , E2 }▷=> Q)%I +Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I (at level 99, E1, E2 at level 50, Q at level 200, - format "P ={ E1 , E2 }▷=★ Q") : uPred_scope. + format "P ={ E1 , E2 }▷=∗ Q") : uPred_scope. Notation "|={ E }▷=> Q" := (|={E,E}▷=> Q)%I (at level 99, E at level 50, Q at level 200, format "|={ E }▷=> Q") : uPred_scope. -Notation "P ={ E }▷=★ Q" := (P ={E,E}▷=★ Q)%I +Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I (at level 99, E at level 50, Q at level 200, - format "P ={ E }▷=★ Q") : uPred_scope. + format "P ={ E }▷=∗ Q") : uPred_scope. Section step_fupd. Context `{invG Σ}. diff --git a/base_logic/lib/invariants.v b/base_logic/lib/invariants.v index 727a8b65998af0bf05be9c6c2cafd9fff12c8091..4fd9016fa1256379955df8c8da6cd80b63b01930 100644 --- a/base_logic/lib/invariants.v +++ b/base_logic/lib/invariants.v @@ -27,7 +27,7 @@ Qed. Global Instance inv_persistent N P : PersistentP (inv N P). Proof. rewrite inv_eq /inv; apply _. Qed. -Lemma inv_alloc N E P : ▷ P ={E}=★ inv N P. +Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P. Proof. rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw \$]". iMod (ownI_alloc (∈ nclose N) P with "[HP Hw]") as (i) "(% & \$ & ?)"; auto. @@ -41,7 +41,7 @@ Proof. Qed. Lemma inv_open E N P : - nclose N ⊆ E → inv N P ={E,E∖N}=★ ▷ P ★ (▷ P ={E∖N,E}=★ True). + nclose N ⊆ E → inv N P ={E,E∖N}=∗ ▷ P ∗ (▷ P ={E∖N,E}=∗ True). Proof. rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]". iDestruct "Hi" as % ?%elem_of_subseteq_singleton. @@ -53,7 +53,7 @@ Proof. Qed. Lemma inv_open_timeless E N P `{!TimelessP P} : - nclose N ⊆ E → inv N P ={E,E∖N}=★ P ★ (P ={E∖N,E}=★ True). + nclose N ⊆ E → inv N P ={E,E∖N}=∗ P ∗ (P ={E∖N,E}=∗ True). Proof. iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto. iIntros "!> {\$HP} HP". iApply "Hclose"; auto. diff --git a/base_logic/lib/own.v b/base_logic/lib/own.v index 1c23162581ad994af74db5e98107cc04c8bfdfa9..d6bde8ab9fe33f57f16c1ea7e3a8ba3e7e447558 100644 --- a/base_logic/lib/own.v +++ b/base_logic/lib/own.v @@ -50,7 +50,7 @@ Proof. rewrite !own_eq. solve_proper. Qed. Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (@own Σ A _ γ) := ne_proper _. -Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2. +Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ∗ own γ a2. Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed. Lemma own_mono γ a1 a2 : a2 ≼ a1 → own γ a1 ⊢ own γ a2. Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed. @@ -68,14 +68,14 @@ Proof. (* implicit arguments differ a bit *) by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf. Qed. -Lemma own_valid_2 γ a1 a2 : own γ a1 ★ own γ a2 ⊢ ✓ (a1 ⋅ a2). +Lemma own_valid_2 γ a1 a2 : own γ a1 ∗ own γ a2 ⊢ ✓ (a1 ⋅ a2). Proof. by rewrite -own_op own_valid. Qed. -Lemma own_valid_3 γ a1 a2 a3 : own γ a1 ★ own γ a2 ★ own γ a3 ⊢ ✓ (a1 ⋅ a2 ⋅ a3). +Lemma own_valid_3 γ a1 a2 a3 : own γ a1 ∗ own γ a2 ∗ own γ a3 ⊢ ✓ (a1 ⋅ a2 ⋅ a3). Proof. by rewrite -!own_op assoc own_valid. Qed. -Lemma own_valid_r γ a : own γ a ⊢ own γ a ★ ✓ a. +Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a. Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed. -Lemma own_valid_l γ a : own γ a ⊢ ✓ a ★ own γ a. +Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a. Proof. by rewrite comm -own_valid_r. Qed. Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a). @@ -87,7 +87,7 @@ Proof. rewrite !own_eq /own_def; apply _. Qed. (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris assertion. However, the map_updateP_alloc does not suffice to show this. *) Lemma own_alloc_strong a (G : gset gname) : - ✓ a → True ==★ ∃ γ, ■ (γ ∉ G) ∧ own γ a. + ✓ a → True ==∗ ∃ γ, ■ (γ ∉ G) ∧ own γ a. Proof. intros Ha. rewrite -(bupd_mono (∃ m, ■ (∃ γ, γ ∉ G ∧ m = iRes_singleton γ a) ∧ uPred_ownM m)%I). @@ -98,14 +98,14 @@ Proof. - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]]. by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id. Qed. -Lemma own_alloc a : ✓ a → True ==★ ∃ γ, own γ a. +Lemma own_alloc a : ✓ a → True ==∗ ∃ γ, own γ a. Proof. intros Ha. rewrite (own_alloc_strong a ∅) //; []. apply bupd_mono, exist_mono=>?. eauto with I. Qed. (** ** Frame preserving updates *) -Lemma own_updateP P γ a : a ~~>: P → own γ a ==★ ∃ a', ■ P a' ∧ own γ a'. +Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ■ P a' ∧ own γ a'. Proof. intros Ha. rewrite !own_eq. rewrite -(bupd_mono (∃ m, ■ (∃ a', m = iRes_singleton γ a' ∧ P a') ∧ uPred_ownM m)%I). @@ -116,16 +116,16 @@ Proof. rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|]. Qed. -Lemma own_update γ a a' : a ~~> a' → own γ a ==★ own γ a'. +Lemma own_update γ a a' : a ~~> a' → own γ a ==∗ own γ a'. Proof. intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP. by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->. Qed. Lemma own_update_2 γ a1 a2 a' : - a1 ⋅ a2 ~~> a' → own γ a1 ★ own γ a2 ==★ own γ a'. + a1 ⋅ a2 ~~> a' → own γ a1 ∗ own γ a2 ==∗ own γ a'. Proof. intros. rewrite -own_op. by apply own_update. Qed. Lemma own_update_3 γ a1 a2 a3 a' : - a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 ★ own γ a2 ★ own γ a3 ==★ own γ a'. + a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 ∗ own γ a2 ∗ own γ a3 ==∗ own γ a'. Proof. intros. rewrite -!own_op assoc. by apply own_update. Qed. End global. @@ -139,7 +139,7 @@ Arguments own_update {_ _} [_] _ _ _ _. Arguments own_update_2 {_ _} [_] _ _ _ _ _. Arguments own_update_3 {_ _} [_] _ _ _ _ _ _. -Lemma own_empty `{inG Σ (A:ucmraT)} γ : True ==★ own γ ∅. +Lemma own_empty `{inG Σ (A:ucmraT)} γ : True ==∗ own γ ∅. Proof. rewrite ownM_empty !own_eq /own_def. apply bupd_ownM_update, iprod_singleton_update_empty. diff --git a/base_logic/lib/saved_prop.v b/base_logic/lib/saved_prop.v index 0cac08c87a976e87dbcf3f64c450dbca283daff4..63ca7211fc8fd02a0e8537f1349ebe80903d7fc3 100644 --- a/base_logic/lib/saved_prop.v +++ b/base_logic/lib/saved_prop.v @@ -26,14 +26,14 @@ Section saved_prop. Proof. rewrite /saved_prop_own; apply _. Qed. Lemma saved_prop_alloc_strong x (G : gset gname) : - True ==★ ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x. + True ==∗ ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x. Proof. by apply own_alloc_strong. Qed. - Lemma saved_prop_alloc x : True ==★ ∃ γ, saved_prop_own γ x. + Lemma saved_prop_alloc x : True ==∗ ∃ γ, saved_prop_own γ x. Proof. by apply own_alloc. Qed. Lemma saved_prop_agree γ x y : - saved_prop_own γ x ★ saved_prop_own γ y ⊢ ▷ (x ≡ y). + saved_prop_own γ x ∗ saved_prop_own γ y ⊢ ▷ (x ≡ y). Proof. rewrite own_valid_2 agree_validI agree_equivI later_equivI. set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)). diff --git a/base_logic/lib/sts.v b/base_logic/lib/sts.v index 47c79df7eb134b2d998a44925fee933bc3f57ea0..6ba8f98fba41d23b64ab0e227aef8c9d7c435030 100644 --- a/base_logic/lib/sts.v +++ b/base_logic/lib/sts.v @@ -22,7 +22,7 @@ Section definitions. Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iProp Σ := own γ (sts_frag_up s T). Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ := - (∃ s, own γ (sts_auth s ∅) ★ φ s)%I. + (∃ s, own γ (sts_auth s ∅) ∗ φ s)%I. Definition sts_ctx (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ := inv N (sts_inv φ). @@ -68,21 +68,21 @@ Section sts. sts_frag_included. *) Lemma sts_ownS_weaken γ S1 S2 T1 T2 : T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 → - sts_ownS γ S1 T1 ==★ sts_ownS γ S2 T2. + sts_ownS γ S1 T1 ==∗ sts_ownS γ S2 T2. Proof. intros ???. by apply own_update, sts_update_frag. Qed. Lemma sts_own_weaken γ s S T1 T2 : T2 ⊆ T1 → s ∈ S → sts.closed S T2 → - sts_own γ s T1 ==★ sts_ownS γ S T2. + sts_own γ s T1 ==∗ sts_ownS γ S T2. Proof. intros ???. by apply own_update, sts_update_frag_up. Qed. Lemma sts_ownS_op γ S1 S2 T1 T2 : T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 → - sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2). + sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2). Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed. Lemma sts_alloc E N s : - ▷ φ s ={E}=★ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s). + ▷ φ s ={E}=∗ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s). Proof. iIntros "Hφ". rewrite /sts_ctx /sts_own. iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ". @@ -93,9 +93,9 @@ Section sts. Qed. Lemma sts_accS E γ S T : - ▷ sts_inv γ φ ★ sts_ownS γ S T ={E}=★ ∃ s, - ■ (s ∈ S) ★ ▷ φ s ★ ∀ s' T', - ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'. + ▷ sts_inv γ φ ∗ sts_ownS γ S T ={E}=∗ ∃ s, + ■ (s ∈ S) ∗ ▷ φ s ∗ ∀ s' T', + ■ sts.steps (s, T) (s', T') ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'. Proof. iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own. iDestruct "Hinv" as (s) "[>Hγ Hφ]". @@ -111,16 +111,16 @@ Section sts. Qed. Lemma sts_acc E γ s0 T : - ▷ sts_inv γ φ ★ sts_own γ s0 T ={E}=★ ∃ s, - ■ sts.frame_steps T s0 s ★ ▷ φ s ★ ∀ s' T', - ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'. + ▷ sts_inv γ φ ∗ sts_own γ s0 T ={E}=∗ ∃ s, + ■ sts.frame_steps T s0 s ∗ ▷ φ s ∗ ∀ s' T', + ■ sts.steps (s, T) (s', T') ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'. Proof. by apply sts_accS. Qed. Lemma sts_openS E N γ S T : nclose N ⊆ E → - sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=★ ∃ s, - ■ (s ∈ S) ★ ▷ φ s ★ ∀ s' T', - ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'. + sts_ctx γ N φ ∗ sts_ownS γ S T ={E,E∖N}=∗ ∃ s, + ■ (s ∈ S) ∗ ▷ φ s ∗ ∀ s' T', + ■ sts.steps (s, T) (s', T') ∗ ▷ φ s' ={E∖N,E}=∗ sts_own γ s' T'. Proof. iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose". (* The following is essentially a very trivial composition of the accessors @@ -136,8 +136,8 @@ Section sts. Lemma sts_open E N γ s0 T : nclose N ⊆ E → - sts_ctx γ N φ ★ sts_own γ s0 T ={E,E∖N}=★ ∃ s, - ■ (sts.frame_steps T s0 s) ★ ▷ φ s ★ ∀ s' T', - ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'. + sts_ctx γ N φ ∗ sts_own γ s0 T ={E,E∖N}=∗ ∃ s, + ■ (sts.frame_steps T s0 s) ∗ ▷ φ s ∗ ∀ s' T', + ■ (sts.steps (s, T) (s', T')) ∗ ▷ φ s' ={E∖N,E}=∗ sts_own γ s' T'. Proof. by apply sts_openS. Qed. End sts. diff --git a/base_logic/lib/thread_local.v b/base_logic/lib/thread_local.v index be3dca1744eeb0b18b51991c9fded4443ab7206c..7fa268625c07a94e83c3c791c4ed9157499f9839 100644 --- a/base_logic/lib/thread_local.v +++ b/base_logic/lib/thread_local.v @@ -17,7 +17,7 @@ Section defs. Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ := (∃ i, ■ (i ∈ nclose N) ∧ - inv tlN (P ★ own tid (∅, GSet {[i]}) ∨ tl_own tid {[i]}))%I. + inv tlN (P ∗ own tid (∅, GSet {[i]}) ∨ tl_own tid {[i]}))%I. End defs. Instance: Params (@tl_inv) 3. @@ -37,21 +37,21 @@ Section proofs. Global Instance tl_inv_persistent tid N P : PersistentP (tl_inv tid N P). Proof. rewrite /tl_inv; apply _. Qed. - Lemma tl_alloc : True ==★ ∃ tid, tl_own tid ⊤. + Lemma tl_alloc : True ==∗ ∃ tid, tl_own tid ⊤. Proof. by apply own_alloc. Qed. - Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 ★ tl_own tid E2 ⊢ ■ (E1 ⊥ E2). + Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 ∗ tl_own tid E2 ⊢ ■ (E1 ⊥ E2). Proof. rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]). Qed. Lemma tl_own_union tid E1 E2 : - E1 ⊥ E2 → tl_own tid (E1 ∪ E2) ⊣⊢ tl_own tid E1 ★ tl_own tid E2. + E1 ⊥ E2 → tl_own tid (E1 ∪ E2) ⊣⊢ tl_own tid E1 ∗ tl_own tid E2. Proof. intros ?. by rewrite /tl_own -own_op pair_op left_id coPset_disj_union. Qed. - Lemma tl_inv_alloc tid E N P : ▷ P ={E}=★ tl_inv tid N P. + Lemma tl_inv_alloc tid E N P : ▷ P ={E}=∗ tl_inv tid N P. Proof. iIntros "HP". iMod (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty". @@ -71,8 +71,8 @@ Section proofs. Lemma tl_inv_open tid tlE E N P : nclose tlN ⊆ tlE → nclose N ⊆ E → - tl_inv tid N P ⊢ tl_own tid E ={tlE}=★ ▷ P ★ tl_own tid (E ∖ N) ★ - (▷ P ★ tl_own tid (E ∖ N) ={tlE}=★ tl_own tid E). + tl_inv tid N P ⊢ tl_own tid E ={tlE}=∗ ▷ P ∗ tl_own tid (E ∖ N) ∗ + (▷ P ∗ tl_own tid (E ∖ N) ={tlE}=∗ tl_own tid E). Proof. rewrite /tl_inv. iIntros (??) "#Htlinv Htoks". iDestruct "Htlinv" as (i) "[% Hinv]". diff --git a/base_logic/lib/viewshifts.v b/base_logic/lib/viewshifts.v index be4a00ef4d523f3f82f2d6bde76fbbfd971d2c95..4648b12d6d123ca3163f3fae78a4b0bde00a3843 100644 --- a/base_logic/lib/viewshifts.v +++ b/base_logic/lib/viewshifts.v @@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants. From iris.proofmode Require Import tactics. Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ := - (□ (P -★ |={E1,E2}=> Q))%I. + (□ (P -∗ |={E1,E2}=> Q))%I. Arguments vs {_ _} _ _ _%I _%I. Instance: Params (@vs) 4. @@ -56,10 +56,10 @@ Proof. by iIntros "!# HP". Qed. Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q. Proof. iIntros "#HPQ !# HP". by iApply "HPQ". Qed. -Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ★ P ={E1,E2}=> R ★ Q. +Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ∗ P ={E1,E2}=> R ∗ Q. Proof. iIntros "#Hvs !# [\$ HP]". by iApply "Hvs". Qed. -Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ★ R ={E1,E2}=> Q ★ R. +Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q ∗ R. Proof. iIntros "#Hvs !# [HP \$]". by iApply "Hvs". Qed. Lemma vs_mask_frame_r E1 E2 Ef P Q : @@ -69,7 +69,7 @@ Proof. Qed. Lemma vs_inv N E P Q R : - nclose N ⊆ E → inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q) ⊢ P ={E}=> Q. + nclose N ⊆ E → inv N R ∗ (▷ R ∗ P ={E ∖ nclose N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q. Proof. iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose". iMod ("Hvs" with "[HR HP]") as "[? \$]"; first by iFrame. diff --git a/base_logic/lib/wsat.v b/base_logic/lib/wsat.v index 949897352fed4fc33431335d4950f9b41f796ebc..78615f2660da12dec6609192a9cc92acf46cea6e 100644 --- a/base_logic/lib/wsat.v +++ b/base_logic/lib/wsat.v @@ -36,8 +36,8 @@ Instance: Params (@ownD) 3. Definition wsat `{invG Σ} : iProp Σ := (∃ I : gmap positive (iProp Σ), - own invariant_name (● (invariant_unfold <\$> I : gmap _ _)) ★ - [★ map] i ↦ Q ∈ I, ▷ Q ★ ownD {[i]} ∨ ownE {[i]})%I. + own invariant_name (● (invariant_unfold <\$> I : gmap _ _)) ∗ + [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I. Section wsat. Context `{invG Σ}. @@ -52,40 +52,40 @@ Qed. Global Instance ownI_persistent i P : PersistentP (ownI i P). Proof. rewrite /ownI. apply _. Qed. -Lemma ownE_empty : True ==★ ownE ∅. +Lemma ownE_empty : True ==∗ ownE ∅. Proof. by rewrite (own_empty (A:=coPset_disjUR) enabled_name). Qed. -Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2. +Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2. Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed. -Lemma ownE_disjoint E1 E2 : ownE E1 ★ ownE E2 ⊢ E1 ⊥ E2. +Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ E1 ⊥ E2. Proof. rewrite /ownE own_valid_2. by iIntros (?%coPset_disj_valid_op). Qed. -Lemma ownE_op' E1 E2 : E1 ⊥ E2 ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2. +Lemma ownE_op' E1 E2 : E1 ⊥ E2 ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2. Proof. iSplit; [iIntros "[% ?]"; by iApply ownE_op|]. iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?. iSplit; first done. iApply ownE_op; by try iFrame. Qed. -Lemma ownE_singleton_twice i : ownE {[i]} ★ ownE {[i]} ⊢ False. +Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False. Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed. -Lemma ownD_empty : True ==★ ownD ∅. +Lemma ownD_empty : True ==∗ ownD ∅. Proof. by rewrite (own_empty (A:=gset_disjUR _) disabled_name). Qed. -Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2. +Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2. Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed. -Lemma ownD_disjoint E1 E2 : ownD E1 ★ ownD E2 ⊢ E1 ⊥ E2. +Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ E1 ⊥ E2. Proof. rewrite /ownD own_valid_2. by iIntros (?%gset_disj_valid_op). Qed. -Lemma ownD_op' E1 E2 : E1 ⊥ E2 ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2. +Lemma ownD_op' E1 E2 : E1 ⊥ E2 ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2. Proof. iSplit; [iIntros "[% ?]"; by iApply ownD_op|]. iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?. iSplit; first done. iApply ownD_op; by try iFrame. Qed. -Lemma ownD_singleton_twice i : ownD {[i]} ★ ownD {[i]} ⊢ False. +Lemma ownD_singleton_twice i : ownD {[i]} ∗ ownD {[i]} ⊢ False. Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed. Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P : - own invariant_name (● (invariant_unfold <\$> I : gmap _ _)) ★ + own invariant_name (● (invariant_unfold <\$> I : gmap _ _)) ∗ own invariant_name (◯ {[i := invariant_unfold P]}) ⊢ - ∃ Q, I !! i = Some Q ★ ▷ (Q ≡ P). + ∃ Q, I !! i = Some Q ∗ ▷ (Q ≡ P). Proof. rewrite own_valid_2 auth_validI /=. iIntros "[#HI #HvI]". iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI. @@ -101,7 +101,7 @@ Proof. by rewrite agree_equivI uPred.later_equivI iProp_unfold_equivI. Qed. -Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}. +Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}. Proof. rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]". iDestruct (invariant_lookup I i P with "[\$Hw \$Hi]") as (Q) "[% #HPQ]". @@ -111,7 +111,7 @@ Proof. iFrame "HI"; eauto. - iDestruct (ownE_singleton_twice with "[\$HiE \$HiE']") as %[]. Qed. -Lemma ownI_close i P : wsat ★ ownI i P ★ ▷ P ★ ownD {[i]} ⊢ wsat ★ ownE {[i]}. +Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}. Proof. rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]". iDestruct (invariant_lookup with "[\$Hw \$Hi]") as (Q) "[% #HPQ]". @@ -123,7 +123,7 @@ Qed. Lemma ownI_alloc φ P : (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) → - wsat ★ ▷ P ==★ ∃ i, ■ (φ i) ★ wsat ★ ownI i P. + wsat ∗ ▷ P ==∗ ∃ i, ■ (φ i) ∗ wsat ∗ ownI i P. Proof. iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]". iMod (own_empty (A:=gset_disjUR positive) disabled_name) as "HE". diff --git a/base_logic/primitive.v b/base_logic/primitive.v index 2850a5921863988d47bda4ee52238d4335c8606f..6e9655d7c95b0e37690a22f4ce07c60045057c2f 100644 --- a/base_logic/primitive.v +++ b/base_logic/primitive.v @@ -166,9 +166,9 @@ Notation "(∧)" := uPred_and (only parsing) : uPred_scope. Infix "∨" := uPred_or : uPred_scope. Notation "(∨)" := uPred_or (only parsing) : uPred_scope. Infix "→" := uPred_impl : uPred_scope. -Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope. -Notation "(★)" := uPred_sep (only parsing) : uPred_scope. -Notation "P -★ Q" := (uPred_wand P Q) +Infix "∗" := uPred_sep (at level 80, right associativity) : uPred_scope. +Notation "(∗)" := uPred_sep (only parsing) : uPred_scope. +Notation "P -∗ Q" := (uPred_wand P Q) (at level 99, Q at level 200, right associativity) : uPred_scope. Notation "∀ x .. y , P" := (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) @@ -184,10 +184,10 @@ Infix "≡" := uPred_internal_eq : uPred_scope. Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope. Notation "|==> Q" := (uPred_bupd Q) (at level 99, Q at level 200, format "|==> Q") : uPred_scope. -Notation "P ==★ Q" := (P ⊢ |==> Q) +Notation "P ==∗ Q" := (P ⊢ |==> Q) (at level 99, Q at level 200, only parsing) : C_scope. -Notation "P ==★ Q" := (P -★ |==> Q)%I - (at level 99, Q at level 200, format "P ==★ Q") : uPred_scope. +Notation "P ==∗ Q" := (P -∗ |==> Q)%I + (at level 99, Q at level 200, format "P ==∗ Q") : uPred_scope. Module uPred_primitive. Definition unseal := @@ -377,39 +377,39 @@ Proof. Qed. (* BI connectives *) -Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ★ P' ⊢ Q ★ Q'. +Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'. Proof. intros HQ HQ'; unseal. split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x; eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails. Qed. -Lemma True_sep_1 P : P ⊢ True ★ P. +Lemma True_sep_1 P : P ⊢ True ∗ P. Proof. unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l. Qed. -Lemma True_sep_2 P : True ★ P ⊢ P. +Lemma True_sep_2 P : True ∗ P ⊢ P. Proof. unseal; split; intros n x ? (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_includedN_r. Qed. -Lemma sep_comm' P Q : P ★ Q ⊢ Q ★ P. +Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P. Proof. unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op). Qed. -Lemma sep_assoc' P Q R : (P ★ Q) ★ R ⊢ P ★ (Q ★ R). +Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R). Proof. unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?). exists y1, (y2 ⋅ x2); split_and?; auto. + by rewrite (assoc op) -Hy -Hx. + by exists y2, x2. Qed. -Lemma wand_intro_r P Q R : (P ★ Q ⊢ R) → P ⊢ Q -★ R. +Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R. Proof. unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto. exists x, x'; split_and?; auto. eapply uPred_closed with n; eauto using cmra_validN_op_l. Qed. -Lemma wand_elim_l' P Q R : (P ⊢ Q -★ R) → P ★ Q ⊢ R. +Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R. Proof. unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst. eapply HPQR; eauto using cmra_validN_op_l. @@ -433,12 +433,12 @@ Proof. by unseal. Qed. Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a). Proof. by unseal. Qed. -Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ★ Q). +Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q). Proof. unseal; split=> n x ? [??]. exists (core x), (core x); rewrite -cmra_core_dup; auto. Qed. -Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ★ Q. +Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q. Proof. unseal; split=> n x ? [??]; exists (core x), x; simpl in *. by rewrite cmra_core_l cmra_core_idemp. @@ -459,7 +459,7 @@ Proof. unseal; by split=> -[|n] x. Qed. Lemma later_exist_false {A} (Φ : A → uPred M) : (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a). Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed. -Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ ▷ P ★ ▷ Q. +Lemma later_sep P Q : ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q. Proof. unseal; split=> n x ?; split. - destruct n as [|n]; simpl. @@ -481,7 +481,7 @@ Proof. by unseal. Qed. (* Own *) Lemma ownM_op (a1 a2 : M) : - uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2. + uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2. Proof. unseal; split=> n x ?; split. - intros [z ?]; exists a1, (a2 ⋅ z); split; [by rewrite (assoc op)|]. @@ -519,20 +519,20 @@ Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a. Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed. (* Basic update modality *) -Lemma bupd_intro P : P ==★ P. +Lemma bupd_intro P : P ==∗ P. Proof. unseal. split=> n x ? HP k yf ?; exists x; split; first done. apply uPred_closed with n; eauto using cmra_validN_op_l. Qed. -Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==★ Q. +Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==∗ Q. Proof. unseal. intros HPQ; split=> n x ? HP k yf ??. destruct (HP k yf) as (x'&?&?); eauto. exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l. Qed. -Lemma bupd_trans P : (|==> |==> P) ==★ P. +Lemma bupd_trans P : (|==> |==> P) ==∗ P. Proof. unseal; split; naive_solver. Qed. -Lemma bupd_frame_r P R : (|==> P) ★ R ==★ P ★ R. +Lemma bupd_frame_r P R : (|==> P) ∗ R ==∗ P ∗ R. Proof. unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??. destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto. @@ -542,7 +542,7 @@ Proof. apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r. Qed. Lemma bupd_ownM_updateP x (Φ : M → Prop) : - x ~~>: Φ → uPred_ownM x ==★ ∃ y, ■ Φ y ∧ uPred_ownM y. + x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ■ Φ y ∧ uPred_ownM y. Proof. unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??. destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *. diff --git a/base_logic/tactics.v b/base_logic/tactics.v index 750dd0f83e614ff6fe28da1a15889dbde1fadd81..88a28ec8c2f0c313cb35eef6a8c93395055baa8b 100644 --- a/base_logic/tactics.v +++ b/base_logic/tactics.v @@ -13,7 +13,7 @@ Module uPred_reflection. Section uPred_reflection. match e with | ETrue => True | EVar n => from_option id True%I (Σ !! n) - | ESep e1 e2 => eval Σ e1 ★ eval Σ e2 + | ESep e1 e2 => eval Σ e1 ∗ eval Σ e2 end. Fixpoint flatten (e : expr) : list nat := match e with @@ -22,7 +22,7 @@ Module uPred_reflection. Section uPred_reflection. | ESep e1 e2 => flatten e1 ++ flatten e2 end. - Notation eval_list Σ l := ([★] ((λ n, from_option id True%I (Σ !! n)) <\$> l))%I. + Notation eval_list Σ l := ([∗] ((λ n, from_option id True%I (Σ !! n)) <\$> l))%I. Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e). Proof. induction e as [| |e1 IH1 e2 IH2]; @@ -106,13 +106,13 @@ Module uPred_reflection. Section uPred_reflection. Qed. Lemma split_l Σ e ns e' : - cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ★ eval Σ e'). + cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ∗ eval Σ e'). Proof. intros He%flatten_cancel. by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten. Qed. Lemma split_r Σ e ns e' : - cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ★ eval Σ (to_expr ns)). + cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ∗ eval Σ (to_expr ns)). Proof. intros. rewrite /= comm. by apply split_l. Qed. Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}. @@ -120,7 +120,7 @@ Module uPred_reflection. Section uPred_reflection. Global Instance quote_var Σ1 Σ2 P i: rlist.QuoteLookup Σ1 Σ2 P i → Quote Σ1 Σ2 P (EVar i) | 1000. Global Instance quote_sep Σ1 Σ2 Σ3 P1 P2 e1 e2 : - Quote Σ1 Σ2 P1 e1 → Quote Σ2 Σ3 P2 e2 → Quote Σ1 Σ3 (P1 ★ P2) (ESep e1 e2). + Quote Σ1 Σ2 P1 e1 → Quote Σ2 Σ3 P2 e2 → Quote Σ1 Σ3 (P1 ∗ P2) (ESep e1 e2). Class QuoteArgs (Σ: list (uPred M)) (Ps: list (uPred M)) (ns: list nat) := {}. Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil. @@ -195,7 +195,7 @@ Tactic Notation "to_back" open_constr(Ps) := first (apply uPred_reflection.split_r with (ns:=ns'); cbv; reflexivity); simpl). -(** [sep_split] is used to introduce a (★). +(** [sep_split] is used to introduce a (∗). Use [sep_split left: [P1, P2, ...]] to define which assertions will be taken to the left; the rest will be available on the right. [sep_split right: [P1, P2, ...]] works the other way around. *) diff --git a/heap_lang/heap.v b/heap_lang/heap.v index 43d374169f01ec1b650edd8de9058a0b02b15a8a..115ff663af930e4037fbd1b485368a028c428501 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -79,13 +79,13 @@ Section heap. Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v). Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed. - Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v. + Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v. Proof. by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. Qed. Lemma heap_mapsto_op l q1 q2 v1 v2 : - l ↦{q1} v1 ★ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1. + l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1. Proof. destruct (decide (v1 = v2)) as [->|]. { by rewrite heap_mapsto_op_eq pure_equiv // left_id. } @@ -96,18 +96,18 @@ Section heap. Qed. Lemma heap_mapsto_op_1 l q1 q2 v1 v2 : - l ↦{q1} v1 ★ l ↦{q2} v2 ⊢ v1 = v2 ∧ l ↦{q1+q2} v1. + l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ v1 = v2 ∧ l ↦{q1+q2} v1. Proof. by rewrite heap_mapsto_op. Qed. Lemma heap_mapsto_op_half l q v1 v2 : - l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q} v1. + l ↦{q/2} v1 ∗ l ↦{q/2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q} v1. Proof. by rewrite heap_mapsto_op Qp_div_2. Qed. Lemma heap_mapsto_op_half_1 l q v1 v2 : - l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊢ v1 = v2 ∧ l ↦{q} v1. + l ↦{q/2} v1 ∗ l ↦{q/2} v2 ⊢ v1 = v2 ∧ l ↦{q} v1. Proof. by rewrite heap_mapsto_op_half. Qed. - Lemma heap_ex_mapsto_op l q1 q2 : l ↦{q1} - ★ l ↦{q2} - ⊣⊢ l ↦{q1+q2} -. + Lemma heap_ex_mapsto_op l q1 q2 : l ↦{q1} - ∗ l ↦{q2} - ⊣⊢ l ↦{q1+q2} -. Proof. iSplit. - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2". @@ -116,7 +116,7 @@ Section heap. iDestruct "H" as "[H1 H2]"; iSplitL "H1"; eauto. Qed. - Lemma heap_ex_mapsto_op_half l q : l ↦{q/2} - ★ l ↦{q/2} - ⊣⊢ l ↦{q} -. + Lemma heap_ex_mapsto_op_half l q : l ↦{q/2} - ∗ l ↦{q/2} - ⊣⊢ l ↦{q} -. Proof. by rewrite heap_ex_mapsto_op Qp_div_2. Qed. (** Weakest precondition *) @@ -136,7 +136,7 @@ Section heap. Lemma wp_load E l q v : nclose heapN ⊆ E → - {{{ heap_ctx ★ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E + {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}. Proof. iIntros (? Φ) "[#Hinv >Hl] HΦ". @@ -149,7 +149,7 @@ Section heap. Lemma wp_store E l v' e v : to_val e = Some v → nclose heapN ⊆ E → - {{{ heap_ctx ★ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E + {{{ heap_ctx ∗ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}. Proof. iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ". @@ -165,7 +165,7 @@ Section heap. Lemma wp_cas_fail E l q v' e1 v1 e2 v2 : to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose heapN ⊆ E → - {{{ heap_ctx ★ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E + {{{ heap_ctx ∗ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ RET LitV (LitBool false); l ↦{q} v' }}}. Proof. iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ". @@ -178,7 +178,7 @@ Section heap. Lemma wp_cas_suc E l e1 v1 e2 v2 : to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E → - {{{ heap_ctx ★ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E + {{{ heap_ctx ∗ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ RET LitV (LitBool true); l ↦ v2 }}}. Proof. iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ". diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v index 764fa2347341f2acc3f1a3f010cd5555ef9f3815..dc9ed307b6aa2212aa61569e557a5d0596feb89d 100644 --- a/heap_lang/lib/barrier/proof.v +++ b/heap_lang/lib/barrier/proof.v @@ -24,7 +24,7 @@ Implicit Types I : gset gname. Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ := (∃ Ψ : gname → iProp Σ, - ▷ (P -★ [★ set] i ∈ I, Ψ 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 _ => #false | State High _ => #true end. @@ -35,18 +35,18 @@ Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ := Arguments state_to_prop !_ _ / : simpl nomatch. Definition barrier_inv (l : loc) (P : iProp Σ) (s : state) : iProp Σ := - (l ↦ s ★ ress (state_to_prop s P) (state_I s))%I. + (l ↦ s ∗ ress (state_to_prop s P) (state_I s))%I. Definition barrier_ctx (γ : gname) (l : loc) (P : iProp Σ) : iProp Σ := - (■ (heapN ⊥ N) ★ heap_ctx ★ sts_ctx γ N (barrier_inv l P))%I. + (■ (heapN ⊥ N) ∗ heap_ctx ∗ sts_ctx γ N (barrier_inv l P))%I. Definition send (l : loc) (P : iProp Σ) : iProp Σ := - (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I. + (∃ γ, barrier_ctx γ l P ∗ sts_ownS γ low_states {[ Send ]})%I. Definition recv (l : loc) (R : iProp Σ) : iProp Σ := (∃ γ P Q i, - barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★ - saved_prop_own i Q ★ ▷ (Q -★ R))%I. + barrier_ctx γ l P ∗ sts_ownS γ (i_states i) {[ Change i ]} ∗ + saved_prop_own i Q ∗ ▷ (Q -∗ R))%I. Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) : PersistentP (barrier_ctx γ l P). @@ -73,8 +73,8 @@ Proof. solve_proper. Qed. (** Helper lemmas *) Lemma ress_split i i1 i2 Q R1 R2 P I : i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 → - saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★ - (Q -★ R1 ★ R2) ★ ress P I + saved_prop_own i Q ∗ saved_prop_own i1 R1 ∗ saved_prop_own i2 R2 ∗ + (Q -∗ R1 ∗ R2) ∗ ress P I ⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}). Proof. iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]". @@ -92,7 +92,7 @@ Qed. (** Actual proofs *) Lemma newbarrier_spec (P : iProp Σ) : heapN ⊥ N → - {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ★ send l P }}}. + {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}. Proof. iIntros (HN Φ) "#? HΦ". rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl". @@ -105,7 +105,7 @@ Proof. iAssert (barrier_ctx γ' l P)%I as "#?". { rewrite /barrier_ctx. by repeat iSplit. } iAssert (sts_ownS γ' (i_states γ) {[Change γ]} - ★ sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]". + ∗ sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]". { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. - set_solver. - iApply (sts_own_weaken with "Hγ'"); @@ -117,7 +117,7 @@ Proof. Qed. Lemma signal_spec l P : - {{{ send l P ★ P }}} signal #l {{{ RET #(); True }}}. + {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}. Proof. rewrite /signal /send /barrier_ctx /=. iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let. @@ -151,7 +151,7 @@ Proof. return to the client *) iDestruct "Hr" as (Ψ) "[HΨ Hsp]". iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done. - iAssert (▷ Ψ i ★ ▷ [★ set] j ∈ I ∖ {[i]}, Ψ j)%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Ψ". } iMod ("Hclose" \$! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]"). { iSplit; [iPureIntro; by eauto using wait_step|]. @@ -162,7 +162,7 @@ Proof. Qed. Lemma recv_split E l P1 P2 : - nclose N ⊆ E → recv l (P1 ★ P2) ={E}=★ recv l P1 ★ recv l P2. + nclose N ⊆ E → recv l (P1 ∗ P2) ={E}=∗ recv l P1 ∗ recv l P2. Proof. rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". @@ -178,7 +178,7 @@ Proof. iNext. rewrite {2}/barrier_inv /=. iFrame "Hl". iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. } iAssert (sts_ownS γ (i_states i1) {[Change i1]} - ★ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]". + ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]". { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. - abstract set_solver. - iApply (sts_own_weaken with "Hγ"); @@ -189,7 +189,7 @@ Proof. - iExists γ, P, R2, i2. iFrame; auto. Qed. -Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ recv l P1 -★ recv l P2. +Lemma recv_weaken l P1 P2 : (P1 -∗ P2) ⊢ recv l P1 -∗ recv l P2. Proof. rewrite /recv. iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)". diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v index c0de6dd97b73b9b7fcb0d23bc392441152673cd3..914f97751df9f9ee99336578456ca4534a6d02d7 100644 --- a/heap_lang/lib/barrier/specification.v +++ b/heap_lang/lib/barrier/specification.v @@ -11,11 +11,11 @@ Lemma barrier_spec (N : namespace) : heapN ⊥ N → ∃ recv send : loc → iProp Σ -n> iProp Σ, (∀ P, heap_ctx ⊢ {{ True }} newbarrier #() - {{ v, ∃ l : loc, v = #l ★ recv l P ★ send l P }}) ∧ - (∀ l P, {{ send l P ★ P }} signal #l {{ _, True }}) ∧ + {{ v, ∃ l : loc, v = #l ∗ recv l P ∗ send l P }}) ∧ + (∀ l P, {{ send l P ∗ P }} signal #l {{ _, True }}) ∧ (∀ l P, {{ recv l P }} wait #l {{ _, P }}) ∧ - (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧ - (∀ l P Q, (P -★ Q) ⊢ recv l P -★ recv l Q). + (∀ l P Q, recv l (P ∗ Q) ={N}=> recv l P ∗ recv l Q) ∧ + (∀ l P Q, (P -∗ Q) ⊢ recv l P -∗ recv l Q). Proof. intros HN. exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)). diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v index 16a4967301f07a33b4341755c147a9337cc96397..5065d5b9da83ae667e2bb34c9d41200c9777887c 100644 --- a/heap_lang/lib/counter.v +++ b/heap_lang/lib/counter.v @@ -23,7 +23,7 @@ Section mono_proof. Context `{!heapG Σ, !mcounterG Σ} (N : namespace). Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ := - (∃ n, own γ (● (n : mnat)) ★ l ↦ #n)%I. + (∃ n, own γ (● (n : mnat)) ∗ l ↦ #n)%I. Definition mcounter (l : loc) (n : nat) : iProp Σ := (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ @@ -96,7 +96,7 @@ Section contrib_spec. Context `{!heapG Σ, !ccounterG Σ} (N : namespace). Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ := - (∃ n, own γ (● Some (1%Qp, n)) ★ l ↦ #n)%I. + (∃ n, own γ (● Some (1%Qp, n)) ∗ l ↦ #n)%I. Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ := (heapN ⊥ N ∧ heap_ctx ∧ inv N (ccounter_inv γ l))%I. @@ -106,13 +106,13 @@ Section contrib_spec. (** The main proofs. *) Lemma ccounter_op γ q1 q2 n1 n2 : - ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1★ ccounter γ q2 n2. + ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1∗ ccounter γ q2 n2. Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed. Lemma newcounter_contrib_spec (R : iProp Σ) : heapN ⊥ N → {{{ heap_ctx }}} newcounter #() - {{{ γ l, RET #l; ccounter_ctx γ l ★ ccounter γ 1 0 }}}. + {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}. Proof. iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat)))) @@ -123,7 +123,7 @@ Section contrib_spec. Qed. Lemma inc_contrib_spec γ l q n : - {{{ ccounter_ctx γ l ★ ccounter γ q n }}} inc #l + {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} inc #l {{{ RET #(); ccounter γ q (S n) }}}. Proof. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec. @@ -144,7 +144,7 @@ Section contrib_spec. Qed. Lemma read_contrib_spec γ l q n : - {{{ ccounter_ctx γ l ★ ccounter γ q n }}} read #l + {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l {{{ c, RET #c; ■ (n ≤ c)%nat ∧ ccounter γ q n }}}. Proof. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". @@ -156,7 +156,7 @@ Section contrib_spec. Qed. Lemma read_contrib_spec_1 γ l n : - {{{ ccounter_ctx γ l ★ ccounter γ 1 n }}} read #l + {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l {{{ n, RET #n; ccounter γ 1 n }}}. Proof. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v index 43f81ecb517a61995abe5797328987b1f0344588..ffa2634c56c4379e241577a99f2ccc18fc233dfd 100644 --- a/heap_lang/lib/lock.v +++ b/heap_lang/lib/lock.v @@ -14,15 +14,15 @@ Structure lock Σ `{!heapG Σ} := Lock { is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk); is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R); locked_timeless γ : TimelessP (locked γ); - locked_exclusive γ : locked γ ★ locked γ ⊢ False; + locked_exclusive γ : locked γ ∗ locked γ ⊢ False; (* -- operation specs -- *) newlock_spec N (R : iProp Σ) : heapN ⊥ N → - {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}}; + {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}}; acquire_spec N γ lk R : - {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}; + {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}; release_spec N γ lk R : - {{{ is_lock N γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}} + {{{ is_lock N γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}} }. Arguments newlock {_ _} _. diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v index 5efd170e7884bd36fd559a0530ccc5dba22e8a46..1e7904dce022b265b6c55c0af5141c5a5d0baf69 100644 --- a/heap_lang/lib/par.v +++ b/heap_lang/lib/par.v @@ -22,8 +22,8 @@ Context `{!heapG Σ, !spawnG Σ}. This is why these are not Texan triples. *) Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) : to_val e = Some (f1,f2)%V → - (heap_ctx ★ WP f1 #() {{ Ψ1 }} ★ WP f2 #() {{ Ψ2 }} ★ - ▷ ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V) + (heap_ctx ∗ WP f1 #() {{ Ψ1 }} ∗ WP f2 #() {{ Ψ2 }} ∗ + ▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) ⊢ WP par e {{ Φ }}. Proof. iIntros (?) "(#Hh&Hf1&Hf2&HΦ)". @@ -37,8 +37,8 @@ Qed. Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) : - (heap_ctx ★ WP e1 {{ Ψ1 }} ★ WP e2 {{ Ψ2 }} ★ - ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V) + (heap_ctx ∗ WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗ + ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) ⊢ WP e1 || e2 {{ Φ }}. Proof. iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- \$Hh \$H]"); try wp_done. diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v index 54053ad1b2c77989ddb5fb5fbf17a270da244ac0..4736671187a35356befafcf0553243ffd5bba9b6 100644 --- a/heap_lang/lib/spawn.v +++ b/heap_lang/lib/spawn.v @@ -29,11 +29,11 @@ Section proof. Context `{!heapG Σ, !spawnG Σ} (N : namespace). Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ := - (∃ lv, l ↦ lv ★ (lv = NONEV ∨ - ∃ v, lv = SOMEV v ★ (Ψ v ∨ own γ (Excl ()))))%I. + (∃ lv, l ↦ lv ∗ (lv = NONEV ∨ + ∃ v, lv = SOMEV v ∗ (Ψ v ∨ own γ (Excl ()))))%I. Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ := - (heapN ⊥ N ★ ∃ γ, heap_ctx ★ own γ (Excl ()) ★ + (heapN ⊥ N ∗ ∃ γ, heap_ctx ∗ own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I. Typeclasses Opaque join_handle. @@ -49,7 +49,7 @@ Proof. solve_proper. Qed. Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) : to_val e = Some f → heapN ⊥ N → - {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}. + {{{ heap_ctx ∗ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}. Proof. iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=. wp_let. wp_alloc l as "Hl". wp_let. diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v index 44443f4f66b634ddfa680dfbd231b61e67be6317..42d5c3821e0b0cc2455fa51ecfcc10009c3b3520 100644 --- a/heap_lang/lib/spin_lock.v +++ b/heap_lang/lib/spin_lock.v @@ -24,14 +24,14 @@ Section proof. Context `{!heapG Σ, !lockG Σ} (N : namespace). Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ := - (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I. + (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I. Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ := (∃ l: loc, heapN ⊥ N ∧ heap_ctx ∧ lk = #l ∧ inv N (lock_inv γ l R))%I. Definition locked (γ : gname): iProp Σ := own γ (Excl ()). - Lemma locked_exclusive (γ : gname) : locked γ ★ locked γ ⊢ False. + Lemma locked_exclusive (γ : gname) : locked γ ∗ locked γ ⊢ False. Proof. rewrite /locked own_valid_2. by iIntros (?). Qed. Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l). @@ -47,7 +47,7 @@ Section proof. Lemma newlock_spec (R : iProp Σ): heapN ⊥ N → - {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}. + {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}. Proof. iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=. wp_seq. wp_alloc l as "Hl". @@ -59,7 +59,7 @@ Section proof. Lemma try_acquire_spec γ lk R : {{{ is_lock γ lk R }}} try_acquire lk - {{{ b, RET #b; if b is true then locked γ ★ R else True }}}. + {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}. Proof. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst. wp_rec. iInv N as ([]) "[Hl HR]" "Hclose". @@ -71,7 +71,7 @@ Section proof. Qed. Lemma acquire_spec γ lk R : - {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}. + {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}. Proof. iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec. wp_apply (try_acquire_spec with "Hl"). iIntros ([]). @@ -80,7 +80,7 @@ Section proof. Qed. Lemma release_spec γ lk R : - {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}. + {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}. Proof. iIntros (Φ) "(Hlock & Hlocked & HR) HΦ". iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst. diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v index 5300485fcc6ef81e7e75f321a8451c104c8321ff..6a9812079b741e11ae25bb35bab468037f2845c3 100644 --- a/heap_lang/lib/ticket_lock.v +++ b/heap_lang/lib/ticket_lock.v @@ -41,9 +41,9 @@ Section proof. Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ := (∃ o n : nat, - lo ↦ #o ★ ln ↦ #n ★ - own γ (● (Excl' o, GSet (seq_set 0 n))) ★ - ((own γ (◯ (Excl' o, ∅)) ★ R) ∨ own γ (◯ (∅, GSet {[ o ]}))))%I. + lo ↦ #o ∗ ln ↦ #n ∗ + own γ (● (Excl' o, GSet (seq_set 0 n))) ∗ + ((own γ (◯ (Excl' o, ∅)) ∗ R) ∨ own γ (◯ (∅, GSet {[ o ]}))))%I. Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ := (∃ lo ln : loc, @@ -68,7 +68,7 @@ Section proof. Global Instance locked_timeless γ : TimelessP (locked γ). Proof. apply _. Qed. - Lemma locked_exclusive (γ : gname) : (locked γ ★ locked γ ⊢ False)%I. + Lemma locked_exclusive (γ : gname) : (locked γ ∗ locked γ ⊢ False)%I. Proof. iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2". iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _]. @@ -76,7 +76,7 @@ Section proof. Lemma newlock_spec (R : iProp Σ) : heapN ⊥ N → - {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}. + {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}. Proof. iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=. wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln". @@ -89,7 +89,7 @@ Section proof. Qed. Lemma wait_loop_spec γ lk x R : - {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ ★ R }}}. + {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}. Proof. iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)". iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E. @@ -110,7 +110,7 @@ Section proof. Qed. Lemma acquire_spec γ lk R : - {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}. + {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}. Proof. iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)". iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj. @@ -141,7 +141,7 @@ Section proof. Qed. Lemma release_spec γ lk R : - {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}. + {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}. Proof. iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst. diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index 71ce9d61655dd367d747d5f57388522078ca6c3c..4709947ba7dc36cc0aefa2e196f666427f457243 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -95,7 +95,7 @@ Qed. (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e Φ : - ▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. + ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto. - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton. diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v index 4fa37193439e1d07a2bd65d48272af6a18ff8b35..c30f339bfc96606493c2b5e64885cea242e5025b 100644 --- a/program_logic/adequacy.v +++ b/program_logic/adequacy.v @@ -38,7 +38,7 @@ Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed. (* Allocation *) -Lemma wsat_alloc `{invPreG Σ} : True ==★ ∃ _ : invG Σ, wsat ★ ownE ⊤. +Lemma wsat_alloc `{invPreG Σ} : True ==∗ ∃ _ : invG Σ, wsat ∗ ownE ⊤. Proof. iIntros. iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done. @@ -50,7 +50,7 @@ Proof. Qed. Lemma iris_alloc `{irisPreG' Λstate Σ} σ : - True ==★ ∃ _ : irisG' Λstate Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ. + True ==∗ ∃ _ : irisG' Λstate Σ, wsat ∗ ownE ⊤ ∗ ownP_auth σ ∗ ownP σ. Proof. iIntros. iMod wsat_alloc as (?) "[Hws HE]". @@ -91,13 +91,13 @@ Implicit Types P Q : iProp Σ. Implicit Types Φ : val Λ → iProp Σ. Implicit Types Φs : list (val Λ → iProp Σ). -Notation world σ := (wsat ★ ownE ⊤ ★ ownP_auth σ)%I. +Notation world σ := (wsat ∗ ownE ⊤ ∗ ownP_auth σ)%I. -Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I. +Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I. Lemma wp_step e1 σ1 e2 σ2 efs Φ : prim_step e1 σ1 e2 σ2 efs → - world σ1 ★ WP e1 {{ Φ }} ==★ ▷ |==> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs). + world σ1 ∗ WP e1 {{ Φ }} ==∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp efs). Proof. rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. } @@ -110,8 +110,8 @@ Qed. Lemma wptp_step e1 t1 t2 σ1 σ2 Φ : step (e1 :: t1,σ1) (t2, σ2) → - world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 - ==★ ∃ e2 t2', t2 = e2 :: t2' ★ ▷ |==> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp t2'). + world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 + ==∗ ∃ e2 t2', t2 = e2 :: t2' ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2'). Proof. iIntros (Hstep) "(HW & He & Ht)". destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=. @@ -125,9 +125,9 @@ Qed. Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → - world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ + world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢ Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2', - t2 = e2 :: t2' ★ world σ2 ★ WP e2 {{ Φ }} ★ wptp t2'). + t2 = e2 :: t2' ∗ world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2'). Proof. revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=. { inversion_clear 1; iIntros "?"; eauto 10. } @@ -140,7 +140,7 @@ Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |==> ▷ Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed. Lemma bupd_iter_frame_l n R Q : - R ★ Nat.iter n (λ P, |==> ▷ P) Q ⊢ Nat.iter n (λ P, |==> ▷ P) (R ★ Q). + R ∗ Nat.iter n (λ P, |==> ▷ P) Q ⊢ Nat.iter n (λ P, |==> ▷ P) (R ∗ Q). Proof. induction n as [|n IH]; simpl; [done|]. by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH. @@ -148,7 +148,7 @@ Qed. Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ : nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) → - world σ1 ★ WP e1 {{ v, ■ φ v }} ★ wptp t1 ⊢ + world σ1 ∗ WP e1 {{ v, ■ φ v }} ∗ wptp t1 ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ φ v2). Proof. intros. rewrite wptp_steps //. @@ -159,7 +159,7 @@ Proof. Qed. Lemma wp_safe e σ Φ : - world σ ★ WP e {{ Φ }} ==★ ▷ ■ (is_Some (to_val e) ∨ reducible e σ). + world σ ∗ WP e {{ Φ }} ==∗ ▷ ■ (is_Some (to_val e) ∨ reducible e σ). Proof. rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]"; eauto 10. } @@ -169,7 +169,7 @@ Qed. Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 → - world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ + world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ (is_Some (to_val e2) ∨ reducible e2 σ2)). Proof. intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. @@ -180,8 +180,8 @@ Qed. Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → - (I ={⊤,∅}=★ ∃ σ', ownP σ' ∧ ■ φ σ') → - I ★ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ + (I ={⊤,∅}=∗ ∃ σ', ownP σ' ∧ ■ φ σ') → + I ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ φ σ2). Proof. intros ? HI. rewrite wptp_steps //. @@ -213,8 +213,8 @@ Proof. Qed. Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ : - (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=★ I ★ WP e {{ Φ }}) → - (∀ `{irisG Λ Σ}, I ={⊤,∅}=★ ∃ σ', ownP σ' ∧ ■ φ σ') → + (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=∗ I ∗ WP e {{ Φ }}) → + (∀ `{irisG Λ Σ}, I ={⊤,∅}=∗ ∃ σ', ownP σ' ∧ ■ φ σ') → rtc step ([e], σ1) (t2, σ2) → φ σ2. Proof. diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v index 28a3e76362232b50d58a109c386771279b0163cd..a35324f53db2e7074b72c877a4ec0af57b6f0ffd 100644 --- a/program_logic/ectx_lifting.v +++ b/program_logic/ectx_lifting.v @@ -16,9 +16,9 @@ Lemma wp_ectx_bind {E e} K Φ : Proof. apply: weakestpre.wp_bind. Qed. Lemma wp_lift_head_step E Φ e1 : - (|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ★ ▷ ownP σ1 ★ - ▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ★ ownP σ2 - ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + (|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ∗ ▷ ownP σ1 ∗ + ▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ∗ ownP σ2 + ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros "H". iApply (wp_lift_step E); try done. @@ -31,7 +31,7 @@ Lemma wp_lift_pure_head_step E Φ e1 : (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) → (▷ ∀ e2 efs σ, ■ head_step e1 σ e2 σ efs → - WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext. @@ -41,9 +41,9 @@ Qed. Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 : atomic e1 → head_reducible e1 σ1 → - ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs, - ■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ - Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + ▷ ownP σ1 ∗ ▷ (∀ v2 σ2 efs, + ■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -∗ + Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext. @@ -55,8 +55,8 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs : head_reducible e1 σ1 → (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' → σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') → - ▷ ownP σ1 ★ ▷ (ownP σ2 -★ - Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ + Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. eauto using wp_lift_atomic_det_step. Qed. @@ -74,7 +74,7 @@ Qed. Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs : (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') → - ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. eauto using wp_lift_pure_det_step. Qed. diff --git a/program_logic/hoare.v b/program_logic/hoare.v index 4ce26dd3a8c469430df623db72edb34e6f4c014f..8fcb0ec3cae82267ab3b4132e493e943f039e038 100644 --- a/program_logic/hoare.v +++ b/program_logic/hoare.v @@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics. Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ) (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ := - (□ (P -★ WP e @ E {{ Φ }}))%I. + (□ (P -∗ WP e @ E {{ Φ }}))%I. Instance: Params (@ht) 4. Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ) @@ -96,17 +96,17 @@ Proof. Qed. Lemma ht_frame_l E P Φ R e : - {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ v, R ★ Φ v }}. + {{ P }} e @ E {{ Φ }} ⊢ {{ R ∗ P }} e @ E {{ v, R ∗ Φ v }}. Proof. iIntros "#Hwp !# [\$ HP]". by iApply "Hwp". Qed. Lemma ht_frame_r E P Φ R e : - {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ v, Φ v ★ R }}. + {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ R }} e @ E {{ v, Φ v ∗ R }}. Proof. iIntros "#Hwp !# [HP \$]". by iApply "Hwp". Qed. Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ : to_val e = None → E2 ⊆ E1 → (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }} - ⊢ {{ R1 ★ P }} e @ E1 {{ λ v, R2 ★ Φ v }}. + ⊢ {{ R1 ∗ P }} e @ E1 {{ λ v, R2 ∗ Φ v }}. Proof. iIntros (??) "[#Hvs #Hwp] !# [HR HP]". iApply (wp_frame_step_l E1 E2); try done. @@ -116,7 +116,7 @@ Qed. Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ : to_val e = None → E2 ⊆ E1 → (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }} - ⊢ {{ P ★ R1 }} e @ E1 {{ λ v, Φ v ★ R2 }}. + ⊢ {{ P ∗ R1 }} e @ E1 {{ λ v, Φ v ∗ R2 }}. Proof. iIntros (??) "[#Hvs #Hwp] !# [HP HR]". iApply (wp_frame_step_r E1 E2); try done. @@ -125,7 +125,7 @@ Qed. Lemma ht_frame_step_l' E P R e Φ : to_val e = None → - {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ v, R ★ Φ v }}. + {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ E {{ v, R ∗ Φ v }}. Proof. iIntros (?) "#Hwp !# [HR HP]". iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp". @@ -133,7 +133,7 @@ Qed. Lemma ht_frame_step_r' E P Φ R e : to_val e = None → - {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ v, Φ v ★ R }}. + {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ E {{ v, Φ v ∗ R }}. Proof. iIntros (?) "#Hwp !# [HP HR]". iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp". diff --git a/program_logic/lifting.v b/program_logic/lifting.v index a3335b346e5a4aea35d697cf96decfc8b6e78206..4e4f84916a4babc9c3c640b6515e5aae5f1592f3 100644 --- a/program_logic/lifting.v +++ b/program_logic/lifting.v @@ -11,9 +11,9 @@ Implicit Types P Q : iProp Σ. Implicit Types Φ : val Λ → iProp Σ. Lemma wp_lift_step E Φ e1 : - (|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ★ ▷ ownP σ1 ★ - ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ★ ownP σ2 - ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + (|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ∗ ▷ ownP σ1 ∗ + ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ∗ ownP σ2 + ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros "H". rewrite wp_unfold /wp_pre. @@ -32,7 +32,7 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 : (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) → (▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs → - WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto. @@ -47,8 +47,8 @@ Qed. Lemma wp_lift_atomic_step {E Φ} e1 σ1 : atomic e1 → reducible e1 σ1 → - (▷ ownP σ1 ★ ▷ ∀ v2 σ2 efs, ■ prim_step e1 σ1 (of_val v2) σ2 efs ★ ownP σ2 -★ - Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + (▷ ownP σ1 ∗ ▷ ∀ v2 σ2 efs, ■ prim_step e1 σ1 (of_val v2) σ2 efs ∗ ownP σ2 -∗ + Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1). @@ -65,8 +65,8 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs : reducible e1 σ1 → (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' → σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') → - ▷ ownP σ1 ★ ▷ (ownP σ2 -★ - Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ + Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done. @@ -77,7 +77,7 @@ Qed. Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs : (∀ σ1, reducible e1 σ1) → (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→ - ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }}) + ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ⊢ WP e1 @ E {{ Φ }}. Proof. iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step E); try done. diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v index d5f94f1c4b34ddf051e6c31fc16143f02f5acc62..ffaa00fa5a3ab26c19a96439eec93cba7918dae5 100644 --- a/program_logic/weakestpre.v +++ b/program_logic/weakestpre.v @@ -29,10 +29,10 @@ Definition wp_pre `{irisG Λ Σ} (∃ v, to_val e1 = Some v ∧ |={E}=> Φ v) ∨ (* step case *) (to_val e1 = None ∧ ∀ σ1, - ownP_auth σ1 ={E,∅}=★ ■ reducible e1 σ1 ★ - ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ={∅,E}=★ - ownP_auth σ2 ★ wp E e2 Φ ★ - [★ list] ef ∈ efs, wp ⊤ ef (λ _, True)))%I. + ownP_auth σ1 ={E,∅}=∗ ■ reducible e1 σ1 ∗ + ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ={∅,E}=∗ + ownP_auth σ2 ∗ wp E e2 Φ ∗ + [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)))%I. Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre. Proof. @@ -70,39 +70,39 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) (* Texan triples *) Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" := (□ ∀ Φ, - P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I + P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I (at level 20, x closed binder, y closed binder, format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : uPred_scope. Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" := (□ ∀ Φ, - P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I + P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I (at level 20, x closed binder, y closed binder, format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : uPred_scope. Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" := - (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I + (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I (at level 20, format "{{{ P } } } e {{{ RET pat ; Q } } }") : uPred_scope. Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" := - (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I + (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I (at level 20, format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : uPred_scope. Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" := (∀ Φ : _ → uPred _, - P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }}) + P ⊢ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) (at level 20, x closed binder, y closed binder, format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : C_scope. Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" := (∀ Φ : _ → uPred _, - P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }}) + P ⊢ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) (at level 20, x closed binder, y closed binder, format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : C_scope. Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" := - (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }}) + (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) (at level 20, format "{{{ P } } } e {{{ RET pat ; Q } } }") : C_scope. Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" := - (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }}) + (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) (at level 20, format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : C_scope. @@ -114,17 +114,17 @@ Implicit Types v : val Λ. Implicit Types e : expr Λ. (* Physical state *) -Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ False. +Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False. Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed. Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ). Proof. rewrite /ownP; apply _. Qed. -Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ★ ownP σ2 ⊢ σ1 = σ2. +Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ∗ ownP σ2 ⊢ σ1 = σ2. Proof. rewrite /ownP /ownP_auth own_valid_2 -auth_both_op. by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete). Qed. -Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 ==★ ownP_auth σ2 ★ ownP σ2. +Lemma ownP_update σ1 σ2 : ownP_auth σ1 ∗ ownP σ1 ==∗ ownP_auth σ2 ∗ ownP σ2. Proof. rewrite /ownP -!own_op. by apply own_update, auth_update, option_local_update, exclusive_local_update. @@ -156,14 +156,14 @@ Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre. iLeft; iExists v; rewrite to_of_val; auto. Qed. -Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=★ Φ v. +Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=∗ Φ v. Proof. rewrite wp_unfold /wp_pre to_of_val. iIntros "[H|[% _]]"; [|done]. by iDestruct "H" as (v') "[% ?]"; simplify_eq. Qed. Lemma wp_strong_mono E1 E2 e Φ Ψ : - E1 ⊆ E2 → (∀ v, Φ v ={E2}=★ Ψ v) ★ WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}. + E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}. Proof. iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre. iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight]. @@ -208,7 +208,7 @@ Qed. Lemma wp_frame_step_l E1 E2 e Φ R : to_val e = None → E2 ⊆ E1 → - (|={E1,E2}▷=> R) ★ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ★ Φ v }}. + (|={E1,E2}▷=> R) ∗ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ∗ Φ v }}. Proof. rewrite !wp_unfold /wp_pre. iIntros (??) "[HR [Hv|[_ H]]]". { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. } @@ -256,33 +256,33 @@ Lemma wp_value_fupd E Φ e v : to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}. Proof. intros. rewrite -wp_fupd -wp_value //. Qed. -Lemma wp_frame_l E e Φ R : R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}. +Lemma wp_frame_l E e Φ R : R ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ∗ Φ v }}. Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed. -Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ★ R ⊢ WP e @ E {{ v, Φ v ★ R }}. +Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ∗ R ⊢ WP e @ E {{ v, Φ v ∗ R }}. Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed. Lemma wp_frame_step_r E1 E2 e Φ R : to_val e = None → E2 ⊆ E1 → - WP e @ E2 {{ Φ }} ★ (|={E1,E2}▷=> R) ⊢ WP e @ E1 {{ v, Φ v ★ R }}. + WP e @ E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ E1 {{ v, Φ v ∗ R }}. Proof. - rewrite [(WP _ @ _ {{ _ }} ★ _)%I]comm; setoid_rewrite (comm _ _ R). + rewrite [(WP _ @ _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R). apply wp_frame_step_l. Qed. Lemma wp_frame_step_l' E e Φ R : - to_val e = None → ▷ R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}. + to_val e = None → ▷ R ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ∗ Φ v }}. Proof. iIntros (?) "[??]". iApply (wp_frame_step_l E E); try iFrame; eauto. Qed. Lemma wp_frame_step_r' E e Φ R : - to_val e = None → WP e @ E {{ Φ }} ★ ▷ R ⊢ WP e @ E {{ v, Φ v ★ R }}. + to_val e = None → WP e @ E {{ Φ }} ∗ ▷ R ⊢ WP e @ E {{ v, Φ v ∗ R }}. Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed. Lemma wp_wand_l E e Φ Ψ : - (∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}. + (∀ v, Φ v -∗ Ψ v) ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}. Proof. iIntros "[H Hwp]". iApply (wp_strong_mono E); auto. iFrame "Hwp". iIntros (?) "?". by iApply "H". Qed. Lemma wp_wand_r E e Φ Ψ : - WP e @ E {{ Φ }} ★ (∀ v, Φ v -★ Ψ v) ⊢ WP e @ E {{ Ψ }}. + WP e @ E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ E {{ Ψ }}. Proof. by rewrite comm wp_wand_l. Qed. End wp. diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v index fb5b5de765a64fb0ab5123e0e276f66f6bba1963..305ba447d24b52c61c62f67b7c9f4e62dd9fe5df 100644 --- a/proofmode/class_instances.v +++ b/proofmode/class_instances.v @@ -69,20 +69,20 @@ Global Instance into_later_or P1 P2 Q1 Q2 : IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2). Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed. Global Instance into_later_sep P1 P2 Q1 Q2 : - IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ★ P2) (Q1 ★ Q2). + IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∗ P2) (Q1 ∗ Q2). Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed. Global Instance into_later_big_sepM `{Countable K} {A} (Φ Ψ : K → A → uPred M) (m : gmap K A) : (∀ x k, IntoLater (Φ k x) (Ψ k x)) → - IntoLater ([★ map] k ↦ x ∈ m, Φ k x) ([★ map] k ↦ x ∈ m, Ψ k x). + IntoLater ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x). Proof. rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono. Qed. Global Instance into_later_big_sepS `{Countable A} (Φ Ψ : A → uPred M) (X : gset A) : (∀ x, IntoLater (Φ x) (Ψ x)) → - IntoLater ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ x). + IntoLater ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x). Proof. rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono. Qed. @@ -97,12 +97,12 @@ Global Instance from_later_or P1 P2 Q1 Q2 : FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2). Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed. Global Instance from_later_sep P1 P2 Q1 Q2 : - FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ★ P2) (Q1 ★ Q2). + FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∗ P2) (Q1 ∗ Q2). Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed. (* IntoWand *) Global Instance into_wand_wand P Q Q' : - FromAssumption false Q Q' → IntoWand (P -★ Q) P Q'. + FromAssumption false Q Q' → IntoWand (P -∗ Q) P Q'. Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed. Global Instance into_wand_impl P Q Q' : FromAssumption false Q Q' → IntoWand (P → Q) P Q'. @@ -121,10 +121,10 @@ Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed. Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2. Proof. done. Qed. Global Instance from_and_sep_persistent_l P1 P2 : - PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9. + PersistentP P1 → FromAnd (P1 ∗ P2) P1 P2 | 9. Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed. Global Instance from_and_sep_persistent_r P1 P2 : - PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10. + PersistentP P2 → FromAnd (P1 ∗ P2) P1 P2 | 10. Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed. Global Instance from_and_always P Q1 Q2 : FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2). @@ -134,7 +134,7 @@ Global Instance from_and_later P Q1 Q2 : Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed. (* FromSep *) -Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100. +Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100. Proof. done. Qed. Global Instance from_sep_ownM (a b1 b2 : M) : FromOp a b1 b2 → @@ -153,14 +153,14 @@ Proof. rewrite /FromSep=><-. apply bupd_sep. Qed. Global Instance from_sep_big_sepM `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m : (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) → - FromSep ([★ map] k ↦ x ∈ m, Φ k x) - ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x). + FromSep ([∗ map] k ↦ x ∈ m, Φ k x) + ([∗ map] k ↦ x ∈ m, Ψ1 k x) ([∗ map] k ↦ x ∈ m, Ψ2 k x). Proof. rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed. Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X : (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) → - FromSep ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x). + FromSep ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ1 x) ([∗ set] x ∈ X, Ψ2 x). Proof. rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono. Qed. @@ -194,7 +194,7 @@ Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 : Proof. by constructor. Qed. (* IntoAnd *) -Global Instance into_and_sep p P Q : IntoAnd p (P ★ Q) P Q. +Global Instance into_and_sep p P Q : IntoAnd p (P ∗ Q) P Q. Proof. by apply mk_into_and_sep. Qed. Global Instance into_and_ownM p (a b1 b2 : M) : IntoOp a b1 b2 → @@ -217,8 +217,8 @@ Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?later_and ?later_sep. Qed. Global Instance into_and_big_sepM `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m : (∀ k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) → - IntoAnd p ([★ map] k ↦ x ∈ m, Φ k x) - ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x). + IntoAnd p ([∗ map] k ↦ x ∈ m, Φ k x) + ([∗ map] k ↦ x ∈ m, Ψ1 k x) ([∗ map] k ↦ x ∈ m, Ψ2 k x). Proof. rewrite /IntoAnd=> HΦ. destruct p. - apply and_intro; apply big_sepM_mono; auto. @@ -228,7 +228,7 @@ Proof. Qed. Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X : (∀ x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) → - IntoAnd p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x). + IntoAnd p ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ1 x) ([∗ set] x ∈ X, Ψ2 x). Proof. rewrite /IntoAnd=> HΦ. destruct p. - apply and_intro; apply big_sepS_mono; auto. @@ -243,18 +243,18 @@ Proof. by rewrite /Frame right_id. Qed. Global Instance frame_here_pure φ Q : FromPure Q φ → Frame (■ φ) Q True. Proof. rewrite /FromPure /Frame=> ->. by rewrite right_id. Qed. -Class MakeSep (P Q PQ : uPred M) := make_sep : P ★ Q ⊣⊢ PQ. +Class MakeSep (P Q PQ : uPred M) := make_sep : P ∗ Q ⊣⊢ PQ. Global Instance make_sep_true_l P : MakeSep True P P. Proof. by rewrite /MakeSep left_id. Qed. Global Instance make_sep_true_r P : MakeSep P True P. Proof. by rewrite /MakeSep right_id. Qed. -Global Instance make_sep_default P Q : MakeSep P Q (P ★ Q) | 100. +Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100. Proof. done. Qed. Global Instance frame_sep_l R P1 P2 Q Q' : - Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9. + Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ∗ P2) Q' | 9. Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed. Global Instance frame_sep_r R P1 P2 Q Q' : - Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10. + Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ∗ P2) Q' | 10. Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed. Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ. @@ -283,7 +283,7 @@ Global Instance frame_or R P1 P2 Q1 Q2 Q : Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed. Global Instance frame_wand R P1 P2 Q2 : - Frame R P2 Q2 → Frame R (P1 -★ P2) (P1 -★ Q2). + Frame R P2 Q2 → Frame R (P1 -∗ P2) (P1 -∗ Q2). Proof. rewrite /Frame=> ?. apply wand_intro_l. by rewrite assoc (comm _ P1) -assoc wand_elim_r. @@ -370,7 +370,7 @@ Proof. apply except_0_intro. Qed. (* ElimModal *) Global Instance elim_modal_wand P P' Q Q' R : - ElimModal P P' Q Q' → ElimModal P P' (R -★ Q) (R -★ Q'). + ElimModal P P' Q Q' → ElimModal P P' (R -∗ Q) (R -∗ Q'). Proof. rewrite /ElimModal=> H. apply wand_intro_r. by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l. @@ -389,13 +389,13 @@ Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed. Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q. Proof. - intros. rewrite /ElimModal (except_0_intro (_ -★ _)). + intros. rewrite /ElimModal (except_0_intro (_ -∗ _)). by rewrite -except_0_sep wand_elim_r. Qed. Global Instance elim_modal_timeless_bupd P Q : TimelessP P → IsExcept0 Q → ElimModal (▷ P) P Q Q. Proof. - intros. rewrite /ElimModal (except_0_intro (_ -★ _)) (timelessP P). + intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (timelessP P). by rewrite -except_0_sep wand_elim_r. Qed. diff --git a/proofmode/classes.v b/proofmode/classes.v index e40a68362c76c0bdd34b335b7de2bad6bd1456a2..c17d464bee33ba18d7d2a407057cee8c07b7529a 100644 --- a/proofmode/classes.v +++ b/proofmode/classes.v @@ -23,20 +23,20 @@ Global Arguments into_later _ _ {_}. Class FromLater (P Q : uPred M) := from_later : ▷ Q ⊢ P. Global Arguments from_later _ _ {_}. -Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -★ Q. +Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q. Global Arguments into_wand : clear implicits. Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P. Global Arguments from_and : clear implicits. -Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ★ Q2 ⊢ P. +Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ∗ Q2 ⊢ P. Global Arguments from_sep : clear implicits. Class IntoAnd (p : bool) (P Q1 Q2 : uPred M) := - into_and : P ⊢ if p then Q1 ∧ Q2 else Q1 ★ Q2. + into_and : P ⊢ if p then Q1 ∧ Q2 else Q1 ∗ Q2. Global Arguments into_and : clear implicits. -Lemma mk_into_and_sep p P Q1 Q2 : (P ⊢ Q1 ★ Q2) → IntoAnd p P Q1 Q2. +Lemma mk_into_and_sep p P Q1 Q2 : (P ⊢ Q1 ∗ Q2) → IntoAnd p P Q1 Q2. Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed. Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1 ⋅ b2 ≡ a. @@ -45,7 +45,7 @@ Global Arguments from_op {_} _ _ _ {_}. Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2. Global Arguments into_op {_} _ _ _ {_}. -Class Frame (R P Q : uPred M) := frame : R ★ Q ⊢ P. +Class Frame (R P Q : uPred M) := frame : R ∗ Q ⊢ P. Global Arguments frame : clear implicits. Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P. @@ -66,7 +66,7 @@ Class IntoModal (P Q : uPred M) := into_modal : P ⊢ Q. Global Arguments into_modal : clear implicits. Class ElimModal (P P' : uPred M) (Q Q' : uPred M) := - elim_modal : P ★ (P' -★ Q') ⊢ Q. + elim_modal : P ∗ (P' -∗ Q') ⊢ Q. Global Arguments elim_modal _ _ _ _ {_}. Lemma elim_modal_dummy P Q : ElimModal P P Q Q. diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v index 39abdb1186be5379abb0a580c053fa1ea4636c8b..a98f650d408fc2eabf2d3ad7ad2e6c55218f347e 100644 --- a/proofmode/coq_tactics.v +++ b/proofmode/coq_tactics.v @@ -19,7 +19,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 := { @@ -110,7 +110,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 : @@ -123,31 +123,31 @@ Proof. Qed. Lemma envs_lookup_sound Δ i p P : - envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ★ envs_delete i p Δ. + envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ envs_delete i p Δ. Proof. rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - rewrite (env_lookup_perm Γp) //= always_sep. - ecancel [□ [★] _; □ P; [★] Γs]%I; apply pure_intro. + ecancel [□ [∗] _; □ P; [∗] Γs]%I; apply pure_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; [★] (env_delete _ _)]%I; apply pure_intro. + ecancel [□ [∗] _; P; [∗] (env_delete _ _)]%I; apply pure_intro. destruct Hwf; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh. Qed. Lemma envs_lookup_sound' Δ i p P : - envs_lookup i Δ = Some (p,P) → Δ ⊢ P ★ envs_delete i p Δ. + envs_lookup i Δ = Some (p,P) → Δ ⊢ P ∗ envs_delete i p Δ. Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed. Lemma envs_lookup_persistent_sound Δ i P : - envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ★ Δ. + envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ. Proof. intros. apply (always_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l. Qed. Lemma envs_lookup_split Δ i p P : - envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ★ (□?p P -★ Δ). + envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ (□?p P -∗ Δ). Proof. rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. @@ -160,10 +160,10 @@ Proof. Qed. Lemma envs_lookup_delete_sound Δ Δ' i p P : - envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ★ Δ'. + envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ∗ Δ'. Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed. Lemma envs_lookup_delete_sound' Δ Δ' i p P : - envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ P ★ Δ'. + envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ P ∗ Δ'. Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed. Lemma envs_lookup_snoc Δ i p P : @@ -180,7 +180,7 @@ Proof. Qed. Lemma envs_snoc_sound Δ p i P : - envs_lookup i Δ = None → Δ ⊢ □?p P -★ envs_snoc Δ p i P. + envs_lookup i Δ = None → Δ ⊢ □?p P -∗ envs_snoc Δ p i P. Proof. rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=. @@ -195,7 +195,7 @@ Proof. + solve_sep_entails. 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 pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=. @@ -218,7 +218,7 @@ Qed. Lemma envs_simple_replace_sound' Δ Δ' i p Γ : envs_simple_replace i p Γ Δ = Some Δ' → - envs_delete i p Δ ⊢ □?p [★] Γ -★ Δ'. + envs_delete i p Δ ⊢ □?p [∗] Γ -∗ Δ'. Proof. rewrite /envs_simple_replace /envs_delete /of_envs=> ?. apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=. @@ -241,11 +241,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 [★] Γ -★ Δ'). + Δ ⊢ □?p P ∗ (□?p [∗] Γ -∗ Δ'). 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 [★] Γ -★ Δ'. + envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ □?q [∗] Γ -∗ Δ'. Proof. rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq. - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'. @@ -254,7 +254,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 [★] Γ -★ Δ'). + Δ ⊢ □?p P ∗ (□?q [∗] Γ -∗ Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed. Lemma envs_lookup_envs_clear_spatial Δ j : @@ -266,7 +266,7 @@ Proof. by destruct (Γs !! j). Qed. -Lemma envs_clear_spatial_sound Δ : Δ ⊢ envs_clear_spatial Δ ★ [★] env_spatial Δ. +Lemma envs_clear_spatial_sound Δ : Δ ⊢ envs_clear_spatial Δ ∗ [∗] env_spatial Δ. Proof. rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l=> Hwf. rewrite right_id -assoc; apply sep_intro_True_l; [apply pure_intro|done]. @@ -298,7 +298,7 @@ Qed. Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' : (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) → - envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') → Δ1 ★ Δ2 ⊢ Δ1' ★ Δ2'. + envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') → Δ1 ∗ Δ2 ⊢ Δ1' ∗ Δ2'. Proof. revert Δ1 Δ2 Δ1' Δ2'. induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|]. @@ -314,7 +314,7 @@ Proof. rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto. Qed. Lemma envs_split_sound Δ lr js Δ1 Δ2 : - envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ★ Δ2. + envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ∗ Δ2. Proof. rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ). rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r. @@ -481,19 +481,19 @@ Proof. Qed. Lemma tac_wand_intro Δ Δ' i P Q : - envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -★ Q. + envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -∗ Q. Proof. intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ. Qed. Lemma tac_wand_intro_persistent Δ Δ' i P P' Q : IntoPersistentP P P' → envs_app true (Esnoc Enil i P') Δ = Some Δ' → - (Δ' ⊢ Q) → Δ ⊢ P -★ Q. + (Δ' ⊢ Q) → Δ ⊢ P -∗ Q. Proof. intros. rewrite envs_app_sound //; simpl. rewrite right_id. by apply wand_mono. Qed. -Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q. +Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -∗ Q. Proof. intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l. Qed. @@ -578,7 +578,7 @@ Qed. Lemma tac_revert Δ Δ' i p P Q : envs_lookup_delete i Δ = Some (p,P,Δ') → - (Δ' ⊢ (if p then □ P else P) -★ Q) → Δ ⊢ Q. + (Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q. Proof. intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. by rewrite HQ /uPred_always_if wand_elim_r. @@ -672,9 +672,9 @@ Proof. rewrite sep_elim_l HPxy always_and_sep_r. rewrite (envs_simple_replace_sound _ _ j) //; simpl. rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr. - - apply (internal_eq_rewrite x y (λ y, □?q Φ y -★ Δ')%I); + - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I); eauto with I. solve_proper. - - apply (internal_eq_rewrite y x (λ y, □?q Φ y -★ Δ')%I); + - apply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ Δ')%I); eauto using internal_eq_sym with I. solve_proper. Qed. diff --git a/proofmode/notation.v b/proofmode/notation.v index 638cf631d10fd66e9a00bca213bc8fae4c035ed4..cde1ce71618589ab3c63b1c12d4edf1dbec452c9 100644 --- a/proofmode/notation.v +++ b/proofmode/notation.v @@ -10,15 +10,15 @@ Notation "​" := Enil (format "​") : proof_scope. Notation "Γ ​ H : P" := (Esnoc Γ H P) (at level 1, P at level 200, left associativity, format "Γ ​ H : P '//'") : proof_scope. -Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" := +Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" := (of_envs (Envs Γ Δ) ⊢ Q%I) (at level 1, Q at level 200, left associativity, - format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") : + format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'") : C_scope. -Notation "Δ '--------------------------------------' ★ Q" := +Notation "Δ '--------------------------------------' ∗ Q" := (of_envs (Envs Enil Δ) ⊢ Q%I) (at level 1, Q at level 200, left associativity, - format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope. + format "Δ '--------------------------------------' ∗ '//' Q '//'") : C_scope. Notation "Γ '--------------------------------------' □ Q" := (of_envs (Envs Γ Enil) ⊢ Q%I) (at level 1, Q at level 200, left associativity, diff --git a/proofmode/sel_patterns.v b/proofmode/sel_patterns.v index 583b49dfb9a9de124678ac14c646b32050fefe5a..1f1f9229d0b8490df5119f0f97d939f81b08d4d5 100644 --- a/proofmode/sel_patterns.v +++ b/proofmode/sel_patterns.v @@ -23,7 +23,7 @@ Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat : | String " " s => parse_go s (cons_name kn k) "" | String "%" s => parse_go s (SelPure :: cons_name kn k) "" | String "#" s => parse_go s (SelPersistent :: cons_name kn k) "" - | String (Ascii.Ascii false true false false false true true true) (* unicode ★ *) + | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *) (String (Ascii.Ascii false false false true true false false true) (String (Ascii.Ascii true false true false false false false true) s)) => parse_go s (SelSpatial :: cons_name kn k) "" diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 721b3f714a718e9e9cc5ec0310ad897ff94292a3..03782f521d8c85b980fd5388122ba1b3a0308a4d 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -357,7 +357,7 @@ Tactic Notation "iSpecialize" open_constr(t) "#" := is a Coq term whose type is of the following shape: - [∀ (x_1 : A_1) .. (x_n : A_n), True ⊢ Q] -- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -★ P2] +- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -∗ P2] - [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊣⊢ P2], in which case [Q] becomes [P1 ↔ P2] The tactic instantiates each dependent argument [x_i] with an evar and generates @@ -685,7 +685,7 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := |(* (?P → _) *) eapply tac_impl_intro_pure; [let P := match goal with |- IntoPure ?P _ => P end in apply _ || fail "iIntro:" P "not pure"|] - |(* (?P -★ _) *) eapply tac_wand_intro_pure; + |(* (?P -∗ _) *) eapply tac_wand_intro_pure; [let P := match goal with |- IntoPure ?P _ => P end in apply _ || fail "iIntro:" P "not pure"|]]; intros x. @@ -696,7 +696,7 @@ Local Tactic Notation "iIntro" constr(H) := first [reflexivity || fail 1 "iIntro: introducing" H "into non-empty spatial context" |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] - | (* (_ -★ _) *) + | (* (_ -∗ _) *) eapply tac_wand_intro with _ H; (* (i:=H) *) [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|] | fail 1 "iIntro: nothing to introduce" ]. @@ -707,7 +707,7 @@ Local Tactic Notation "iIntro" "#" constr(H) := first [let P := match goal with |- IntoPersistentP ?P _ => P end in apply _ || fail 1 "iIntro: " P " not persistent" |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|] - | (* (?P -★ _) *) + | (* (?P -∗ _) *) eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *) [let P := match goal with |- IntoPersistentP ?P _ => P end in apply _ || fail 1 "iIntro: " P " not persistent" @@ -723,7 +723,7 @@ Local Tactic Notation "iIntroForall" := Local Tactic Notation "iIntro" := lazymatch goal with | |- _ → ?P => intro - | |- _ ⊢ (_ -★ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H + | |- _ ⊢ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H end. @@ -956,33 +956,33 @@ Tactic Notation "iInductionCore" constr(x) induction x as pat; fix_ihs. Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) := - iRevertIntros "★" with (iInductionCore x as pat IH). + iRevertIntros "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ")" := - iRevertIntros(x1) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ")" := - iRevertIntros(x1 x2) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1 x2) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ident(x3) ")" := - iRevertIntros(x1 x2 x3) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1 x2 x3) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" := - iRevertIntros(x1 x2 x3 x4) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1 x2 x3 x4) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")" := - iRevertIntros(x1 x2 x3 x4 x5) "★" with (iInductionCore x as aat IH). + iRevertIntros(x1 x2 x3 x4 x5) "∗" with (iInductionCore x as aat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")" := - iRevertIntros(x1 x2 x3 x4 x5 x6) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1 x2 x3 x4 x5 x6) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" := - iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" := - iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "★" with (iInductionCore x as pat IH). + iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "∗" with (iInductionCore x as pat IH). Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) "forall" constr(Hs) := @@ -1023,29 +1023,29 @@ Tactic Notation "iLöbCore" "as" constr (IH) := |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|]. Tactic Notation "iLöb" "as" constr (IH) := - iRevertIntros "★" with (iLöbCore as IH). + iRevertIntros "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" := - iRevertIntros(x1) "★" with (iLöbCore as IH). + iRevertIntros(x1) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")" := - iRevertIntros(x1 x2) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ident(x3) ")" := - iRevertIntros(x1 x2 x3) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2 x3) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" := - iRevertIntros(x1 x2 x3 x4) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2 x3 x4) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")" := - iRevertIntros(x1 x2 x3 x4 x5) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2 x3 x4 x5) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")" := - iRevertIntros(x1 x2 x3 x4 x5 x6) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2 x3 x4 x5 x6) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" := - iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" := - iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "★" with (iLöbCore as IH). + iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "∗" with (iLöbCore as IH). Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) := iRevertIntros Hs with (iLöbCore as IH). @@ -1203,12 +1203,12 @@ Hint Extern 0 (of_envs _ ⊢ _) => iAssumption. Hint Extern 0 (of_envs _ ⊢ _) => progress iIntros. Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *) -(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ★ _)%I) => ...], +(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ∗ _)%I) => ...], but then [eauto] mysteriously fails. See bug 4762 *) Hint Extern 1 (of_envs _ ⊢ _) => match goal with | |- _ ⊢ _ ∧ _ => iSplit - | |- _ ⊢ _ ★ _ => iSplit + | |- _ ⊢ _ ∗ _ => iSplit | |- _ ⊢ ▷ _ => iNext | |- _ ⊢ □ _ => iClear "*"; iAlways | |- _ ⊢ ∃ _, _ => iExists _ diff --git a/tests/barrier_client.v b/tests/barrier_client.v index e29e8cbb59ad1e391f54c422550a8c0d4b74f3b3..0fe8dea52acd21fc15ac7376cd034a79c80bd770 100644 --- a/tests/barrier_client.v +++ b/tests/barrier_client.v @@ -17,16 +17,16 @@ Section client. Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace). Definition y_inv (q : Qp) (l : loc) : iProp Σ := - (∃ f : val, l ↦{q} f ★ □ ∀ n : Z, WP f #n {{ v, v = #(n + 42) }})%I. + (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, v = #(n + 42) }})%I. - Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ★ y_inv (q/2) l). + Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ∗ y_inv (q/2) l). Proof. iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]". iSplitL "Hl1"; iExists f; by iSplitL; try iAlways. Qed. Lemma worker_safe q (n : Z) (b y : loc) : - heap_ctx ★ recv N b (y_inv q y) ⊢ WP worker n #b #y {{ _, True }}. + heap_ctx ∗ recv N b (y_inv q y) ⊢ WP worker n #b #y {{ _, True }}. Proof. iIntros "[#Hh Hrecv]". wp_lam. wp_let. wp_apply (wait_spec with "[- \$Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]". diff --git a/tests/counter.v b/tests/counter.v index 7056e303ccc6b4ec6ecbc956399033ab881d68bd..7b2c15763c3377e5215aed952f5031173109436e 100644 --- a/tests/counter.v +++ b/tests/counter.v @@ -82,7 +82,7 @@ Context `{!heapG Σ, !counterG Σ}. Implicit Types l : loc. Definition I (γ : gname) (l : loc) : iProp Σ := - (∃ c : nat, l ↦ #c ★ own γ (Auth c))%I. + (∃ c : nat, l ↦ #c ∗ own γ (Auth c))%I. Definition C (l : loc) (n : nat) : iProp Σ := (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ inv N (I γ l) ∧ own γ (Frag n))%I. diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v index 2abc3576672b5ddb0a36598748fef86e839f4068..581cf8a16c77c80684184a6f78e1ced16dc7d085 100644 --- a/tests/joining_existentials.v +++ b/tests/joining_existentials.v @@ -29,10 +29,10 @@ Context (N : namespace). Local Notation X := (F (iProp Σ)). Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ := - (∃ x, own γ (Shot x) ★ Φ x)%I. + (∃ x, own γ (Shot x) ∗ Φ x)%I. Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} : - recv N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) + recv N l (barrier_res γ Φ) ∗ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}. Proof. iIntros "[Hl #He]". wp_apply (wait_spec with "[- \$Hl]"); simpl. @@ -42,16 +42,16 @@ Proof. Qed. Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ). -Context {Φ_split : ∀ x, Φ x ⊢ (Φ1 x ★ Φ2 x)}. -Context {Ψ_join : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}. +Context {Φ_split : ∀ x, Φ x ⊢ (Φ1 x ∗ Φ2 x)}. +Context {Ψ_join : ∀ x, (Ψ1 x ∗ Ψ2 x) ⊢ Ψ x}. -Lemma P_res_split γ : barrier_res γ Φ ⊢ barrier_res γ Φ1 ★ barrier_res γ Φ2. +Lemma P_res_split γ : barrier_res γ Φ ⊢ barrier_res γ Φ1 ∗ barrier_res γ Φ2. Proof. iDestruct 1 as (x) "[#Hγ Hx]". iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit. Qed. -Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_res γ Ψ. +Lemma Q_res_join γ : barrier_res γ Ψ1 ∗ barrier_res γ Ψ2 ⊢ ▷ barrier_res γ Ψ. Proof. iIntros "[Hγ Hγ']"; iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']". @@ -68,17 +68,17 @@ Qed. Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} : heapN ⊥ N → - heap_ctx ★ P - ★ {{ P }} eM {{ _, ∃ x, Φ x }} - ★ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) - ★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) + heap_ctx ∗ P + ∗ {{ P }} eM {{ _, ∃ x, Φ x }} + ∗ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) + ∗ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) ⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}. Proof. iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client. iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done. wp_apply (newbarrier_spec N (barrier_res γ Φ) with "Hh"); auto. iIntros (l) "[Hr Hs]". - set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I). + set (workers_post (v : val) := (barrier_res γ Ψ1 ∗ barrier_res γ Ψ2)%I). wp_let. wp_apply (wp_par (λ _, True)%I workers_post with "[- \$Hh]"). iSplitL "HP Hs Hγ"; [|iSplitL "Hr"]. - wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"]. diff --git a/tests/list_reverse.v b/tests/list_reverse.v index 93a83113d5ef4a5164075ff3b044344aaf65b8ad..5af0d7fab958603044af441939d79362c606aeef 100644 --- a/tests/list_reverse.v +++ b/tests/list_reverse.v @@ -11,7 +11,7 @@ Implicit Types l : loc. Fixpoint is_list (hd : val) (xs : list val) : iProp Σ := match xs with | [] => hd = NONEV - | x :: xs => ∃ l hd', hd = SOMEV #l ★ l ↦ (x,hd') ★ is_list hd' xs + | x :: xs => ∃ l hd', hd = SOMEV #l ∗ l ↦ (x,hd') ∗ is_list hd' xs end%I. Definition rev : val := @@ -27,8 +27,8 @@ Definition rev : val := Global Opaque rev. Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp Σ) : - heap_ctx ★ is_list hd xs ★ is_list acc ys ★ - (∀ w, is_list w (reverse xs ++ ys) -★ Φ w) + heap_ctx ∗ is_list hd xs ∗ is_list acc ys ∗ + (∀ w, is_list w (reverse xs ++ ys) -∗ Φ w) ⊢ WP rev hd acc {{ Φ }}. Proof. iIntros "(#Hh & Hxs & Hys & HΦ)". @@ -43,7 +43,7 @@ Proof. Qed. Lemma rev_wp hd xs (Φ : val → iProp Σ) : - heap_ctx ★ is_list hd xs ★ (∀ w, is_list w (reverse xs) -★ Φ w) + heap_ctx ∗ is_list hd xs ∗ (∀ w, is_list w (reverse xs) -∗ Φ w) ⊢ WP rev hd (InjL #()) {{ Φ }}. Proof. iIntros "(#Hh & Hxs & HΦ)". diff --git a/tests/one_shot.v b/tests/one_shot.v index cfdaecc0d7d65d69725a09230f3fe2f357d05cc1..dea6c813d7ce326c0087245b6843283e091afca9 100644 --- a/tests/one_shot.v +++ b/tests/one_shot.v @@ -33,12 +33,12 @@ Section proof. Context `{!heapG Σ, !one_shotG Σ} (N : namespace) (HN : heapN ⊥ N). Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ := - (l ↦ NONEV ★ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ★ own γ (Shot n))%I. + (l ↦ NONEV ∗ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I. Lemma wp_one_shot (Φ : val → iProp Σ) : - heap_ctx ★ (∀ f1 f2 : val, - (∀ n : Z, □ WP f1 #n {{ w, w = #true ∨ w = #false }}) ★ - □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -★ Φ (f1,f2)%V) + heap_ctx ∗ (∀ f1 f2 : val, + (∀ n : Z, □ WP f1 #n {{ w, w = #true ∨ w = #false }}) ∗ + □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V) ⊢ WP one_shot_example #() {{ Φ }}. Proof. iIntros "[#? Hf] /=". @@ -57,14 +57,14 @@ Proof. rewrite /one_shot_inv; eauto 10. - iIntros "!#". wp_seq. wp_bind (! _)%E. iInv N as ">Hγ" "Hclose". - iAssert (∃ v, l ↦ v ★ ((v = NONEV ★ own γ Pending) ∨ - ∃ n : Z, v = SOMEV #n ★ own γ (Shot n)))%I with "[Hγ]" as "Hv". + iAssert (∃ v, l ↦ v ∗ ((v = NONEV ∗ own γ Pending) ∨ + ∃ n : Z, v = SOMEV #n ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv". { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]". + iExists NONEV. iFrame. eauto. + iExists (SOMEV #m). iFrame. eauto. } iDestruct "Hv" as (v) "[Hl Hv]". wp_load. - iAssert (one_shot_inv γ l ★ (v = NONEV ∨ ∃ n : Z, - v = SOMEV #n ★ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]". + iAssert (one_shot_inv γ l ∗ (v = NONEV ∨ ∃ n : Z, + v = SOMEV #n ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]". { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst. + iSplit. iLeft; by iSplitL "Hl". eauto. + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. } @@ -86,7 +86,7 @@ Qed. Lemma ht_one_shot (Φ : val → iProp Σ) : heap_ctx ⊢ {{ True }} one_shot_example #() {{ ff, - (∀ n : Z, {{ True }} Fst ff #n {{ w, w = #true ∨ w = #false }}) ★ + (∀ n : Z, {{ True }} Fst ff #n {{ w, w = #true ∨ w = #false }}) ∗ {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }} }}. Proof. diff --git a/tests/proofmode.v b/tests/proofmode.v index fa970acf34daa9a565051e03e291b8028cf2d1af..97bec6d8bde135a52fb75557725bd0e9086d2a8e 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -14,11 +14,11 @@ Qed. Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat → uPred M) : True ⊢ ∀ (x y : nat) a b, x ≡ y → - □ (uPred_ownM (a ⋅ b) -★ - (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -★ - □ ▷ (∀ z, P2 z ∨ True → P2 z) -★ - ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -★ - ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b)). + □ (uPred_ownM (a ⋅ b) -∗ + (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗ + □ ▷ (∀ z, P2 z ∨ True → P2 z) -∗ + ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -∗ + ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)). Proof. iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst. { iLeft. by iNext. } @@ -37,8 +37,8 @@ Proof. Qed. Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M): - P2 ★ (P3 ★ Q) ★ True ★ P1 ★ P2 ★ (P4 ★ (∃ x:nat, P5 x ∨ P3)) ★ True - ⊢ P1 -★ (True ★ True) -★ (((P2 ∧ False ∨ P2 ∧ 0 = 0) ★ P3) ★ Q ★ P1 ★ True) ∧ + P2 ∗ (P3 ∗ Q) ∗ True ∗ P1 ∗ P2 ∗ (P4 ∗ (∃ x:nat, P5 x ∨ P3)) ∗ True + ⊢ P1 -∗ (True ∗ True) -∗ (((P2 ∧ False ∨ P2 ∧ 0 = 0) ∗ P3) ∗ Q ∗ P1 ∗ True) ∧ (P2 ∨ False) ∧ (False → P5 0). Proof. (* Intro-patterns do something :) *) @@ -54,7 +54,7 @@ Proof. Qed. Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) : - P1 ★ P2 ★ P3 ⊢ ▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3). + P1 ∗ P2 ∗ P3 ⊢ ▷ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ x = 0) ∨ P3). Proof. iIntros "(\$ & \$ & H)". iFrame "H". iNext. by iExists 0. Qed. Definition foo {M} (P : uPred M) := (P → P)%I. @@ -64,7 +64,7 @@ Lemma demo_4 (M : ucmraT) : True ⊢ @bar M. Proof. iIntros. iIntros (P) "HP". done. Qed. Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) : - (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)). + (∀ z, P → z ≡ y) ⊢ (P -∗ (x,x) ≡ (y,x)). Proof. iIntros "H1 H2". iRewrite (uPred.internal_eq_sym x x with "[#]"); first done. @@ -81,7 +81,7 @@ Proof. by iIntros "# _". Qed. -Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ★ (Q1 ∧ Q2) ⊢ P ★ Q1. +Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ∗ (Q1 ∧ Q2) ⊢ P ∗ Q1. Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed. Section iris. @@ -91,7 +91,7 @@ Section iris. Lemma demo_8 N E P Q R : nclose N ⊆ E → - (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q ={E}=★ R. + (True -∗ P -∗ inv N Q -∗ True -∗ R) ⊢ P -∗ ▷ Q ={E}=∗ R. Proof. iIntros (?) "H HP HQ". iApply ("H" with "[#] HP >[HQ] >"). diff --git a/tests/tree_sum.v b/tests/tree_sum.v index 4fec2a4f51f63caca261da7fb61f9c227a618fec..ff0978afdc3a9bed68ad9ae2b1e10050f47436bb 100644 --- a/tests/tree_sum.v +++ b/tests/tree_sum.v @@ -12,7 +12,7 @@ Fixpoint is_tree `{!heapG Σ} (v : val) (t : tree) : iProp Σ := | leaf n => v = InjLV #n | node tl tr => ∃ (ll lr : loc) (vl vr : val), - v = InjRV (#ll,#lr) ★ ll ↦ vl ★ is_tree vl tl ★ lr ↦ vr ★ is_tree vr tr + v = InjRV (#ll,#lr) ∗ ll ↦ vl ∗ is_tree vl tl ∗ lr ↦ vr ∗ is_tree vr tr end%I. Fixpoint sum (t : tree) : Z := @@ -36,8 +36,8 @@ Definition sum' : val := λ: "t", Global Opaque sum_loop sum'. Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) : - heap_ctx ★ l ↦ #n ★ is_tree v t - ★ (l ↦ #(sum t + n) -★ is_tree v t -★ Φ #()) + heap_ctx ∗ l ↦ #n ∗ is_tree v t + ∗ (l ↦ #(sum t + n) -∗ is_tree v t -∗ Φ #()) ⊢ WP sum_loop v #l {{ Φ }}. Proof. iIntros "(#Hh & Hl & Ht & HΦ)". @@ -57,7 +57,7 @@ Proof. Qed. Lemma sum_wp `{!heapG Σ} v t Φ : - heap_ctx ★ is_tree v t ★ (is_tree v t -★ Φ #(sum t)) + heap_ctx ∗ is_tree v t ∗ (is_tree v t -∗ Φ #(sum t)) ⊢ WP sum' v {{ Φ }}. Proof. iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=.