cmra.v 15.6 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
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)
}.
108 109 110 111 112 113 114
Instance compose_cmra_monotone {A B C : cmraT} (f : A -n> B) (g : B -n> C) :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (g  f).
Proof.
  split.
  - move=> n x y Hxy /=. eapply includedN_preserving, includedN_preserving; done.
  - move=> n x Hx /=. eapply validN_preserving, validN_preserving; done.
Qed.
115

Robbert Krebbers's avatar
Robbert Krebbers committed
116
(** * Updates *)
117
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
118
  {n} (x  z)   y, P y  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120
Instance: Params (@cmra_updateP) 3.
Infix "⇝:" := cmra_updateP (at level 70).
121
Definition cmra_update {A : cmraT} (x y : A) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
122
  {n} (x  z)  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125
Infix "⇝" := cmra_update (at level 70).
Instance: Params (@cmra_update) 3.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
184
(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
185
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
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
201 202
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
203 204 205 206 207

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

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

230 231 232 233 234 235 236 237 238 239 240
(** ** 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
241
(** ** Properties of [()] relation *)
242
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244 245 246 247 248 249
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
250 251
End cmra.

252 253 254 255 256
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.

257 258 259 260 261 262 263 264 265 266
(* 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.

267
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
268
Proof. by split. Qed.
269
Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A  B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
270 271 272 273 274 275 276 277
  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.
278 279 280 281 282 283

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

317 318 319
(** CMRA for the unit type *)
Canonical Structure unitRA : cmraT := discreteRA ().

320
(** Product *)
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 370 371 372 373 374 375 376 377 378 379
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).
380 381
Proof.
  split.
382
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
    by split; apply includedN_preserving.
384 385 386 387 388
  * 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
389 390
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.