Commit a20c86e3 authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent names for (local) updates.

parent aa6c43a2
...@@ -535,10 +535,10 @@ Proof. ...@@ -535,10 +535,10 @@ Proof.
by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L). by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
Qed. Qed.
Global Instance local_update_op x : LocalUpdate (λ _, True) (op x). Global Instance op_local_update x : LocalUpdate (λ _, True) (op x).
Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed. Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
Global Instance local_update_id : LocalUpdate (λ _, True) (@id A). Global Instance id_local_update : LocalUpdate (λ _, True) (@id A).
Proof. split; auto with typeclass_instances. Qed. Proof. split; auto with typeclass_instances. Qed.
Global Instance exclusive_local_update y : Global Instance exclusive_local_update y :
...@@ -1218,14 +1218,14 @@ Section option. ...@@ -1218,14 +1218,14 @@ Section option.
Proof. intros. destruct mx; apply _. Qed. Proof. intros. destruct mx; apply _. Qed.
(** Updates *) (** Updates *)
Global Instance option_local_fmap_update L Lv : Global Instance option_fmap_local_update L Lv :
LocalUpdate Lv L LocalUpdate Lv L
LocalUpdate (λ mx, if mx is Some x then Lv x else False) (fmap L). LocalUpdate (λ mx, if mx is Some x then Lv x else False) (fmap L).
Proof. Proof.
split; first apply _. split; first apply _.
intros n [x|] [z|]; constructor; by eauto using (local_updateN L). intros n [x|] [z|]; constructor; by eauto using (local_updateN L).
Qed. Qed.
Global Instance option_local_const_update Lv y : Global Instance option_const_local_update Lv y :
LocalUpdate Lv (λ _, y) LocalUpdate Lv (λ _, y)
LocalUpdate (λ mx, if mx is Some x then Lv x else False) (λ _, Some y). LocalUpdate (λ mx, if mx is Some x then Lv x else False) (λ _, Some y).
Proof. Proof.
......
...@@ -283,7 +283,7 @@ Proof. apply insert_update. Qed. ...@@ -283,7 +283,7 @@ Proof. apply insert_update. Qed.
Section freshness. Section freshness.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}. Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma updateP_alloc_strong (Q : gmap K A Prop) (I : gset K) m x : Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : gset K) m x :
x ( i, m !! i = None i I Q (<[i:=x]>m)) m ~~>: Q. x ( i, m !! i = None i I Q (<[i:=x]>m)) m ~~>: Q.
Proof. Proof.
intros ? HQ. apply cmra_total_updateP. intros ? HQ. apply cmra_total_updateP.
...@@ -297,15 +297,15 @@ Proof. ...@@ -297,15 +297,15 @@ Proof.
last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union. last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
by apply insert_validN; [apply cmra_valid_validN|]. by apply insert_validN; [apply cmra_valid_validN|].
Qed. Qed.
Lemma updateP_alloc (Q : gmap K A Prop) m x : Lemma alloc_updateP (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. move=>??. eapply updateP_alloc_strong with (I:=); by eauto. Qed. Proof. move=>??. eapply alloc_updateP_strong with (I:=); by eauto. Qed.
Lemma updateP_alloc_strong' m x (I : gset K) : Lemma alloc_updateP_strong' m x (I : gset K) :
x m ~~>: λ m', i, i I m' = <[i:=x]>m m !! i = None. x m ~~>: λ m', i, i I m' = <[i:=x]>m m !! i = None.
Proof. eauto using updateP_alloc_strong. Qed. Proof. eauto using alloc_updateP_strong. Qed.
Lemma updateP_alloc' m x : Lemma alloc_updateP' 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 updateP_alloc. Qed. Proof. eauto using alloc_updateP. Qed.
Lemma singleton_updateP_unit (P : A Prop) (Q : gmap K A Prop) u i : Lemma singleton_updateP_unit (P : A Prop) (Q : gmap K A Prop) u i :
u LeftId () u () u LeftId () u ()
...@@ -335,7 +335,7 @@ End freshness. ...@@ -335,7 +335,7 @@ End freshness.
(* Allocation is a local update: Just use composition with a singleton map. *) (* Allocation is a local update: Just use composition with a singleton map. *)
Global Instance gmap_delete_update : Global Instance delete_local_update :
LocalUpdate (λ m, x, m !! i = Some x Exclusive x) (delete i). LocalUpdate (λ m, x, m !! i = Some x Exclusive x) (delete i).
Proof. Proof.
split; first apply _. split; first apply _.
...@@ -348,7 +348,7 @@ Proof. ...@@ -348,7 +348,7 @@ Proof.
Qed. Qed.
(* Applying a local update at a position we own is a local update. *) (* Applying a local update at a position we own is a local update. *)
Global Instance gmap_alter_update `{!LocalUpdate Lv L} i : Global Instance alter_local_update `{!LocalUpdate Lv L} i :
LocalUpdate (λ m, x, m !! i = Some x Lv x) (alter L i). LocalUpdate (λ m, x, m !! i = Some x Lv x) (alter L i).
Proof. Proof.
split; first apply _. split; first apply _.
......
...@@ -316,7 +316,7 @@ Section properties. ...@@ -316,7 +316,7 @@ Section properties.
Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed. Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
(* Update *) (* Update *)
Lemma list_update_updateP (P : A Prop) (Q : list A Prop) l1 x l2 : Lemma list_middle_updateP (P : A Prop) (Q : list A Prop) l1 x l2 :
x ~~>: P ( y, P y Q (l1 ++ y :: l2)) l1 ++ x :: l2 ~~>: Q. x ~~>: P ( y, P y Q (l1 ++ y :: l2)) l1 ++ x :: l2 ~~>: Q.
Proof. Proof.
intros Hx%option_updateP' HP. intros Hx%option_updateP' HP.
...@@ -332,13 +332,13 @@ Section properties. ...@@ -332,13 +332,13 @@ Section properties.
rewrite !list_lookup_op !lookup_app_r !app_length //=; lia. rewrite !list_lookup_op !lookup_app_r !app_length //=; lia.
Qed. Qed.
Lemma list_update_update l1 l2 x y : x ~~> y l1 ++ x :: l2 ~~> l1 ++ y :: l2. Lemma list_middle_update l1 l2 x y : x ~~> y l1 ++ x :: l2 ~~> l1 ++ y :: l2.
Proof. Proof.
rewrite !cmra_update_updateP => H; eauto using list_update_updateP with subst. rewrite !cmra_update_updateP => H; eauto using list_middle_updateP with subst.
Qed. Qed.
(* Applying a local update at a position we own is a local update. *) (* Applying a local update at a position we own is a local update. *)
Global Instance list_alter_update `{LocalUpdate A Lv L} i : Global Instance list_alter_local_update `{LocalUpdate A Lv L} i :
LocalUpdate (λ L, x, L !! i = Some x Lv x) (alter L i). LocalUpdate (λ L, x, L !! i = Some x Lv x) (alter L i).
Proof. Proof.
split; [apply _|]; intros n l1 l2 (x&Hi1&?) Hm; apply list_dist_lookup=> j. split; [apply _|]; intros n l1 l2 (x&Hi1&?) Hm; apply list_dist_lookup=> j.
......
...@@ -49,7 +49,7 @@ Proof. ...@@ -49,7 +49,7 @@ Proof.
rewrite -(pvs_mono _ _ ( m, ( γ, γ G m = to_globalF γ a) ownG m)%I). rewrite -(pvs_mono _ _ ( m, ( γ, γ G m = to_globalF γ a) ownG m)%I).
- rewrite ownG_empty. - rewrite ownG_empty.
eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty (inG_id i)); eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty (inG_id i));
first (eapply updateP_alloc_strong', cmra_transport_valid, Ha); first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver. naive_solver.
- apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]]. - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv // left_id. by rewrite -(exist_intro γ) const_equiv // left_id.
......
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