Commit a8591b70 authored by Robbert Krebbers's avatar Robbert Krebbers

Use {[_ := _]} for singleton map so we can use ↦ for maps to.

The singleton maps notation is now also more consistent with the
insert <[_ := _]> _ notation for maps.
parent f081f494
...@@ -55,7 +55,7 @@ Lemma big_opM_delete (m : M A) i x : ...@@ -55,7 +55,7 @@ Lemma big_opM_delete (m : M A) i x :
Proof. Proof.
intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete. intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
Qed. Qed.
Lemma big_opM_singleton i x : big_opM ({[i x]} : M A) x. Lemma big_opM_singleton i x : big_opM ({[i := x]} : M A) x.
Proof. Proof.
rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty. rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
by rewrite big_opM_empty right_id. by rewrite big_opM_empty right_id.
......
...@@ -84,7 +84,7 @@ Proof. ...@@ -84,7 +84,7 @@ Proof.
by apply (timeless _); rewrite -Hm lookup_insert_ne. by apply (timeless _); rewrite -Hm lookup_insert_ne.
Qed. Qed.
Global Instance map_singleton_timeless i x : Global Instance map_singleton_timeless i x :
Timeless x Timeless ({[ i x ]} : gmap K A) := _. Timeless x Timeless ({[ i := x ]} : gmap K A) := _.
End cofe. End cofe.
Arguments mapC _ {_ _} _. Arguments mapC _ {_ _} _.
...@@ -196,16 +196,16 @@ Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. ...@@ -196,16 +196,16 @@ Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m.
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed. Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
Lemma map_insert_valid m i x : x m <[i:=x]>m. Lemma map_insert_valid m i x : x m <[i:=x]>m.
Proof. intros ?? n j; apply map_insert_validN; auto. Qed. Proof. intros ?? n j; apply map_insert_validN; auto. Qed.
Lemma map_singleton_validN n i x : {n} ({[ i x ]} : gmap K A) {n} x. Lemma map_singleton_validN n i x : {n} ({[ i := x ]} : gmap K A) {n} x.
Proof. Proof.
split; [|by intros; apply map_insert_validN, cmra_empty_valid]. split; [|by intros; apply map_insert_validN, cmra_empty_valid].
by move=>/(_ i); simplify_map_equality. by move=>/(_ i); simplify_map_equality.
Qed. Qed.
Lemma map_singleton_valid i x : ({[ i x ]} : gmap K A) x. Lemma map_singleton_valid i x : ({[ i := x ]} : gmap K A) x.
Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed. Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed.
Lemma map_insert_singleton_opN n m i x : Lemma map_insert_singleton_opN n m i x :
m !! i = None m !! i {n} Some (unit x) <[i:=x]> m {n} {[ i x ]} m. m !! i = None m !! i {n} Some (unit x) <[i:=x]> m {n} {[ i := x ]} m.
Proof. Proof.
intros Hi j; destruct (decide (i = j)) as [->|]; intros Hi j; destruct (decide (i = j)) as [->|];
[|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id]. [|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
...@@ -213,20 +213,20 @@ Proof. ...@@ -213,20 +213,20 @@ Proof.
by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r. by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r.
Qed. Qed.
Lemma map_insert_singleton_op m i x : Lemma map_insert_singleton_op m i x :
m !! i = None m !! i Some (unit x) <[i:=x]> m {[ i x ]} m. m !! i = None m !! i Some (unit x) <[i:=x]> m {[ i := x ]} m.
Proof. Proof.
rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN. rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN.
Qed. Qed.
Lemma map_unit_singleton (i : K) (x : A) : Lemma map_unit_singleton (i : K) (x : A) :
unit ({[ i x ]} : gmap K A) = {[ i unit x ]}. unit ({[ i := x ]} : gmap K A) = {[ i := unit x ]}.
Proof. apply map_fmap_singleton. Qed. Proof. apply map_fmap_singleton. Qed.
Lemma map_op_singleton (i : K) (x y : A) : Lemma map_op_singleton (i : K) (x y : A) :
{[ i x ]} {[ i y ]} = ({[ i x y ]} : gmap K A). {[ i := x ]} {[ i := y ]} = ({[ i := x y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed. Proof. by apply (merge_singleton _ _ _ x y). Qed.
Lemma singleton_includedN n m i x : Lemma singleton_includedN n m i x :
{[ i x ]} {n} m y, m !! i {n} Some y x y. {[ i := x ]} {n} m y, m !! i {n} Some y x y.
(* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *) (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
Proof. Proof.
split. split.
...@@ -264,23 +264,23 @@ Proof. ...@@ -264,23 +264,23 @@ Proof.
Qed. Qed.
Lemma map_singleton_updateP (P : A Prop) (Q : gmap K A Prop) i x : Lemma map_singleton_updateP (P : A Prop) (Q : gmap K A Prop) i x :
x ~~>: P ( y, P y Q {[ i y ]}) {[ i x ]} ~~>: Q. x ~~>: P ( y, P y Q {[ i := y ]}) {[ i := x ]} ~~>: Q.
Proof. apply map_insert_updateP. Qed. Proof. apply map_insert_updateP. Qed.
Lemma map_singleton_updateP' (P : A Prop) i x : Lemma map_singleton_updateP' (P : A Prop) i x :
x ~~>: P {[ i x ]} ~~>: λ m, y, m = {[ i y ]} P y. x ~~>: P {[ i := x ]} ~~>: λ m, y, m = {[ i := y ]} P y.
Proof. apply map_insert_updateP'. Qed. Proof. apply map_insert_updateP'. Qed.
Lemma map_singleton_update i (x y : A) : x ~~> y {[ i x ]} ~~> {[ i y ]}. Lemma map_singleton_update i (x y : A) : x ~~> y {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply map_insert_update. Qed. Proof. apply map_insert_update. Qed.
Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A} Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
(P : A Prop) (Q : gmap K A Prop) i : (P : A Prop) (Q : gmap K A Prop) i :
~~>: P ( y, P y Q {[ i y ]}) ~~>: Q. ~~>: P ( y, P y Q {[ i := y ]}) ~~>: Q.
Proof. Proof.
intros Hx HQ gf n Hg. intros Hx HQ gf n Hg.
destruct (Hx (from_option (gf !! i)) n) as (y&?&Hy). destruct (Hx (from_option (gf !! i)) n) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id. { move:(Hg i). rewrite !left_id.
case _: (gf !! i); simpl; auto using cmra_empty_valid. } case _: (gf !! i); simpl; auto using cmra_empty_valid. }
exists {[ i y ]}; split; first by auto. exists {[ i := y ]}; split; first by auto.
intros i'; destruct (decide (i' = i)) as [->|]. intros i'; destruct (decide (i' = i)) as [->|].
- rewrite lookup_op lookup_singleton. - rewrite lookup_op lookup_singleton.
move:Hy; case _: (gf !! i); first done. move:Hy; case _: (gf !! i); first done.
...@@ -288,7 +288,7 @@ Proof. ...@@ -288,7 +288,7 @@ Proof.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed. Qed.
Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A Prop) i : Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A Prop) i :
~~>: P ~~>: λ m, y, m = {[ i y ]} P y. ~~>: P ~~>: λ m, y, m = {[ i := y ]} P y.
Proof. eauto using map_singleton_updateP_empty. Qed. Proof. eauto using map_singleton_updateP_empty. Qed.
Section freshness. Section freshness.
......
...@@ -77,7 +77,7 @@ Section fin_map. ...@@ -77,7 +77,7 @@ Section fin_map.
Proof. Proof.
intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert. intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert.
Qed. Qed.
Lemma big_sepM_singleton i x : (Π★{map {[i x]}} P)%I (P i x)%I. Lemma big_sepM_singleton i x : (Π★{map {[i := x]}} P)%I (P i x)%I.
Proof. Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty. rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id. by rewrite big_sepM_empty right_id.
......
...@@ -116,7 +116,7 @@ Section proof. ...@@ -116,7 +116,7 @@ Section proof.
Local Notation state_to_val s := Local Notation state_to_val s :=
(match s with State Low _ => 0 | State High _ => 1 end). (match s with State Low _ => 0 | State High _ => 1 end).
Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp := Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
(l !=> '(state_to_val s) (l '(state_to_val s)
match s with State Low I' => waiting P I' | State High I' => ress I' end match s with State Low I' => waiting P I' | State High I' => ress I' end
)%I. )%I.
......
...@@ -20,14 +20,13 @@ Definition to_heap : state → heapRA := fmap Excl. ...@@ -20,14 +20,13 @@ Definition to_heap : state → heapRA := fmap Excl.
Definition of_heap : heapRA state := omap (maybe Excl). Definition of_heap : heapRA state := omap (maybe Excl).
Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ := Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l Excl v ]}. auth_own heap_name {[ l := Excl v ]}.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ := Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
ownP (of_heap h). ownP (of_heap h).
Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ := Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
auth_ctx heap_name N heap_inv. auth_ctx heap_name N heap_inv.
(* FIXME: ↦ is already used for the singleton empty map. Resolve that... *) Notation "l ↦ v" := (heap_mapsto l v) (at level 20) : uPred_scope.
Notation "l !=> v" := (heap_mapsto l v) (at level 20) : uPred_scope.
Section heap. Section heap.
Context {Σ : iFunctorG}. Context {Σ : iFunctorG}.
...@@ -56,7 +55,7 @@ Section heap. ...@@ -56,7 +55,7 @@ Section heap.
by case: (h !! l)=> [[]|]; auto. by case: (h !! l)=> [[]|]; auto.
Qed. Qed.
Lemma heap_singleton_inv_l h l v : Lemma heap_singleton_inv_l h l v :
({[l Excl v]} h) h !! l = None h !! l Some ExclUnit. ({[l := Excl v]} h) h !! l = None h !! l Some ExclUnit.
Proof. Proof.
move=> /(_ O l). rewrite lookup_op lookup_singleton. move=> /(_ O l). rewrite lookup_op lookup_singleton.
by case: (h !! l)=> [[]|]; auto. by case: (h !! l)=> [[]|]; auto.
...@@ -86,7 +85,7 @@ Section heap. ...@@ -86,7 +85,7 @@ Section heap.
Proof. intros h1 h2. by fold_leibniz=> ->. Qed. Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
(** General properties of mapsto *) (** General properties of mapsto *)
Lemma heap_mapsto_disjoint l v1 v2 : (l !=> v1 l !=> v2)%I False. Lemma heap_mapsto_disjoint l v1 v2 : (l v1 l v2)%I False.
Proof. Proof.
rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton. rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton.
rewrite map_validI (forall_elim l) lookup_singleton. rewrite map_validI (forall_elim l) lookup_singleton.
...@@ -97,7 +96,7 @@ Section heap. ...@@ -97,7 +96,7 @@ Section heap.
Lemma wp_alloc N E e v P Q : Lemma wp_alloc N E e v P Q :
to_val e = Some v nclose N E to_val e = Some v nclose N E
P heap_ctx N P heap_ctx N
P ( l, l !=> v - Q (LocV l)) P ( l, l v - Q (LocV l))
P wp E (Alloc e) Q. P wp E (Alloc e) Q.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
...@@ -112,7 +111,7 @@ Section heap. ...@@ -112,7 +111,7 @@ Section heap.
apply sep_mono_r; rewrite HP; apply later_mono. apply sep_mono_r; rewrite HP; apply later_mono.
apply forall_mono=> l; apply wand_intro_l. apply forall_mono=> l; apply wand_intro_l.
rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?. rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
rewrite -(exist_intro (op {[ l Excl v ]})). rewrite -(exist_intro (op {[ l := Excl v ]})).
repeat erewrite <-exist_intro by apply _; simpl. repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id !assoc. rewrite -of_heap_insert left_id right_id !assoc.
apply sep_mono_l. apply sep_mono_l.
...@@ -124,12 +123,12 @@ Section heap. ...@@ -124,12 +123,12 @@ Section heap.
Lemma wp_load N E l v P Q : Lemma wp_load N E l v P Q :
nclose N E nclose N E
P heap_ctx N P heap_ctx N
P ( l !=> v (l !=> v - Q v)) P ( l v (l v - Q v))
P wp E (Load (Loc l)) Q. P wp E (Load (Loc l)) Q.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ. rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l Excl v ]}; simpl; eauto with I. with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?. rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs. rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
...@@ -143,12 +142,12 @@ Section heap. ...@@ -143,12 +142,12 @@ Section heap.
Lemma wp_store N E l v' e v P Q : Lemma wp_store N E l v' e v P Q :
to_val e = Some v nclose N E to_val e = Some v nclose N E
P heap_ctx N P heap_ctx N
P ( l !=> v' (l !=> v - Q (LitV LitUnit))) P ( l v' (l v - Q (LitV LitUnit)))
P wp E (Store (Loc l) e) Q. P wp E (Store (Loc l) e) Q.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ. rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
with N heap_name {[ l Excl v' ]}; simpl; eauto with I. with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?. rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs. rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
...@@ -164,12 +163,12 @@ Section heap. ...@@ -164,12 +163,12 @@ Section heap.
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 to_val e1 = Some v1 to_val e2 = Some v2 v' v1
nclose N E nclose N E
P heap_ctx N P heap_ctx N
P ( l !=> v' (l !=> v' - Q (LitV (LitBool false)))) P ( l v' (l v' - Q (LitV (LitBool false))))
P wp E (Cas (Loc l) e1 e2) Q. P wp E (Cas (Loc l) e1 e2) Q.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ. rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ.
apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l Excl v' ]}; simpl; eauto 10 with I. with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?. rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs. rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
...@@ -184,12 +183,12 @@ Section heap. ...@@ -184,12 +183,12 @@ Section heap.
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
nclose N E nclose N E
P heap_ctx N P heap_ctx N
P ( l !=> v1 (l !=> v2 - Q (LitV (LitBool true)))) P ( l v1 (l v2 - Q (LitV (LitBool true))))
P wp E (Cas (Loc l) e1 e2) Q. P wp E (Cas (Loc l) e1 e2) Q.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
with N heap_name {[ l Excl v1 ]}; simpl; eauto 10 with I. with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?. rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs. rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
......
...@@ -433,7 +433,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch. ...@@ -433,7 +433,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
(** The singleton map *) (** The singleton map *)
Class SingletonM K A M := singletonM: K A M. Class SingletonM K A M := singletonM: K A M.
Instance: Params (@singletonM) 5. Instance: Params (@singletonM) 5.
Notation "{[ x ↦ y ]}" := (singletonM x y) (at level 1) : C_scope. Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with (** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *) value [a] in [m]. *)
...@@ -628,7 +628,6 @@ Class Lattice A `{SubsetEq A, Union A, Intersection A} : Prop := { ...@@ -628,7 +628,6 @@ Class Lattice A `{SubsetEq A, Union A, Intersection A} : Prop := {
(** ** Axiomatization of collections *) (** ** Axiomatization of collections *)
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with (** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *) elements of type [A]. *)
Instance: Params (@map) 3.
Class SimpleCollection A C `{ElemOf A C, Class SimpleCollection A C `{ElemOf A C,
Empty C, Singleton A C, Union C} : Prop := { Empty C, Singleton A C, Union C} : Prop := {
not_elem_of_empty (x : A) : x ; not_elem_of_empty (x : A) : x ;
......
...@@ -61,7 +61,7 @@ Proof. rewrite (dom_insert _). solve_elem_of. Qed. ...@@ -61,7 +61,7 @@ Proof. rewrite (dom_insert _). solve_elem_of. Qed.
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X : Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
X dom D m X dom D (<[i:=x]>m). X dom D m X dom D (<[i:=x]>m).
Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed. Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed.
Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i x]} {[ i ]}. Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} {[ i ]}.
Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed. Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed.
Lemma dom_delete {A} (m : M A) i : dom D (delete i m) dom D m {[ i ]}. Lemma dom_delete {A} (m : M A) i : dom D (delete i m) dom D m {[ i ]}.
Proof. Proof.
...@@ -123,7 +123,7 @@ Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m. ...@@ -123,7 +123,7 @@ Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
Proof. unfold_leibniz; apply dom_alter. Qed. Proof. unfold_leibniz; apply dom_alter. Qed.
Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} dom D m. Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} dom D m.
Proof. unfold_leibniz; apply dom_insert. Qed. Proof. unfold_leibniz; apply dom_insert. Qed.
Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i x]} = {[ i ]}. Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i := x]} = {[ i ]}.
Proof. unfold_leibniz; apply dom_singleton. Qed. Proof. unfold_leibniz; apply dom_singleton. Qed.
Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m {[ i ]}. Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m {[ i ]}.
Proof. unfold_leibniz; apply dom_delete. Qed. Proof. unfold_leibniz; apply dom_delete. Qed.
......
This diff is collapsed.
...@@ -23,7 +23,7 @@ Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l, ...@@ -23,7 +23,7 @@ Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
Program Instance hashset_empty: Empty (hashset hash) := Hashset _. Program Instance hashset_empty: Empty (hashset hash) := Hashset _.
Next Obligation. by intros n X; simpl_map. Qed. Next Obligation. by intros n X; simpl_map. Qed.
Program Instance hashset_singleton: Singleton A (hashset hash) := λ x, Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
Hashset {[ hash x [x] ]} _. Hashset {[ hash x := [x] ]} _.
Next Obligation. Next Obligation.
intros x n l [<- <-]%lookup_singleton_Some. intros x n l [<- <-]%lookup_singleton_Some.
rewrite Forall_singleton; auto using NoDup_singleton. rewrite Forall_singleton; auto using NoDup_singleton.
......
...@@ -17,7 +17,7 @@ Instance mapset_elem_of: ElemOf K (mapset M) := λ x X, ...@@ -17,7 +17,7 @@ Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
mapset_car X !! x = Some (). mapset_car X !! x = Some ().
Instance mapset_empty: Empty (mapset M) := Mapset . Instance mapset_empty: Empty (mapset M) := Mapset .
Instance mapset_singleton: Singleton K (mapset M) := λ x, Instance mapset_singleton: Singleton K (mapset M) := λ x,
Mapset {[ x () ]}. Mapset {[ x := () ]}.
Instance mapset_union: Union (mapset M) := λ X1 X2, Instance mapset_union: Union (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2). let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2).
Instance mapset_intersection: Intersection (mapset M) := λ X1 X2, Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
......
...@@ -17,7 +17,7 @@ Class inG (Λ : language) (Σ : gid → iFunctor) (A : cmraT) := InG { ...@@ -17,7 +17,7 @@ Class inG (Λ : language) (Σ : gid → iFunctor) (A : cmraT) := InG {
}. }.
Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) := Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id {[ γ cmra_transport inG_prf a ]}. iprod_singleton inG_id {[ γ := cmra_transport inG_prf a ]}.
Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iProp Λ (globalF Σ) := Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
ownG (to_globalF γ a). ownG (to_globalF γ a).
Instance: Params (@to_globalF) 5. Instance: Params (@to_globalF) 5.
......
From program_logic Require Export model. From program_logic Require Export model.
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ := Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
uPred_ownM (Res {[ i to_agree (Next (iProp_unfold P)) ]} ). uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ).
Arguments ownI {_ _} _ _%I. Arguments ownI {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res (Excl σ) ). Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res (Excl σ) ).
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res (Some m)). Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res (Some m)).
...@@ -66,7 +66,6 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed. ...@@ -66,7 +66,6 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m). Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed. Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *) (* inversion lemmas *)
Lemma ownI_spec r n i P : Lemma ownI_spec r n i P :
{n} r {n} r
......
...@@ -121,7 +121,7 @@ Proof. ...@@ -121,7 +121,7 @@ Proof.
intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia. intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto. destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
{ apply uPred_weaken with r n; eauto. } { apply uPred_weaken with r n; eauto. }
exists (Res {[ i to_agree (Next (iProp_unfold P)) ]} ). exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ).
by split; [by exists i; split; rewrite /uPred_holds /=|]. by split; [by exists i; split; rewrite /uPred_holds /=|].
Qed. Qed.
......
...@@ -137,7 +137,7 @@ Qed. ...@@ -137,7 +137,7 @@ Qed.
Lemma wsat_alloc n E1 E2 σ r P rP : Lemma wsat_alloc n E1 E2 σ r P rP :
¬set_finite E1 P n rP wsat (S n) (E1 E2) σ (rP r) ¬set_finite E1 P n rP wsat (S n) (E1 E2) σ (rP r)
i, wsat (S n) (E1 E2) σ i, wsat (S n) (E1 E2) σ
(Res {[i to_agree (Next (iProp_unfold P))]} r) (Res {[i := to_agree (Next (iProp_unfold P))]} r)
wld r !! i = None i E1. wld r !! i = None i E1.
Proof. Proof.
intros HE1 ? [rs [Hval Hσ HE Hwld]]. intros HE1 ? [rs [Hval Hσ HE Hwld]].
......
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