From cb4fd1bbcc30278e634e1b30c3a66e96b0028ed8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Feb 2016 10:03:21 +0100
Subject: [PATCH] change notation for frame-preserving updates
---
iris/pviewshifts.v | 4 ++--
iris/viewshifts.v | 4 ++--
iris/wsat.v | 2 +-
modures/auth.v | 6 +++---
modures/cmra.v | 28 ++++++++++++++--------------
modures/dra.v | 2 +-
modures/excl.v | 4 ++--
modures/fin_maps.v | 10 +++++-----
modures/option.v | 6 +++---
modures/sts.v | 2 +-
10 files changed, 34 insertions(+), 34 deletions(-)
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index e84941e58..4ff9bf80f 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -97,7 +97,7 @@ Proof.
* apply uPred_weaken with r n; auto.
Qed.
Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
- m â‡: P → ownG m ⊑ pvs E E (∃ m', â– P m' ∧ ownG m').
+ m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■P m' ∧ ownG m').
Proof.
intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P)
@@ -136,7 +136,7 @@ Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P.
Proof.
intros; rewrite (union_difference_L E1 E2) //; apply pvs_mask_frame; auto.
Qed.
-Lemma pvs_update E m m' : m ⇠m' → ownG m ⊑ pvs E E (ownG m').
+Lemma pvs_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
Proof.
intros; rewrite ->(pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
diff --git a/iris/viewshifts.v b/iris/viewshifts.v
index 7e6b3640f..55a54e1c1 100644
--- a/iris/viewshifts.v
+++ b/iris/viewshifts.v
@@ -87,9 +87,9 @@ Proof.
apply vs_close.
Qed.
Lemma vs_updateP E m (P : iGst Λ Σ → Prop) :
- m â‡: P → ownG m >{E}> (∃ m', â– P m' ∧ ownG m').
+ m ~~>: P → ownG m >{E}> (∃ m', ■P m' ∧ ownG m').
Proof. by intros; apply vs_alt, pvs_updateP. Qed.
-Lemma vs_update E m m' : m ⇠m' → ownG m >{E}> ownG m'.
+Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'.
Proof. by intros; apply vs_alt, pvs_update. Qed.
Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■(i ∈ E) ∧ inv i P).
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
diff --git a/iris/wsat.v b/iris/wsat.v
index 9b57849ed..996842ca5 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -125,7 +125,7 @@ Proof.
by constructor; split_ands'; try (rewrite /= -associative Hpst').
Qed.
Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
- m1 ≼{S n} gst r → m1 â‡: P →
+ m1 ≼{S n} gst r → m1 ~~>: P →
wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
Proof.
intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
diff --git a/modures/auth.v b/modures/auth.v
index 53ffa01e8..c99b37013 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -148,7 +148,7 @@ Proof. done. Qed.
Lemma auth_update a a' b b' :
(∀ n af, ✓{n} a → a ={n}= a' ⋅ af → b ={n}= b' ⋅ af ∧ ✓{n} b) →
- ◠a ⋅ ◯ a' ⇠◠b ⋅ ◯ b'.
+ â— a â‹… â—¯ a' ~~> â— b â‹… â—¯ b'.
Proof.
move=> Hab [[] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
destruct (Hab (S n) (bf1 â‹… bf2)) as [Ha' ?]; auto.
@@ -156,13 +156,13 @@ Proof.
split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
Qed.
Lemma auth_update_op_l a a' b :
- ✓ (b ⋅ a) → ◠a ⋅ ◯ a' ⇠◠(b ⋅ a) ⋅ ◯ (b ⋅ a').
+ ✓ (b ⋅ a) → ◠a ⋅ ◯ a' ~~> ◠(b ⋅ a) ⋅ ◯ (b ⋅ a').
Proof.
intros; apply auth_update.
by intros n af ? Ha; split; [by rewrite Ha associative|].
Qed.
Lemma auth_update_op_r a a' b :
- ✓ (a ⋅ b) → ◠a ⋅ ◯ a' ⇠◠(a ⋅ b) ⋅ ◯ (a' ⋅ b).
+ ✓ (a ⋅ b) → ◠a ⋅ ◯ a' ~~> ◠(a ⋅ b) ⋅ ◯ (a' ⋅ b).
Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
End cmra.
diff --git a/modures/cmra.v b/modures/cmra.v
index c5d385f67..44d02b431 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -144,10 +144,10 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z).
Instance: Params (@cmra_updateP) 1.
-Infix "â‡:" := cmra_updateP (at level 70).
+Infix "~~>:" := cmra_updateP (at level 70).
Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z).
-Infix "â‡" := cmra_update (at level 70).
+Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
(** * Properties **)
@@ -323,24 +323,24 @@ End identity.
(** ** Updates *)
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
-Lemma cmra_update_updateP x y : x ⇠y ↔ x â‡: (y =).
+Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
Proof.
split.
* by intros Hx z ?; exists y; split; [done|apply (Hx z)].
* by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
Qed.
-Lemma cmra_updateP_id (P : A → Prop) x : P x → x â‡: P.
+Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
Proof. by intros ? z n ?; exists x. Qed.
Lemma cmra_updateP_compose (P Q : A → Prop) x :
- x â‡: P → (∀ y, P y → y â‡: Q) → x â‡: Q.
+ x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
Proof.
intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y).
Qed.
-Lemma cmra_updateP_weaken (P Q : A → Prop) x : x â‡: P → (∀ y, P y → Q y) → x â‡: Q.
+Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
- x1 â‡: P1 → x2 â‡: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 â‹… y2)) → x1 â‹… x2 â‡: Q.
+ x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q.
Proof.
intros Hx1 Hx2 Hy z n ?.
destruct (Hx1 (x2 â‹… z) n) as (y1&?&?); first by rewrite associative.
@@ -349,9 +349,9 @@ Proof.
exists (y1 â‹… y2); split; last rewrite (commutative _ y1) -associative; auto.
Qed.
Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
- x1 â‡: P1 → x2 â‡: P2 → x1 â‹… x2 â‡: λ y, ∃ y1 y2, y = y1 â‹… y2 ∧ P1 y1 ∧ P2 y2.
+ x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
Proof. eauto 10 using cmra_updateP_op. Qed.
-Lemma cmra_update_op x1 x2 y1 y2 : x1 ⇠y1 → x2 ⇠y2 → x1 ⋅ x2 ⇠y1 ⋅ y2.
+Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2.
Proof.
rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
@@ -422,10 +422,10 @@ Section discrete.
Definition discreteRA : cmraT :=
CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
- (∀ z, ✓ (x â‹… z) → ∃ y, P y ∧ ✓ (y â‹… z)) → x â‡: P.
+ (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
Proof. intros Hvalid z n; apply Hvalid. Qed.
Lemma discrete_update (x y : discreteRA) :
- (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ⇠y.
+ (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
Proof. intros Hvalid z n; apply Hvalid. Qed.
End discrete.
@@ -499,17 +499,17 @@ Section prod.
* by split; rewrite /=left_id.
* by intros ? [??]; split; apply (timeless _).
Qed.
- Lemma prod_update x y : x.1 ⇠y.1 → x.2 ⇠y.2 → x ⇠y.
+ Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
- x.1 â‡: P1 → x.2 â‡: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x â‡: Q.
+ x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Proof.
intros Hx1 Hx2 HP z n [??]; simpl in *.
destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto.
exists (a,b); repeat split; auto.
Qed.
Lemma prod_updateP' P1 P2 x :
- x.1 â‡: P1 → x.2 â‡: P2 → x â‡: λ y, P1 (y.1) ∧ P2 (y.2).
+ x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
Proof. eauto using prod_updateP. Qed.
End prod.
Arguments prodRA : clear implicits.
diff --git a/modures/dra.v b/modures/dra.v
index 4965a1264..933deff4a 100644
--- a/modures/dra.v
+++ b/modures/dra.v
@@ -131,7 +131,7 @@ Proof.
Qed.
Definition validityRA : cmraT := discreteRA validity_ra.
Definition validity_update (x y : validityRA) :
- (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ⇠y.
+ (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
Proof.
intros Hxy. apply discrete_update.
intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
diff --git a/modures/excl.v b/modures/excl.v
index 54389faa5..a86ccd72e 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -144,9 +144,9 @@ Proof.
Qed.
(* Updates *)
-Lemma excl_update (x : A) y : ✓ y → Excl x ⇠y.
+Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
Proof. by destruct y; intros ? [?| |]. Qed.
-Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x â‡: P.
+Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P.
Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
End excl.
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index d11b2fcee..58eb39cd1 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -193,7 +193,7 @@ Proof.
Qed.
Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
- x â‡: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m â‡: Q.
+ x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
Proof.
intros Hx%option_updateP' HP mf n Hm.
destruct (Hx (mf !! i) n) as ([y|]&?&?); try done.
@@ -203,16 +203,16 @@ Proof.
destruct (decide (i = j)); simplify_map_equality'; auto.
Qed.
Lemma map_insert_updateP' (P : A → Prop) (Q : gmap K A → Prop) m i x :
- x â‡: P → <[i:=x]>m â‡: λ m', ∃ y, m' = <[i:=y]>m ∧ P y.
+ x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y.
Proof. eauto using map_insert_updateP. Qed.
-Lemma map_insert_update m i x y : x ⇠y → <[i:=x]>m ⇠<[i:=y]>m.
+Lemma map_insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m.
Proof.
rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
Qed.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
- ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m â‡: Q.
+ ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
Proof.
intros ? HQ mf n Hm. set (i := fresh (dom (gset K) (m â‹… mf))).
assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [??].
@@ -222,7 +222,7 @@ Proof.
by apply map_insert_validN; [apply cmra_valid_validN|].
Qed.
Lemma map_updateP_alloc' m x :
- ✓ x → m â‡: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+ ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
Proof. eauto using map_updateP_alloc. Qed.
End properties.
diff --git a/modures/option.v b/modures/option.v
index 5275e5b31..a553fa1b0 100644
--- a/modures/option.v
+++ b/modures/option.v
@@ -140,7 +140,7 @@ Lemma option_op_positive_dist_r n mx my : mx ⋅ my ={n}= None → my ={n}= None
Proof. by destruct mx, my; inversion_clear 1. Qed.
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
- x â‡: P → (∀ y, P y → Q (Some y)) → Some x â‡: Q.
+ x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
Proof.
intros Hx Hy [y|] n ?.
{ destruct (Hx y n) as (y'&?&?); auto. exists (Some y'); auto. }
@@ -148,9 +148,9 @@ Proof.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
Qed.
Lemma option_updateP' (P : A → Prop) x :
- x â‡: P → Some x â‡: λ y, default False y P.
+ x ~~>: P → Some x ~~>: λ y, default False y P.
Proof. eauto using option_updateP. Qed.
-Lemma option_update x y : x ⇠y → Some x ⇠Some y.
+Lemma option_update x y : x ~~> y → Some x ~~> Some y.
Proof.
rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
Qed.
diff --git a/modures/sts.v b/modures/sts.v
index 4697c82c0..90ad94ba3 100644
--- a/modures/sts.v
+++ b/modures/sts.v
@@ -210,7 +210,7 @@ Canonical Structure stsRA := validityRA (sts R tok).
Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
Lemma sts_update s1 s2 T1 T2 :
- sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇠sts_auth s2 T2.
+ sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
Proof.
intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
--
GitLab