Commit 560bd3a9 authored by Ralf Jung's avatar Ralf Jung

change naming conventions for LocalUpdates: L is the function, Lv the validity

parent 88c1dd29
...@@ -157,12 +157,12 @@ Proof. ...@@ -157,12 +157,12 @@ Proof.
split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done]. split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
Qed. Qed.
Lemma auth_local_update f `{!LocalUpdate P f} a a' : Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
P a (f a') Lv a (L a')
a' a ~~> f a' f a. a' a ~~> L a' L a.
Proof. Proof.
intros. apply auth_update=>n af ? EQ; split; last done. intros. apply auth_update=>n af ? EQ; split; last done.
by rewrite EQ (local_updateN f) // -EQ. by rewrite EQ (local_updateN L) // -EQ.
Qed. Qed.
Lemma auth_update_op_l a a' b : Lemma auth_update_op_l a a' b :
...@@ -173,15 +173,15 @@ Lemma auth_update_op_r a a' b : ...@@ -173,15 +173,15 @@ Lemma auth_update_op_r a a' b :
Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed. Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
(* This does not seem to follow from auth_local_update. (* This does not seem to follow from auth_local_update.
The trouble is that given ✓ (f a ⋅ a'), P a The trouble is that given ✓ (L a ⋅ a'), Lv a
we need ✓ (a ⋅ a'). I think this should hold for every local update, we need ✓ (a ⋅ a'). I think this should hold for every local update,
but adding an extra axiom to local updates just for this is silly. *) but adding an extra axiom to local updates just for this is silly. *)
Lemma auth_local_update_l f `{!LocalUpdate P f} a a' : Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' :
P a (f a a') Lv a (L a a')
(a a') a ~~> (f a a') f a. (a a') a ~~> (L a a') L a.
Proof. Proof.
intros. apply auth_update=>n af ? EQ; split; last done. intros. apply auth_update=>n af ? EQ; split; last done.
by rewrite -(local_updateN f) // EQ -(local_updateN f) // -EQ. by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
Qed. Qed.
End cmra. End cmra.
......
...@@ -137,9 +137,9 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := { ...@@ -137,9 +137,9 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
}. }.
(** * Local updates *) (** * Local updates *)
Class LocalUpdate {A : cmraT} (P : A Prop) (f : A A) := { Class LocalUpdate {A : cmraT} (Lv : A Prop) (L : A A) := {
local_update_ne n :> Proper (dist n ==> dist n) f; local_update_ne n :> Proper (dist n ==> dist n) L;
local_updateN n x y : P x {n} (x y) f (x y) {n} f x y local_updateN n x y : Lv x {n} (x y) L (x y) {n} L x y
}. }.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _. Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
...@@ -322,13 +322,13 @@ Section identity. ...@@ -322,13 +322,13 @@ Section identity.
End identity. End identity.
(** ** Local updates *) (** ** Local updates *)
Global Instance local_update_proper P (f : A A) : Global Instance local_update_proper Lv (L : A A) :
LocalUpdate P f Proper (() ==> ()) f. LocalUpdate Lv L Proper (() ==> ()) L.
Proof. intros; apply (ne_proper _). Qed. Proof. intros; apply (ne_proper _). Qed.
Lemma local_update f `{!LocalUpdate P f} x y : Lemma local_update L `{!LocalUpdate Lv L} x y :
P x (x y) f (x y) f x y. Lv x (x y) L (x y) L x y.
Proof. by rewrite equiv_dist=>?? n; apply (local_updateN f). Qed. Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.
Global Instance local_update_op x : LocalUpdate (λ _, True) (op x). Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed. Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed.
......
...@@ -288,14 +288,14 @@ End freshness. ...@@ -288,14 +288,14 @@ End freshness.
(* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]}, (* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
then the frame could always own "unit x", and prevent deallocation. *) then the frame could always own "unit x", and prevent deallocation. *)
Global Instance map_alter_update `{!LocalUpdate P f} i : Global Instance map_alter_update `{!LocalUpdate Lv L} i :
LocalUpdate (λ m, x, m !! i = Some x P x) (alter f i). LocalUpdate (λ m, x, m !! i = Some x Lv x) (alter L i).
Proof. Proof.
split; first apply _. split; first apply _.
intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|]. intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
- rewrite lookup_alter !lookup_op lookup_alter Hix /=. - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
move: (Hm j); rewrite lookup_op Hix. move: (Hm j); rewrite lookup_op Hix.
case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN f). case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L).
- by rewrite lookup_op !lookup_alter_ne // lookup_op. - by rewrite lookup_op !lookup_alter_ne // lookup_op.
Qed. Qed.
End properties. End properties.
......
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