cmra.v 14.9 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
14
Record CMRAMixin A
    `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  (* setoids *)
16
17
18
19
  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
  mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
  mixin_cmra_valid_ne n : Proper (dist n ==> impl) ({n});
  mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  (* valid *)
21
22
23
  mixin_cmra_valid_0 x : {0} x;
  mixin_cmra_valid_S n x : {S n} x  {n} x;
  mixin_cmra_valid_validN x :  x   n, {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  (* monoid *)
25
26
27
28
29
30
31
  mixin_cmra_associative : Associative () ();
  mixin_cmra_commutative : Commutative () ();
  mixin_cmra_unit_l x : unit x  x  x;
  mixin_cmra_unit_idempotent x : unit (unit x)  unit x;
  mixin_cmra_unit_preserving n x y : x {n} y  unit x {n} unit y;
  mixin_cmra_valid_op_l n x y : {n} (x  y)  {n} x;
  mixin_cmra_op_minus n x y : x {n} y  x  y  x ={n}= y
Robbert Krebbers's avatar
Robbert Krebbers committed
32
}.
33
34
35
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} :=  n x y1 y2,
  {n} x  x ={n}= y1  y2 
  { z | x  z.1  z.2  z.1 ={n}= y1  z.2 ={n}= y2 }.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
39
40
41
42
43
44
45
46
47
(** 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;
48
49
50
  cmra_cofe_mixin : CofeMixin cmra_car;
  cmra_mixin : CMRAMixin cmra_car;
  cmra_extend_mixin : CMRAExtendMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
51
}.
52
53
54
55
56
57
58
59
60
61
62
63
64
Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _ _.
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_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Arguments cmra_extend_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Add Printing Constructor cmraT.
66
67
Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
Canonical Structure cmra_cofeC.

70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
(** Lifting properties from the mixin *)
Section cmra_mixin.
  Context {A : cmraT}.
  Implicit Types x y : A.
  Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
  Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
  Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _).
  Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
  Global Instance cmra_valid_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_valid_ne _ (cmra_mixin A)). Qed.
  Global Instance cmra_minus_ne n :
    Proper (dist n ==> dist n ==> dist n) (@minus A _).
  Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
  Lemma cmra_valid_0 x : {0} x.
  Proof. apply (mixin_cmra_valid_0 _ (cmra_mixin A)). Qed.
  Lemma cmra_valid_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_valid_S _ (cmra_mixin A)). Qed.
  Lemma cmra_valid_validN x :  x   n, {n} x.
  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_preserving n x y : x {n} y  unit x {n} unit y.
  Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
  Lemma cmra_valid_op_l n x y : {n} (x  y)  {n} x.
  Proof. apply (mixin_cmra_valid_op_l _ (cmra_mixin A)). Qed.
  Lemma cmra_op_minus n x y : x {n} y  x  y  x ={n}= y.
  Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
  Lemma cmra_extend_op n x y1 y2 :
    {n} x  x ={n}= y1  y2 
    { z | x  z.1  z.2  z.1 ={n}= y1  z.2 ={n}= y2 }.
  Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.

Hint Extern 0 ({0} _) => apply cmra_valid_0.

(** Morphisms *)
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
  includedN_preserving n x y : x {n} y  f x {n} f y;
  validN_preserving n x : {n} x  {n} (f x)
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
109
(** Updates *)
110
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  {n} (x  z)   y, P y  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
Instance: Params (@cmra_updateP) 3.
Infix "⇝:" := cmra_updateP (at level 70).
114
Definition cmra_update {A : cmraT} (x y : A) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
115
  {n} (x  z)  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
118
Infix "⇝" := cmra_update (at level 70).
Instance: Params (@cmra_update) 3.

Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
121
(** Timeless validity *)
(* Not sure whether this is useful, see the rule [uPred_valid_elim_timeless]
in logic.v *)
122
Class ValidTimeless {A : cmraT} (x : A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  valid_timeless : validN 1 x  valid x.
124
Arguments valid_timeless {_} _ {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126
(** Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Section cmra.
128
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
131
132
133
134
135
136
137
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.

138
Global Instance cmra_valid_ne' : Proper (dist n ==> iff) ({n} : A  _) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof. by split; apply cmra_valid_ne. Qed.
140
Global Instance cmra_valid_proper : Proper (() ==> iff) ({n} : A  _) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
Global Instance cmra_ra : RA A.
Proof.
144
  split; try by (destruct (@cmra_mixin A);
145
    eauto using ne_proper, ne_proper_2 with typeclass_instances).
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
  * intros x y; rewrite !cmra_included_includedN.
148
    eauto using @cmra_unit_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
  * intros x y; rewrite !cmra_valid_validN; intros ? n.
    by apply cmra_valid_op_l with y.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
  * 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
153
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Lemma cmra_valid_op_r x y n : {n} (x  y)  {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Lemma cmra_valid_le x n n' : {n} x  n'  n  {n'} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Proof. induction 2; eauto using cmra_valid_S. Qed.
158
Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (@op A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
Proof.
  intros x1 x2 Hx y1 y2 Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Lemma cmra_unit_valid x n : {n} x  {n} (unit x).
164
Proof. rewrite -{1}(ra_unit_l x); apply cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
(** * Timeless *)
167
Lemma cmra_timeless_included_l x y : Timeless x  {1} y  x {1} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
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
171
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
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.
175
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
176
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
Proof.
  intros ??? z Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
  { by rewrite -?Hz; apply cmra_valid_validN. }
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
185

(** * Included *)
Global Instance cmra_included_ne n :
186
  Proper (dist n ==> dist n ==> iff) (includedN n : relation A) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
189
190
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
191
Global Instance cmra_included_proper : 
192
  Proper (() ==> () ==> iff) (includedN n : relation A) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
196
197
198
199
200
201
202
203
204
205
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.
206
Global Instance cmra_included_ord n : PreOrder (includedN n : relation A).
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
209
210
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
211
    by rewrite (associative _) -Hy -Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Lemma cmra_valid_includedN x y n : {n} y  x {n} y  {n} x.
214
Proof. intros Hyv [z ?]; cofe_subst y; eauto using @cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Lemma cmra_valid_included x y n : {n} y  x  y  {n} x.
216
Proof. rewrite cmra_included_includedN; eauto using @cmra_valid_includedN. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
219
220
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
221
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224

(** * Properties of [(⇝)] relation *)
225
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
228
229
230
231
232
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
233
234
End cmra.

235
236
237
238
239
240
Hint Resolve cmra_ra.
Hint Extern 0 (_ {0} _) => apply cmra_included_0.
(* Also via [cmra_cofe; cofe_equivalence] *)
Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.

Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
241
Proof. by split. Qed.
242
Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A  B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
243
244
245
246
247
248
249
250
  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.
251
252
253
254
255
256

(** Discrete *)
Section discrete.
  Context `{ra : RA A}.
  Existing Instances discrete_dist discrete_compl.
  Instance discrete_validN : ValidN A := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
