cmra.v 13.1 KB
Newer Older
1
Require Export modures.ra modures.cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4

Class ValidN (A : Type) := validN : nat  A  Prop.
Instance: Params (@validN) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
Robbert Krebbers's avatar
Robbert Krebbers committed
6

Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y ={n}= x  z.
Notation "x ≼{ n } y" := (includedN n x y)
  (at level 70, format "x  ≼{ n }  y") : C_scope.
Instance: Params (@includedN) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
Hint Extern 0 (?x {_} ?x) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13

Class CMRA A `{Equiv A, Compl A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17
  (* setoids *)
  cmra_cofe :> Cofe A;
  cmra_op_ne n x :> Proper (dist n ==> dist n) (op x);
  cmra_unit_ne n :> Proper (dist n ==> dist n) unit;
Robbert Krebbers's avatar
Robbert Krebbers committed
18
  cmra_valid_ne n :> Proper (dist n ==> impl) ({n});
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20
  cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus;
  (* valid *)
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22 23
  cmra_valid_0 x : {0} x;
  cmra_valid_S n x : {S n} x  {n} x;
  cmra_valid_validN x :  x   n, {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27 28
  (* monoid *)
  cmra_associative : Associative () ();
  cmra_commutative : Commutative () ();
  cmra_unit_l x : unit x  x  x;
  cmra_unit_idempotent x : unit (unit x)  unit x;
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  cmra_unit_preserving n x y : x {n} y  unit x {n} unit y;
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  cmra_valid_op_l n x y : {n} (x  y)  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  cmra_op_minus n x y : x {n} y  x  y  x ={n}= y
Robbert Krebbers's avatar
Robbert Krebbers committed
32 33
}.
Class CMRAExtend A `{Equiv A, Dist A, Op A, ValidN A} :=
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  cmra_extend_op n x y1 y2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    {n} x  x ={n}= y1  y2  { z | x  z.1  z.2  z ={n}= (y1,y2) }.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

Robbert Krebbers's avatar
Robbert Krebbers committed
37 38 39
Class CMRAMonotone
    `{Dist A, Op A, ValidN A, Dist B, Op B, ValidN B} (f : A  B) := {
  includedN_preserving n x y : x {n} y  f x {n} f y;
Robbert Krebbers's avatar
Robbert Krebbers committed
40
  validN_preserving n x : {n} x  {n} (f x)
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
43
Hint Extern 0 ({0} _) => apply cmra_valid_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
44

Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58
(** Bundeled version *)
Structure cmraT := CMRAT {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_compl : Compl cmra_car;
  cmra_unit : Unit cmra_car;
  cmra_op : Op cmra_car;
  cmra_valid : Valid cmra_car;
  cmra_validN : ValidN cmra_car;
  cmra_minus : Minus cmra_car;
  cmra_cmra : CMRA cmra_car;
  cmra_extend : CMRAExtend cmra_car
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _}.
60 61 62 63 64 65 66 67 68 69
Arguments cmra_car _ : simpl never.
Arguments cmra_equiv _ _ _ : simpl never.
Arguments cmra_dist _ _ _ _ : simpl never.
Arguments cmra_compl _ _ : simpl never.
Arguments cmra_unit _ _ : simpl never.
Arguments cmra_op _ _ _ : simpl never.
Arguments cmra_valid _ _ : simpl never.
Arguments cmra_validN _ _ _ : simpl never.
Arguments cmra_minus _ _ _ : simpl never.
Arguments cmra_cmra _ : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
Add Printing Constructor cmraT.
Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  cmra_valid cmra_validN cmra_minus cmra_cmra cmra_extend.
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74 75
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A.
Canonical Structure cmra_cofeC.

Robbert Krebbers's avatar
Robbert Krebbers committed
76
(** Updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
Definition cmra_updateP `{Op A, ValidN A} (x : A) (P : A  Prop) :=  z n,
  {n} (x  z)   y, P y  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81
Instance: Params (@cmra_updateP) 3.
Infix "⇝:" := cmra_updateP (at level 70).
Definition cmra_update `{Op A, ValidN A} (x y : A) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  {n} (x  z)  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85
Infix "⇝" := cmra_update (at level 70).
Instance: Params (@cmra_update) 3.

Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88
(** Timeless validity *)
(* Not sure whether this is useful, see the rule [uPred_valid_elim_timeless]
in logic.v *)
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91 92
Class ValidTimeless `{Valid A, ValidN A} (x : A) :=
  valid_timeless : validN 1 x  valid x.
Arguments valid_timeless {_ _ _} _ {_} _.

