Commit 41aaefe0 authored by Ralf Jung's avatar Ralf Jung

more nits

parent 734bc0ab
......@@ -442,10 +442,10 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Definition state_upd_heap (f: gmap loc val gmap loc val) (σ: state) :=
Definition state_upd_heap (f: gmap loc val gmap loc val) (σ: state) : state :=
{| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Arguments state_upd_heap _ !_ /.
Definition state_upd_used_proph_id (f: gset proph_id gset proph_id) (σ: state) :=
Definition state_upd_used_proph_id (f: gset proph_id gset proph_id) (σ: state) : state :=
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
......
......@@ -7,54 +7,6 @@ Import uPred.
Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
Definition proph_val_list (P V : Type) := list (P * V).
Section first_resolve.
Context {P V : Type} `{Countable P}.
Implicit Type pvs : proph_val_list P V.
Implicit Type p : P.
Implicit Type v : V.
Implicit Type R : proph_map P V.
(** The first resolve for [p] in [pvs] *)
Definition first_resolve pvs p :=
(map_of_list pvs : gmap P V) !! p.
Definition first_resolve_in_list R pvs :=
p v, p dom (gset _) R
first_resolve pvs p = Some v
R !! p = Some (Some v).
Lemma first_resolve_insert pvs p R :
first_resolve_in_list R pvs
p dom (gset _) R
first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
Proof.
intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
- by rewrite lookup_insert.
- rewrite lookup_insert_ne; first auto. by intros ->.
Qed.
Lemma first_resolve_delete pvs p v R :
first_resolve_in_list R ((p, v) :: pvs)
first_resolve_in_list (delete p R) pvs.
Proof.
intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
Qed.
Lemma first_resolve_eq R p v w pvs :
first_resolve_in_list R ((p, v) :: pvs)
R !! p = Some w
w = Some v.
Proof.
intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
inversion Hlookup. done.
Qed.
End first_resolve.
Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
gmapUR P $ exclR $ optionC $ leibnizC V.
......@@ -81,6 +33,15 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{pG : proph_mapG P V Σ}.
(** The first resolve for [p] in [pvs] *)
Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
(map_of_list pvs : gmap P V) !! p.
Definition first_resolve_in_list (R : proph_map P V) pvs :=
p v, p dom (gset _) R
first_resolve pvs p = Some v
R !! p = Some (Some v).
Definition proph_map_auth (R : proph_map P V) : iProp Σ :=
own (proph_map_name pG) ( (to_proph_map R)).
......@@ -98,6 +59,45 @@ Section definitions.
End definitions.
Section first_resolve.
Context {P V : Type} `{Countable P}.
Implicit Type pvs : proph_val_list P V.
Implicit Type p : P.
Implicit Type v : V.
Implicit Type R : proph_map P V.
Lemma first_resolve_insert pvs p R :
first_resolve_in_list R pvs
p dom (gset _) R
first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
Proof.
intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
- by rewrite lookup_insert.
- rewrite lookup_insert_ne; first auto. by intros ->.
Qed.
Lemma first_resolve_delete pvs p v R :
first_resolve_in_list R ((p, v) :: pvs)
first_resolve_in_list (delete p R) pvs.
Proof.
intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
Qed.
Lemma first_resolve_eq R p v w pvs :
first_resolve_in_list R ((p, v) :: pvs)
R !! p = Some w
w = Some v.
Proof.
intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
inversion Hlookup. done.
Qed.
End first_resolve.
Section to_proph_map.
Context (P V : Type) `{Countable P}.
Implicit Types p : P.
......
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