Commit cb4fd1bb authored by Ralf Jung's avatar Ralf Jung

change notation for frame-preserving updates

parent 2935cc99
......@@ -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=> ->.
......
......@@ -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.
......
......@@ -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]].
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment