Commit 49f290a4 authored by Ralf Jung's avatar Ralf Jung
Browse files

rename namespace_map → reservation_map and generalize it to `positive` keys

parent 5380a1d7
......@@ -45,7 +45,7 @@ iris/algebra/gmultiset.v
iris/algebra/coPset.v
iris/algebra/proofmode_classes.v
iris/algebra/ufrac.v
iris/algebra/namespace_map.v
iris/algebra/reservation_map.v
iris/algebra/lib/excl_auth.v
iris/algebra/lib/frac_auth.v
iris/algebra/lib/ufrac_auth.v
......
From stdpp Require Import namespaces.
From iris.algebra Require Export gmap coPset local_updates.
From iris.algebra Require Import updates proofmode_classes.
From iris.prelude Require Import options.
(** The camera [namespace_map A] over a camera [A] provides the connectives
[namespace_map_data N a], which associates data [a : A] with a namespace [N],
and [namespace_map_token E], which says that no data has been associated with
the namespaces in the mask [E]. The important properties of this camera are:
- The lemma [namespace_map_token_union] enables one to split [namespace_map_token]
w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
[namespace_map_token (E1 ∪ E2) = namespace_map_token E1 ⋅ namespace_map_token E2]
- The lemma [namespace_map_alloc_update] provides a frame preserving update to
associate data to a namespace [namespace_map_token E ~~> namespace_map_data N a]
provided [↑N ⊆ E] and [✓ a]. *)
Record namespace_map (A : Type) := NamespaceMap {
namespace_map_data_proj : gmap positive A;
namespace_map_token_proj : coPset_disj
}.
Add Printing Constructor namespace_map.
Global Arguments NamespaceMap {_} _ _.
Global Arguments namespace_map_data_proj {_} _.
Global Arguments namespace_map_token_proj {_} _.
Global Instance: Params (@NamespaceMap) 1 := {}.
Global Instance: Params (@namespace_map_data_proj) 1 := {}.
Global Instance: Params (@namespace_map_token_proj) 1 := {}.
(** TODO: [positives_flatten] violates the namespace abstraction. *)
Definition namespace_map_data {A : cmra} (N : namespace) (a : A) : namespace_map A :=
NamespaceMap {[ positives_flatten N := a ]} ε.
Definition namespace_map_token {A : cmra} (E : coPset) : namespace_map A :=
NamespaceMap (CoPset E).
Global Instance: Params (@namespace_map_data) 2 := {}.
(* Ofe *)
Section ofe.
Context {A : ofe}.
Implicit Types x y : namespace_map A.
Local Instance namespace_map_equiv : Equiv (namespace_map A) := λ x y,
namespace_map_data_proj x namespace_map_data_proj y
namespace_map_token_proj x = namespace_map_token_proj y.
Local Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
namespace_map_data_proj x {n} namespace_map_data_proj y
namespace_map_token_proj x = namespace_map_token_proj y.
Global Instance NamespaceMap_ne : NonExpansive2 (@NamespaceMap A).
Proof. by split. Qed.
Global Instance NamespaceMap_proper : Proper (() ==> (=) ==> ()) (@NamespaceMap A).
Proof. by split. Qed.
Global Instance namespace_map_data_proj_ne: NonExpansive (@namespace_map_data_proj A).
Proof. by destruct 1. Qed.
Global Instance namespace_map_data_proj_proper :
Proper (() ==> ()) (@namespace_map_data_proj A).
Proof. by destruct 1. Qed.
Definition namespace_map_ofe_mixin : OfeMixin (namespace_map A).
Proof.
by apply (iso_ofe_mixin
(λ x, (namespace_map_data_proj x, namespace_map_token_proj x))).
Qed.
Canonical Structure namespace_mapO :=
Ofe (namespace_map A) namespace_map_ofe_mixin.
Global Instance NamespaceMap_discrete a b :
Discrete a Discrete b Discrete (NamespaceMap a b).
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
Global Instance namespace_map_ofe_discrete :
OfeDiscrete A OfeDiscrete namespace_mapO.
Proof. intros ? [??]; apply _. Qed.
End ofe.
Global Arguments namespace_mapO : clear implicits.
(* Camera *)
Section cmra.
Context {A : cmra}.
Implicit Types a b : A.
Implicit Types x y : namespace_map A.
Global Instance namespace_map_data_ne i : NonExpansive (@namespace_map_data A i).
Proof. solve_proper. Qed.
Global Instance namespace_map_data_proper N :
Proper (() ==> ()) (@namespace_map_data A N).
Proof. solve_proper. Qed.
Global Instance namespace_map_data_discrete N a :
Discrete a Discrete (namespace_map_data N a).
Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
Global Instance namespace_map_token_discrete E : Discrete (@namespace_map_token A E).
Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
Local Instance namespace_map_valid_instance : Valid (namespace_map A) := λ x,
match namespace_map_token_proj x with
| CoPset E =>
(namespace_map_data_proj x)
(* dom (namespace_map_data_proj x) ⊥ E *)
i, namespace_map_data_proj x !! i = None i E
| CoPsetBot => False
end.
Global Arguments namespace_map_valid_instance !_ /.
Local Instance namespace_map_validN_instance : ValidN (namespace_map A) := λ n x,
match namespace_map_token_proj x with
| CoPset E =>
{n} (namespace_map_data_proj x)
(* dom (namespace_map_data_proj x) ⊥ E *)
i, namespace_map_data_proj x !! i = None i E
| CoPsetBot => False
end.
Global Arguments namespace_map_validN_instance !_ /.
Local Instance namespace_map_pcore_instance : PCore (namespace_map A) := λ x,
Some (NamespaceMap (core (namespace_map_data_proj x)) ε).
Local Instance namespace_map_op_instance : Op (namespace_map A) := λ x y,
NamespaceMap (namespace_map_data_proj x namespace_map_data_proj y)
(namespace_map_token_proj x namespace_map_token_proj y).
Definition namespace_map_valid_eq :
valid = λ x, match namespace_map_token_proj x with
| CoPset E =>
(namespace_map_data_proj x)
(* dom (namespace_map_data_proj x) ⊥ E *)
i, namespace_map_data_proj x !! i = None i E
| CoPsetBot => False
end := eq_refl _.
Definition namespace_map_validN_eq :
validN = λ n x, match namespace_map_token_proj x with
| CoPset E =>
{n} (namespace_map_data_proj x)
(* dom (namespace_map_data_proj x) ⊥ E *)
i, namespace_map_data_proj x !! i = None i E
| CoPsetBot => False
end := eq_refl _.
Lemma namespace_map_included x y :
x y
namespace_map_data_proj x namespace_map_data_proj y
namespace_map_token_proj x namespace_map_token_proj y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (NamespaceMap z1 z2); split; auto.
Qed.
Lemma namespace_map_data_proj_validN n x : {n} x {n} namespace_map_data_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
Lemma namespace_map_token_proj_validN n x : {n} x {n} namespace_map_token_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
Lemma namespace_map_cmra_mixin : CmraMixin (namespace_map A).
Proof.
apply cmra_total_mixin.
- eauto.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- solve_proper.
- intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[??]; split; simplify_eq/=.
+ by rewrite -Hm.
+ intros i. by rewrite -(dist_None n) -Hm dist_None.
- intros [m [E|]]; rewrite namespace_map_valid_eq namespace_map_validN_eq /=
?cmra_valid_validN; naive_solver eauto using O.
- intros n [m [E|]]; rewrite namespace_map_validN_eq /=;
naive_solver eauto using cmra_validN_S.
- split; simpl; [by rewrite assoc|by rewrite assoc_L].
- split; simpl; [by rewrite comm|by rewrite comm_L].
- split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
- split; simpl; [by rewrite cmra_core_idemp|done].
- intros ??; rewrite! namespace_map_included; intros [??].
by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
- intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite namespace_map_validN_eq /=.
rewrite {1}/op /cmra_op /=. case_decide; last done.
intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
intros i. move: (Hdisj i). rewrite lookup_op.
case: (m1 !! i)=> [a|]; last auto.
move=> [].
{ by case: (m2 !! i). }
set_solver.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (namespace_map_data_proj x)
(namespace_map_data_proj y1) (namespace_map_data_proj y2))
as (m1&m2&?&?&?); auto using namespace_map_data_proj_validN.
destruct (cmra_extend n (namespace_map_token_proj x)
(namespace_map_token_proj y1) (namespace_map_token_proj y2))
as (E1&E2&?&?&?); auto using namespace_map_token_proj_validN.
by exists (NamespaceMap m1 E1), (NamespaceMap m2 E2).
Qed.
Canonical Structure namespace_mapR :=
Cmra (namespace_map A) namespace_map_cmra_mixin.
Global Instance namespace_map_cmra_discrete :
CmraDiscrete A CmraDiscrete namespace_mapR.
Proof.
split; first apply _.
intros [m [E|]]; rewrite namespace_map_validN_eq namespace_map_valid_eq //=.
by intros [?%cmra_discrete_valid ?].
Qed.
Local Instance namespace_map_empty_instance : Unit (namespace_map A) := NamespaceMap ε ε.
Lemma namespace_map_ucmra_mixin : UcmraMixin (namespace_map A).
Proof.
split; simpl.
- rewrite namespace_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
- split; simpl; [by rewrite left_id|by rewrite left_id_L].
- do 2 constructor; [apply (core_id_core _)|done].
Qed.
Canonical Structure namespace_mapUR :=
Ucmra (namespace_map A) namespace_map_ucmra_mixin.
Global Instance namespace_map_data_core_id N a :
CoreId a CoreId (namespace_map_data N a).
Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
Lemma namespace_map_data_valid N a : (namespace_map_data N a) a.
Proof. rewrite namespace_map_valid_eq /= singleton_valid. set_solver. Qed.
Lemma namespace_map_token_valid E : (namespace_map_token E).
Proof. rewrite namespace_map_valid_eq /=. split; first done. by left. Qed.
Lemma namespace_map_data_op N a b :
namespace_map_data N (a b) = namespace_map_data N a namespace_map_data N b.
Proof.
by rewrite {2}/op /namespace_map_op_instance /namespace_map_data /= singleton_op left_id_L.
Qed.
Lemma namespace_map_data_mono N a b :
a b namespace_map_data N a namespace_map_data N b.
Proof. intros [c ->]. rewrite namespace_map_data_op. apply cmra_included_l. Qed.
Global Instance namespace_map_data_is_op N a b1 b2 :
IsOp a b1 b2
IsOp' (namespace_map_data N a) (namespace_map_data N b1) (namespace_map_data N b2).
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite namespace_map_data_op. Qed.
Lemma namespace_map_token_union E1 E2 :
E1 ## E2
namespace_map_token (E1 E2) = namespace_map_token E1 namespace_map_token E2.
Proof.
intros. by rewrite /op /namespace_map_op_instance
/namespace_map_token /= coPset_disj_union // left_id_L.
Qed.
Lemma namespace_map_token_difference E1 E2 :
E1 E2
namespace_map_token E2 = namespace_map_token E1 namespace_map_token (E2 E1).
Proof.
intros. rewrite -namespace_map_token_union; last set_solver.
by rewrite -union_difference_L.
Qed.
Lemma namespace_map_token_valid_op E1 E2 :
(namespace_map_token E1 namespace_map_token E2) E1 ## E2.
Proof.
rewrite namespace_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
split; [done|]; intros _. split.
- by rewrite left_id.
- intros i. rewrite lookup_op lookup_empty. auto.
Qed.
(** [↑N ⊆ E] is stronger than needed, just [positives_flatten N ∈ E] would be
sufficient. However, we do not have convenient infrastructure to prove the
latter, so we use the former. *)
Lemma namespace_map_alloc_update E N a :
N E a namespace_map_token E ~~> namespace_map_data N a.
Proof.
assert (positives_flatten N (N : coPset)).
{ rewrite nclose_eq. apply elem_coPset_suffixes.
exists 1%positive. by rewrite left_id_L. }
intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
rewrite namespace_map_validN_eq /= {1}/op /cmra_op /=. case_decide; last done.
rewrite left_id_L {1}left_id. intros [Hmf Hdisj]; split.
- destruct (Hdisj (positives_flatten N)) as [Hmfi|]; last set_solver.
move: Hmfi. rewrite lookup_op lookup_empty left_id_L=> Hmfi.
intros j. rewrite lookup_op.
destruct (decide (positives_flatten N = j)) as [<-|].
+ rewrite Hmfi lookup_singleton right_id_L. by apply cmra_valid_validN.
+ by rewrite lookup_singleton_ne // left_id_L.
- intros j. destruct (decide (positives_flatten N = j)); first set_solver.
rewrite lookup_op lookup_singleton_ne //.
destruct (Hdisj j) as [Hmfi|?]; last set_solver.
move: Hmfi. rewrite lookup_op lookup_empty; auto.
Qed.
Lemma namespace_map_updateP P (Q : namespace_map A Prop) N a :
a ~~>: P
( a', P a' Q (namespace_map_data N a')) namespace_map_data N a ~~>: Q.
Proof.
intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
rewrite namespace_map_validN_eq /= left_id_L. intros [Hmf Hdisj].
destruct (Hup n (mf !! positives_flatten N)) as (a'&?&?).
{ move: (Hmf (positives_flatten N)).
by rewrite lookup_op lookup_singleton Some_op_opM. }
exists (namespace_map_data N a'); split; first by eauto.
rewrite /= left_id_L. split.
- intros j. destruct (decide (positives_flatten N = j)) as [<-|].
+ by rewrite lookup_op lookup_singleton Some_op_opM.
+ rewrite lookup_op lookup_singleton_ne // left_id_L.
move: (Hmf j). rewrite lookup_op. eauto using cmra_validN_op_r.
- intros j. move: (Hdisj j).
rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
Qed.
Lemma namespace_map_update N a b :
a ~~> b namespace_map_data N a ~~> namespace_map_data N b.
Proof.
rewrite !cmra_update_updateP. eauto using namespace_map_updateP with subst.
Qed.
End cmra.
Global Arguments namespace_mapR : clear implicits.
Global Arguments namespace_mapUR : clear implicits.
From iris.algebra Require Export gmap coPset local_updates.
From iris.algebra Require Import updates proofmode_classes.
From iris.prelude Require Import options.
(** The camera [reservation_map A] over a camera [A] extends [gmap positive A]
with a notion of "reservation tokens" for a (potentially infinite) set
[E : coPset] which represent the right to allocate a map entry at any position
[k ∈ E]. The key connectives are [reservation_map_data k a] (the "points-to"
assertion of this map), which associates data [a : A] with a key [k : positive],
and [reservation_map_token E] (the reservation token), which says
that no data has been associated with the indices in the mask [E]. The important
properties of this camera are:
- The lemma [reservation_map_token_union] enables one to split [reservation_map_token]
w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
[reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2].
- The lemma [reservation_map_alloc_update] provides a frame preserving update to
associate data to a key: [reservation_map_token E ~~> reservation_map_data k a]
provided [k ∈ E] and [✓ a].
In the future, it could be interesting to generalize this map to arbitrary key
types instead of hard-coding [positive]. *)
Record reservation_map (A : Type) := ReservationMap {
reservation_map_data_proj : gmap positive A;
reservation_map_token_proj : coPset_disj
}.
Add Printing Constructor reservation_map.
Global Arguments ReservationMap {_} _ _.
Global Arguments reservation_map_data_proj {_} _.
Global Arguments reservation_map_token_proj {_} _.
Global Instance: Params (@ReservationMap) 1 := {}.
Global Instance: Params (@reservation_map_data_proj) 1 := {}.
Global Instance: Params (@reservation_map_token_proj) 1 := {}.
Definition reservation_map_data {A : cmra} (k : positive) (a : A) : reservation_map A :=
ReservationMap {[ k := a ]} ε.
Definition reservation_map_token {A : cmra} (E : coPset) : reservation_map A :=
ReservationMap (CoPset E).
Global Instance: Params (@reservation_map_data) 2 := {}.
(* Ofe *)
Section ofe.
Context {A : ofe}.
Implicit Types x y : reservation_map A.
Local Instance reservation_map_equiv : Equiv (reservation_map A) := λ x y,
reservation_map_data_proj x reservation_map_data_proj y
reservation_map_token_proj x = reservation_map_token_proj y.
Local Instance reservation_map_dist : Dist (reservation_map A) := λ n x y,
reservation_map_data_proj x {n} reservation_map_data_proj y
reservation_map_token_proj x = reservation_map_token_proj y.
Global Instance ReservationMap_ne : NonExpansive2 (@ReservationMap A).
Proof. by split. Qed.
Global Instance ReservationMap_proper : Proper (() ==> (=) ==> ()) (@ReservationMap A).
Proof. by split. Qed.
Global Instance reservation_map_data_proj_ne: NonExpansive (@reservation_map_data_proj A).
Proof. by destruct 1. Qed.
Global Instance reservation_map_data_proj_proper :
Proper (() ==> ()) (@reservation_map_data_proj A).
Proof. by destruct 1. Qed.
Definition reservation_map_ofe_mixin : OfeMixin (reservation_map A).
Proof.
by apply (iso_ofe_mixin
(λ x, (reservation_map_data_proj x, reservation_map_token_proj x))).
Qed.
Canonical Structure reservation_mapO :=
Ofe (reservation_map A) reservation_map_ofe_mixin.
Global Instance ReservationMap_discrete a b :
Discrete a Discrete b Discrete (ReservationMap a b).
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
Global Instance reservation_map_ofe_discrete :
OfeDiscrete A OfeDiscrete reservation_mapO.
Proof. intros ? [??]; apply _. Qed.
End ofe.
Global Arguments reservation_mapO : clear implicits.
(* Camera *)
Section cmra.
Context {A : cmra}.
Implicit Types a b : A.
Implicit Types x y : reservation_map A.
Implicit Types k : positive.
Global Instance reservation_map_data_ne i : NonExpansive (@reservation_map_data A i).
Proof. solve_proper. Qed.
Global Instance reservation_map_data_proper N :
Proper (() ==> ()) (@reservation_map_data A N).
Proof. solve_proper. Qed.
Global Instance reservation_map_data_discrete N a :
Discrete a Discrete (reservation_map_data N a).
Proof. intros. apply ReservationMap_discrete; apply _. Qed.
Global Instance reservation_map_token_discrete E : Discrete (@reservation_map_token A E).
Proof. intros. apply ReservationMap_discrete; apply _. Qed.
Local Instance reservation_map_valid_instance : Valid (reservation_map A) := λ x,
match reservation_map_token_proj x with
| CoPset E =>
(reservation_map_data_proj x)
(* dom (reservation_map_data_proj x) ⊥ E *)
i, reservation_map_data_proj x !! i = None i E
| CoPsetBot => False
end.
Global Arguments reservation_map_valid_instance !_ /.
Local Instance reservation_map_validN_instance : ValidN (reservation_map A) := λ n x,
match reservation_map_token_proj x with
| CoPset E =>
{n} (reservation_map_data_proj x)
(* dom (reservation_map_data_proj x) ⊥ E *)
i, reservation_map_data_proj x !! i = None i E
| CoPsetBot => False
end.
Global Arguments reservation_map_validN_instance !_ /.
Local Instance reservation_map_pcore_instance : PCore (reservation_map A) := λ x,
Some (ReservationMap (core (reservation_map_data_proj x)) ε).
Local Instance reservation_map_op_instance : Op (reservation_map A) := λ x y,
ReservationMap (reservation_map_data_proj x reservation_map_data_proj y)
(reservation_map_token_proj x reservation_map_token_proj y).
Definition reservation_map_valid_eq :
valid = λ x, match reservation_map_token_proj x with
| CoPset E =>
(reservation_map_data_proj x)
(* dom (reservation_map_data_proj x) ⊥ E *)
i, reservation_map_data_proj x !! i = None i E
| CoPsetBot => False
end := eq_refl _.
Definition reservation_map_validN_eq :
validN = λ n x, match reservation_map_token_proj x with
| CoPset E =>
{n} (reservation_map_data_proj x)
(* dom (reservation_map_data_proj x) ⊥ E *)
i, reservation_map_data_proj x !! i = None i E
| CoPsetBot => False
end := eq_refl _.
Lemma reservation_map_included x y :
x y
reservation_map_data_proj x reservation_map_data_proj y
reservation_map_token_proj x reservation_map_token_proj y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (ReservationMap z1 z2); split; auto.
Qed.
Lemma reservation_map_data_proj_validN n x : {n} x {n} reservation_map_data_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
Lemma reservation_map_token_proj_validN n x : {n} x {n} reservation_map_token_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
Lemma reservation_map_cmra_mixin : CmraMixin (reservation_map A).
Proof.
apply cmra_total_mixin.
- eauto.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- solve_proper.
- intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[??]; split; simplify_eq/=.
+ by rewrite -Hm.
+ intros i. by rewrite -(dist_None n) -Hm dist_None.
- intros [m [E|]]; rewrite reservation_map_valid_eq reservation_map_validN_eq /=
?cmra_valid_validN; naive_solver eauto using O.
- intros n [m [E|]]; rewrite reservation_map_validN_eq /=;
naive_solver eauto using cmra_validN_S.
- split; simpl; [by rewrite assoc|by rewrite assoc_L].
- split; simpl; [by rewrite comm|by rewrite comm_L].
- split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
- split; simpl; [by rewrite cmra_core_idemp|done].
- intros ??; rewrite! reservation_map_included; intros [??].
by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
- intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite reservation_map_validN_eq /=.
rewrite {1}/op /cmra_op /=. case_decide; last done.
intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
intros i. move: (Hdisj i). rewrite lookup_op.
case: (m1 !! i)=> [a|]; last auto.
move=> [].
{ by case: (m2 !! i). }
set_solver.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (reservation_map_data_proj x)
(reservation_map_data_proj y1) (reservation_map_data_proj y2))
as (m1&m2&?&?&?); auto using reservation_map_data_proj_validN.
destruct (cmra_extend n (reservation_map_token_proj x)
(reservation_map_token_proj y1) (reservation_map_token_proj y2))
as (E1&E2&?&?&?); auto using reservation_map_token_proj_validN.
by exists (ReservationMap m1 E1), (ReservationMap m2 E2).
Qed.
Canonical Structure reservation_mapR :=
Cmra (reservation_map A) reservation_map_cmra_mixin.
Global Instance reservation_map_cmra_discrete :
CmraDiscrete A CmraDiscrete reservation_mapR.
Proof.
split; first apply _.
intros [m [E|]]; rewrite reservation_map_validN_eq reservation_map_valid_eq //=.
by intros [?%cmra_discrete_valid ?].
Qed.
Local Instance reservation_map_empty_instance : Unit (reservation_map A) := ReservationMap ε ε.
Lemma reservation_map_ucmra_mixin : UcmraMixin (reservation_map A).
Proof.
split; simpl.
- rewrite reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
- split; simpl; [by rewrite left_id|by rewrite left_id_L].
- do 2 constructor; [apply (core_id_core _)|done].
Qed.
Canonical Structure reservation_mapUR :=
Ucmra (reservation_map A) reservation_map_ucmra_mixin.
Global Instance reservation_map_data_core_id N a :
CoreId a CoreId (reservation_map_data N a).
Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
Lemma reservation_map_data_valid N a : (reservation_map_data N a) a.
Proof. rewrite reservation_map_valid_eq /= singleton_valid. set_solver. Qed.
Lemma reservation_map_token_valid E : (reservation_map_token E).
Proof. rewrite reservation_map_valid_eq /=. split; first done. by left. Qed.
Lemma reservation_map_data_op N a b :
reservation_map_data N (a b) = reservation_map_data N a reservation_map_data N b.
Proof.
by rewrite {2}/op /reservation_map_op_instance /reservation_map_data /= singleton_op left_id_L.
Qed.
Lemma reservation_map_data_mono N a b :
a b reservation_map_data N a reservation_map_data N b.
Proof. intros [c ->]. rewrite reservation_map_data_op. apply cmra_included_l. Qed.
Global Instance reservation_map_data_is_op N a b1 b2 :
IsOp a b1 b2
IsOp' (reservation_map_data N a) (reservation_map_data N b1) (reservation_map_data N b2).
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite reservation_map_data_op. Qed.
Lemma reservation_map_token_union E1 E2 :
E1 ## E2