257
    match n with 0 => True | S n =>  x end.
258
  Definition discrete_cmra_mixin : CMRAMixin A.
259
260
261
262
263
264
265
266
  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
267
    * by intros [|n]; try apply ra_unit_preserving.
268
    * by intros [|n]; try apply ra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
    * by intros [|n] x y; try apply ra_op_minus.
270
  Qed.
271
  Definition discrete_extend_mixin : CMRAExtendMixin A.
272
  Proof.
273
    intros [|n] x y1 y2 ??; [|by exists (y1,y2); rewrite /dist /discrete_dist].
274
275
    by exists (x,unit x); simpl; rewrite ra_unit_r.
  Qed.
276
277
278
  Definition discreteRA : cmraT :=
    CMRAT discrete_cofe_mixin discrete_cmra_mixin discrete_extend_mixin.
  Global Instance discrete_timeless (x : A) : ValidTimeless (x : discreteRA).
Robbert Krebbers's avatar
Robbert Krebbers committed
279
  Proof. by intros ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  Lemma discrete_updateP (x : A) (P : A  Prop) `{!Inhabited (sig P)} :
281
    ( z,  (x  z)   y, P y   (y  z))  (x : discreteRA) : P.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
284
285
  Proof.
    intros Hvalid z [|n]; [|apply Hvalid].
    by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
  Qed.
286
287
  Lemma discrete_update (x y : A) :
    ( z,  (x  z)   (y  z))  (x : discreteRA)  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
  Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
289
End discrete.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Arguments discreteRA _ {_ _ _ _ _ _}.
291
292

(** Product *)
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
Section prod.
  Context {A B : cmraT}.
  Instance prod_op : Op (A * B) := λ x y, (x.1  y.1, x.2  y.2).
  Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (, ).
  Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
  Instance prod_valid : Valid (A * B) := λ x,  (x.1)   (x.2).
  Instance prod_validN : ValidN (A * B) := λ n x, {n} (x.1)  {n} (x.2).
  Instance prod_minus : Minus (A * B) := λ x y, (x.1  y.1, x.2  y.2).
  Lemma prod_included (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 (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.
  Definition prod_cmra_mixin : CMRAMixin (A * B).
  Proof.
    split; try apply _.
    * by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
    * by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
    * by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
    * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
        split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
    * 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.
    * intros n x y; rewrite !prod_includedN.
      by intros [??]; split; apply cmra_unit_preserving.
    * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
    * intros x y n; rewrite prod_includedN; intros [??].
      by split; apply cmra_op_minus.
  Qed.
  Global Instance prod_ra_empty `{Empty A, Empty B} :
    RAIdentity A  RAIdentity B  RAIdentity (A * B).
  Proof.
    repeat split; simpl; repeat (apply ra_empty_valid || apply (left_id _ _)).
  Qed.
  Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
  Proof.
    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.
    by exists ((z1.1,z2.1),(z1.2,z2.2)).
  Qed.
  Canonical Structure prodRA : cmraT :=
    CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin.
  Instance pair_timeless (x : A) (y : B) :
    ValidTimeless x  ValidTimeless y  ValidTimeless (x,y).
  Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
End prod.
Arguments prodRA : clear implicits.

Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A  A') (g : B  B') :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (prod_map f g).
355
356
Proof.
  split.
357
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
    by split; apply includedN_preserving.
359
360
361
362
363
  * 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
364
365
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.