cmra.v 15.2 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.
11
Hint Extern 0 (?x {_} ?y) => 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
(** 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
103
(** * Morphisms *)
104
105
106
107
108
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
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Section cmra.
121
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
127
128
129
130
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.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
177
(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Global Instance cmra_included_ne n :
179
  Proper (dist n ==> dist n ==> iff) (includedN n : relation A) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
182
183
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
184
Global Instance cmra_included_proper : 
185
  Proper (() ==> () ==> iff) (includedN n : relation A) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
190
191
192
193
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
Lemma cmra_included_le x y n n' : x {n} y  n'  n  x {n'} y.
Proof. induction 2; auto using cmra_included_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
199
200

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.
201
Global Instance cmra_included_ord n : PreOrder (includedN n : relation A).
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
204
205
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
206
    by rewrite (associative _) -Hy -Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
Lemma cmra_valid_includedN x y n : {n} y  x {n} y  {n} x.
209
Proof. intros Hyv [z ?]; cofe_subst y; eauto using @cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Lemma cmra_valid_included x y n : {n} y  x  y  {n} x.
211
Proof. rewrite cmra_included_includedN; eauto using @cmra_valid_includedN. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
214
215
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
216
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
218

Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
222
(** ** RAs with empty element *)
Lemma cmra_empty_least `{Empty A, !RAIdentity A} n x :  {n} x.
Proof. by exists x; rewrite (left_id _ _). Qed.

223
224
225
226
227
228
229
230
231
232
233
(** ** big ops *)
Section bigop.
  Context `{Empty A, !RAIdentity A, FinMap K M}.
  Lemma big_opM_lookup_valid n m i x :
    {n} (big_opM m)  m !! i = Some x  {n} x.
  Proof.
    intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
    apply cmra_valid_op_l.
  Qed.
End bigop.

Robbert Krebbers's avatar
Robbert Krebbers committed
234
(** ** Properties of [(⇝)] relation *)
235
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
239
240
241
242
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
243
244
End cmra.

245
246
247
248
249
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.

250
251
252
253
254
255
256
257
258
259
(* Solver for validity *)
Ltac solve_validN :=
  match goal with
  | H : {?n} ?y |- {?n'} ?x =>
     let Hn := fresh in let Hx := fresh in
     assert (n'  n) as Hn by omega;
     assert (x  y) as Hx by solve_included;
     eapply cmra_valid_le, Hn; eapply cmra_valid_included, Hx; apply H
  end.

260
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
261
Proof. by split. Qed.
262
Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A  B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
265
266
267
268
269
270
  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.
271
272
273
274
275
276

(** 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
277
    match n with 0 => True | S n =>  x end.
278
  Definition discrete_cmra_mixin : CMRAMixin A.
279
280
281
282
283
284
285
286
  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
287
    * by intros [|n]; try apply ra_unit_preserving.
288
    * by intros [|n]; try apply ra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
    * by intros [|n] x y; try apply ra_op_minus.
290
  Qed.
291
  Definition discrete_extend_mixin : CMRAExtendMixin A.
292
  Proof.
293
    intros [|n] x y1 y2 ??; [|by exists (y1,y2); rewrite /dist /discrete_dist].
294
295
    by exists (x,unit x); simpl; rewrite ra_unit_r.
  Qed.
296
297
  Definition discreteRA : cmraT :=
    CMRAT discrete_cofe_mixin discrete_cmra_mixin discrete_extend_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  Lemma discrete_updateP (x : A) (P : A  Prop) `{!Inhabited (sig P)} :
299
    ( z,  (x  z)   y, P y   (y  z))  (x : discreteRA) : P.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
302
303
  Proof.
    intros Hvalid z [|n]; [|apply Hvalid].
    by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
  Qed.
304
305
  Lemma discrete_update (x y : A) :
    ( z,  (x  z)   (y  z))  (x : discreteRA)  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
  Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
307
End discrete.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Arguments discreteRA _ {_ _ _ _ _ _}.
309
310

(** Product *)
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
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
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.
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).
370
371
Proof.
  split.
372
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
    by split; apply includedN_preserving.
374
375
376
377
378
  * 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
379
380
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.