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.