Robbert Krebbers's avatar
Robbert Krebbers committed
93
(** Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96 97
Section cmra.
Context `{cmra : CMRA A}.
Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101 102 103 104
Lemma cmra_included_includedN x y : x  y   n, x {n} y.
Proof.
  split; [by intros [z Hz] n; exists z; rewrite Hz|].
  intros Hxy; exists (y  x); apply equiv_dist; intros n.
  symmetry; apply cmra_op_minus, Hxy.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
105
Global Instance cmra_valid_ne' : Proper (dist n ==> iff) ({n}) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof. by split; apply cmra_valid_ne. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Global Instance cmra_valid_proper : Proper (() ==> iff) ({n}) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109 110
Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
Global Instance cmra_ra : RA A.
Proof.
111 112
  split; try by (destruct cmra;
    eauto using ne_proper, ne_proper_2 with typeclass_instances).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
  * intros x y; rewrite !cmra_included_includedN.
    eauto using cmra_unit_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117
  * intros x y; rewrite !cmra_valid_validN; intros ? n.
    by apply cmra_valid_op_l with y.
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119
  * intros x y [z Hz]; apply equiv_dist; intros n.
    by apply cmra_op_minus; exists z; rewrite Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Lemma cmra_valid_op_r x y n : {n} (x  y)  {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Lemma cmra_valid_le x n n' : {n} x  n'  n  {n'} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
124 125 126 127
Proof. induction 2; eauto using cmra_valid_S. Qed.
Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) ().
Proof.
  intros x1 x2 Hx y1 y2 Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma cmra_unit_valid x n : {n} x  {n} (unit x).
Robbert Krebbers's avatar
Robbert Krebbers committed
131
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
132

Robbert Krebbers's avatar
Robbert Krebbers committed
133
(** * Timeless *)
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135 136 137 138
Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
  Timeless x  {1} y  x {1} y  x  y.
Proof.
  intros ?? [x' ?].
  destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y  x {1} y  x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
144
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146
Proof.
  intros ??? z Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
  destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
148 149
  { by rewrite -?Hz; apply cmra_valid_validN. }
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153

(** * Included *)
Global Instance cmra_included_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  Proper (dist n ==> dist n ==> iff) (includedN n) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158
Proof.
  intros x x' Hx y y' Hy; unfold includedN.
  by setoid_rewrite Hx; setoid_rewrite Hy.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
Global Instance cmra_included_proper : 
  Proper (() ==> () ==> iff) (includedN n) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
Proof.
  intros n x x' Hx y y' Hy; unfold includedN.
  by setoid_rewrite Hx; setoid_rewrite Hy.
Qed.
Lemma cmra_included_0 x y : x {0} y.
Proof. by exists (unit x). Qed.
Lemma cmra_included_S x y n : x {S n} y  x {n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.

Lemma cmra_included_l n x y : x {n} x  y.
Proof. by exists y. Qed.
Lemma cmra_included_r n x y : y {n} x  y.
Proof. rewrite (commutative op); apply cmra_included_l. Qed.
Global Instance cmra_included_ord n : PreOrder (includedN n).
Proof.
  split.
  * by intros x; exists (unit x); rewrite ra_unit_r.
  * intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
Robbert Krebbers's avatar
Robbert Krebbers committed
179
    by rewrite (associative _) -Hy -Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
Lemma cmra_valid_includedN x y n : {n} y  x {n} y  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Proof. intros Hyv [z Hy]; revert Hyv; rewrite Hy; apply cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Lemma cmra_valid_included x y n : {n} y  x  y  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185 186 187 188
Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed.
Lemma cmra_included_dist_l x1 x2 x1' n :
  x1  x2  x1' ={n}= x1   x2', x1'  x2'  x2' ={n}= x2.
Proof.
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using ra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193 194 195 196 197 198 199 200

(** * Properties of [()] relation *)
Global Instance cmra_update_preorder : PreOrder cmra_update.
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
Lemma cmra_update_updateP x y : x  y  x : (y =).
Proof.
  split.
  * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
  * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202
End cmra.

Robbert Krebbers's avatar
Robbert Krebbers committed
203
Instance cmra_monotone_id `{CMRA A} : CMRAMonotone (@id A).
204
Proof. by split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206 207 208 209 210 211 212 213
Instance cmra_monotone_ra_monotone `{CMRA A, CMRA B} (f : A  B) :
  CMRAMonotone f  RAMonotone f.
Proof.
  split.
  * intros x y; rewrite !cmra_included_includedN.
    by intros ? n; apply includedN_preserving.
  * intros x; rewrite !cmra_valid_validN.
    by intros ? n; apply validN_preserving.
Qed.
214

Robbert Krebbers's avatar
Robbert Krebbers committed
215
Hint Extern 0 (_ {0} _) => apply cmra_included_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217
(* Also via [cmra_cofe; cofe_equivalence] *)
Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
218 219 220 221 222 223 224

(** Discrete *)
Section discrete.
  Context `{ra : RA A}.
  Existing Instances discrete_dist discrete_compl.
  Let discrete_cofe' : Cofe A := discrete_cofe.
  Instance discrete_validN : ValidN A := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
225
    match n with 0 => True | S n =>  x end.
226 227 228 229 230 231 232 233 234
  Instance discrete_cmra : CMRA A.
  Proof.
    split; try by (destruct ra; auto).
    * by intros [|n]; try apply ra_op_proper.
    * by intros [|n]; try apply ra_unit_proper.
    * by intros [|n]; try apply ra_valid_proper.
    * by intros [|n]; try apply ra_minus_proper.
    * by intros [|n].
    * intros x; split; intros Hvalid. by intros [|n]. apply (Hvalid 1).
Robbert Krebbers's avatar
Robbert Krebbers committed
235
    * by intros [|n]; try apply ra_unit_preserving.
236
    * by intros [|n]; try apply ra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
    * by intros [|n] x y; try apply ra_op_minus.
238 239 240
  Qed.
  Instance discrete_extend : CMRAExtend A.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
    intros [|n] x y1 y2 ??; [|by exists (y1,y2)].
242 243
    by exists (x,unit x); simpl; rewrite ra_unit_r.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245
  Global Instance discrete_timeless (x : A) : ValidTimeless x.
  Proof. by intros ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
  Definition discreteRA : cmraT := CMRAT A.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
  Lemma discrete_updateP (x : A) (P : A  Prop) `{!Inhabited (sig P)} :
Robbert Krebbers's avatar
Robbert Krebbers committed
248
    ( z,  (x  z)   y, P y   (y  z))  x : P.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252
  Proof.
    intros Hvalid z [|n]; [|apply Hvalid].
    by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  Lemma discrete_update (x y : A) : ( z,  (x  z)   (y  z))  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
  Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
255
End discrete.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Arguments discreteRA _ {_ _ _ _ _ _}.
257 258 259 260 261 262 263

(** Product *)
Instance prod_op `{Op A, Op B} : Op (A * B) := λ x y, (x.1  y.1, x.2  y.2).
Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (, ).
Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := λ x,
  (unit (x.1), unit (x.2)).
Instance prod_valid `{Valid A, Valid B} : Valid (A * B) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
264
   (x.1)   (x.2).
265
Instance prod_validN `{ValidN A, ValidN B} : ValidN (A * B) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
266
  {n} (x.1)  {n} (x.2).
267 268
Instance prod_minus `{Minus A, Minus B} : Minus (A * B) := λ x y,
  (x.1  y.1, x.2  y.2).
Robbert Krebbers's avatar
Robbert Krebbers committed
269 270 271 272 273 274 275 276 277 278 279 280
Lemma prod_included `{Equiv A, Equiv B, Op A, Op B} (x y : A * B) :
  x  y  x.1  y.1  x.2  y.2.
Proof.
  split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
  intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
Qed.
Lemma prod_includedN `{Dist A, Dist B, Op A, Op B} (x y : A * B) n :
  x {n} y  x.1 {n} y.1  x.2 {n} y.2.
Proof.
  split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
  intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
Qed.
281 282 283
Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B).
Proof.
  split; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285 286
  * by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
  * by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
  * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite -?Hy1 -?Hy2.
287
  * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
Robbert Krebbers's avatar
Robbert Krebbers committed
288
      split; simpl in *; rewrite ?Hx1 ?Hx2 ?Hy1 ?Hy2.
289 290 291 292 293 294 295 296
  * split; apply cmra_valid_0.
  * by intros n x [??]; split; apply cmra_valid_S.
  * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
    intros Hvalid; split; apply cmra_valid_validN; intros n; apply Hvalid.
  * split; simpl; apply (associative _).
  * split; simpl; apply (commutative _).
  * split; simpl; apply ra_unit_l.
  * split; simpl; apply ra_unit_idempotent.
Robbert Krebbers's avatar
Robbert Krebbers committed
297 298
  * intros n x y; rewrite !prod_includedN.
    by intros [??]; split; apply cmra_unit_preserving.
299
  * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
300 301
  * intros x y n; rewrite prod_includedN; intros [??].
    by split; apply cmra_op_minus.
302
Qed.
303
Instance prod_ra_empty `{RAIdentity A, RAIdentity B} : RAIdentity (A * B).
304 305 306 307 308
Proof.
  repeat split; simpl; repeat apply ra_empty_valid; repeat apply (left_id _ _).
Qed.
Instance prod_cmra_extend `{CMRAExtend A, CMRAExtend B} : CMRAExtend (A * B).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310 311
  intros n x y1 y2 [??] [??]; simpl in *.
  destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
  destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
312 313
  by exists ((z1.1,z2.1),(z1.2,z2.2)).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316
Instance pair_timeless `{Valid A, ValidN A, Valid B, ValidN B} (x : A) (y : B) :
  ValidTimeless x  ValidTimeless y  ValidTimeless (x,y).
Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
317
Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B).
Robbert Krebbers's avatar
Robbert Krebbers committed
318 319 320
Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'}
  (f : A  A') (g : B  B') `{!CMRAMonotone f, !CMRAMonotone g} :
  CMRAMonotone (prod_map f g).
321 322
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
323 324
  * intros n x1 x2; rewrite !prod_includedN; intros [??]; simpl.
    by split; apply includedN_preserving.
325 326 327 328 329
  * by intros n x [??]; split; simpl; apply validN_preserving.
Qed.
Definition prodRA_map {A A' B B' : cmraT}
    (f : A -n> A') (g : B -n> B') : prodRA A B -n> prodRA A' B' :=
  CofeMor (prod_map f g : prodRA A B  prodRA A' B').
Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
Instance prodRA_map_ne {A A' B B'} n :
  Proper (dist n==> dist n==> dist n) (@prodRA_map A A' B B') := prodC_map_ne n.