cmra.v 19.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Require Export modures.cofe.

Class Unit (A : Type) := unit : A  A.
Instance: Params (@unit) 2.

Class Op (A : Type) := op : A  A  A.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

Definition included `{Equiv A, Op A} (x y : A) :=  z, y  x  z.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
Hint Extern 0 (?x  ?y) => reflexivity.
Instance: Params (@included) 3.

Class Minus (A : Type) := minus : A  A  A.
Instance: Params (@minus) 2.
Infix "⩪" := minus (at level 40) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22

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

25 26 27 28 29
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
Notation "✓" := valid (at level 1).
Instance validN_valid `{ValidN A} : Valid A := λ x,  n, {n} x.

Robbert Krebbers's avatar
Robbert Krebbers committed
30 31 32 33
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.
34
Hint Extern 0 (?x {_} ?y) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
35

36
Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  (* setoids *)
38 39
  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;
40
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) ({n});
41
  mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  (* valid *)
43 44
  mixin_cmra_validN_0 x : {0} x;
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  (* monoid *)
46 47 48 49
  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;
50 51
  mixin_cmra_unit_preservingN n x y : x {n} y  unit x {n} unit y;
  mixin_cmra_validN_op_l n x y : {n} (x  y)  {n} x;
52
  mixin_cmra_op_minus n x y : x {n} y  x  y  x ={n}= y
Robbert Krebbers's avatar
Robbert Krebbers committed
53
}.
54 55 56
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
57

Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61 62 63 64 65 66 67
(** 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_validN : ValidN cmra_car;
  cmra_minus : Minus cmra_car;
68 69 70
  cmra_cofe_mixin : CofeMixin cmra_car;
  cmra_mixin : CMRAMixin cmra_car;
  cmra_extend_mixin : CMRAExtendMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
71
}.
72
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _.
73 74 75 76 77 78 79 80 81 82 83
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_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
84
Add Printing Constructor cmraT.
85
Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
86
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88
Canonical Structure cmra_cofeC.

89 90 91 92 93 94 95 96
(** 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.
97 98
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
99 100 101
  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.
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
  Lemma cmra_validN_0 x : {0} x.
  Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed.
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
  Global Instance cmra_associative : Associative () (@op A _).
  Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed.
  Global Instance cmra_commutative : Commutative () (@op A _).
  Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_l x : unit x  x  x.
  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_idempotent x : unit (unit x)  unit x.
  Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_preservingN n x y : x {n} y  unit x {n} unit y.
  Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed.
  Lemma cmra_validN_op_l n x y : {n} (x  y)  {n} x.
  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
118 119 120 121 122 123 124 125
  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.

126 127 128 129 130 131 132 133 134 135
Hint Extern 0 ({0} _) => apply cmra_validN_0.

(** * CMRAs with a global identity element *)
(** We use the notation  because for most instances (maps, sets, etc) the
`empty' element is the global identity. *)
Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
  cmra_empty_valid :  ;
  cmra_empty_left_id :> LeftId ()  ();
  cmra_empty_timeless :> Timeless 
}.
136

Robbert Krebbers's avatar
Robbert Krebbers committed
137
(** * Morphisms *)
138 139 140 141 142
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)
}.

143
(** * Frame preserving updates *)
144
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
145
  {n} (x  z)   y, P y  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147
Instance: Params (@cmra_updateP) 3.
Infix "⇝:" := cmra_updateP (at level 70).
148
Definition cmra_update {A : cmraT} (x y : A) :=  z n,
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  {n} (x  z)  {n} (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151 152
Infix "⇝" := cmra_update (at level 70).
Instance: Params (@cmra_update) 3.

Robbert Krebbers's avatar
Robbert Krebbers committed
153
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Section cmra.
155
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Implicit Types x y z : A.
157
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
158

159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
(** ** Setoids *)
Global Instance cmra_unit_proper : Proper (() ==> ()) (@unit A _).
Proof. apply (ne_proper _). Qed.
Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
Proof.
  intros x1 x2 Hx y1 y2 Hy.
  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Qed.
Global Instance ra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
Global Instance cmra_validN_proper : Proper (() ==> iff) (@validN A _ n) | 1.
Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
Global Instance cmra_minus_proper : Proper (() ==> () ==> ()) (@minus A _).
Proof. apply (ne_proper_2 _). Qed.

Global Instance cmra_valid_proper : Proper (() ==> iff) (@valid A _).
Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed.
Global Instance cmra_includedN_ne n :
  Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_includedN_proper n :
  Proper (() ==> () ==> iff) (@includedN A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
  by rewrite (Hx n) (Hy n).
Qed.
Global Instance cmra_included_proper :
  Proper (() ==> () ==> iff) (@included A _ _) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.

(** ** Validity *)
Lemma cmra_valid_validN x :  x   n, {n} x.
Proof. done. Qed.
Lemma cmra_validN_le x n n' : {n} x  n'  n  {n'} x.
Proof. induction 2; eauto using cmra_validN_S. Qed.
Lemma cmra_valid_op_l x y :  (x  y)   x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_op_r x y n : {n} (x  y)  {n} y.
Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed.
Lemma cmra_valid_op_r x y :  (x  y)   y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.

(** ** Units *)
Lemma cmra_unit_r x : x  unit x  x.
Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
Lemma cmra_unit_unit x : unit x  unit x  unit x.
Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed.
Lemma cmra_unit_validN x n : {n} x  {n} (unit x).
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_unit_valid x :  x   (unit x).
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
220 221 222 223 224 225
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.
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
  * by intros x; exists (unit x); rewrite cmra_unit_r.
  * intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
    by rewrite (associative _) -Hy -Hz.
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
  split; red; intros until 0; rewrite !cmra_included_includedN; first done.
  intros; etransitivity; eauto.
Qed.
Lemma cmra_validN_includedN x y n : {n} y  x {n} y  {n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included x y n : {n} y  x  y  {n} x.
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.

Lemma cmra_includedN_0 x y : x {0} y.
Proof. by exists (unit x). Qed.
Lemma cmra_includedN_S x y n : x {S n} y  x {n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Lemma cmra_includedN_le x y n n' : x {n} y  n'  n  x {n'} y.
Proof. induction 2; auto using cmra_includedN_S. Qed.

Lemma cmra_includedN_l n x y : x {n} x  y.
Proof. by exists y. Qed.
Lemma cmra_included_l x y : x  x  y.
Proof. by exists y. Qed.
Lemma cmra_includedN_r n x y : y {n} x  y.
Proof. rewrite (commutative op); apply cmra_includedN_l. Qed.
Lemma cmra_included_r x y : y  x  y.
Proof. rewrite (commutative op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258

259 260 261 262 263 264 265 266 267 268 269
Lemma cmra_unit_preserving x y : x  y  unit x  unit y.
Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
Lemma cmra_included_unit x : unit x  x.
Proof. by exists x; rewrite cmra_unit_l. Qed.
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.

Lemma cmra_included_dist_l x1 x2 x1' n :
  x1  x2  x1' ={n}= x1   x2', x1'  x2'  x2' ={n}= x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
Proof.
271 272
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
Qed.
274 275 276

(** ** Minus *)
Lemma cmra_op_minus' x y : x  y  x  y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
Proof.
278
  rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
280

Robbert Krebbers's avatar
Robbert Krebbers committed
281
(** ** Timeless *)
282
Lemma cmra_timeless_included_l x y : Timeless x  {1} y  x {1} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
283 284 285
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
286
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289
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.
290
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
291
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
292 293
Proof.
  intros ??? z Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
  destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
295
  { by rewrite -?Hz. }
Robbert Krebbers's avatar
Robbert Krebbers committed
296
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
297
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298

299 300 301 302 303 304 305 306 307 308 309 310
(** ** RAs with an empty element *)
Section identity.
  Context `{Empty A, !CMRAIdentity A}.
  Lemma cmra_empty_leastN  n x :  {n} x.
  Proof. by exists x; rewrite left_id. Qed.
  Lemma cmra_empty_least x :   x.
  Proof. by exists x; rewrite left_id. Qed.
  Global Instance cmra_empty_right_id : RightId ()  ().
  Proof. by intros x; rewrite (commutative op) left_id. Qed.
  Lemma cmra_unit_empty : unit   .
  Proof. by rewrite -{2}(cmra_unit_l ) right_id. Qed.
End identity.
Robbert Krebbers's avatar
Robbert Krebbers committed
311

312
(** ** Updates *)
313
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316 317 318 319 320
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
321 322
End cmra.

323
Hint Extern 0 (_ {0} _) => apply cmra_includedN_0.
324

325
(** * Properties about monotone functions *)
326
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
327
Proof. by split. Qed.
328 329
Instance cmra_monotone_compose {A B C : cmraT} (f : A  B) (g : B  C) :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
Proof.
  split.
332 333
  * move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
  * move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Qed.
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
Section cmra_monotone.
  Context {A B : cmraT} (f : A  B) `{!CMRAMonotone f}.
  Lemma included_preserving x y : x  y  f x  f y.
  Proof.
    rewrite !cmra_included_includedN; eauto using includedN_preserving.
  Qed.
  Lemma valid_preserving x :  x   (f x).
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

(** * Instances *)
(** ** Discrete CMRA *)
Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
  (* setoids *)
  ra_op_ne (x : A) : Proper (() ==> ()) (op x);
  ra_unit_ne :> Proper (() ==> ()) unit;
  ra_validN_ne :> Proper (() ==> impl) ;
  ra_minus_ne :> Proper (() ==> () ==> ()) minus;
  (* monoid *)
  ra_associative :> Associative () ();
  ra_commutative :> Commutative () ();
  ra_unit_l x : unit x  x  x;
  ra_unit_idempotent x : unit (unit x)  unit x;
  ra_unit_preserving x y : x  y  unit x  unit y;
  ra_valid_op_l x y :  (x  y)   x;
  ra_op_minus x y : x  y  x  y  x  y
}.

364
Section discrete.
365 366 367
  Context {A : cofeT} `{ x : A, Timeless x}.
  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).

368
  Instance discrete_validN : ValidN A := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
369
    match n with 0 => True | S n =>  x end.
370
  Definition discrete_cmra_mixin : CMRAMixin A.
371
  Proof.
372 373 374 375 376
    destruct ra; split; unfold Proper, respectful, includedN;
      repeat match goal with
      | |-  n : nat, _ => intros [|?]
      end; try setoid_rewrite <-(timeless_S _ _ _ _); try done.
    by intros x y ?; exists x.
377
  Qed.
378
  Definition discrete_extend_mixin : CMRAExtendMixin A.
379
  Proof.
380 381 382 383
    intros [|n] x y1 y2 ??.
    * by exists (unit x, x); rewrite /= ra_unit_l.
    * exists (y1,y2); split_ands; auto.
      apply (timeless _), dist_le with (S n); auto with lia.
384
  Qed.
385
  Definition discreteRA : cmraT :=
386
    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
  Lemma discrete_updateP (x : A) (P : A  Prop) `{!Inhabited (sig P)} :
388
    ( z,  (x  z)   y, P y   (y  z))  (x : discreteRA) : P.
Robbert Krebbers's avatar
Robbert Krebbers committed
389 390 391 392
  Proof.
    intros Hvalid z [|n]; [|apply Hvalid].
    by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
  Qed.
393 394
  Lemma discrete_update (x y : A) :
    ( z,  (x  z)   (y  z))  (x : discreteRA)  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
  Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
396 397
End discrete.

398 399 400 401 402 403 404 405 406 407 408 409 410 411
(** ** CMRA for the unit type *)
Section unit.
  Instance unit_valid : Valid () := λ x, True.
  Instance unit_unit : Unit () := λ x, x.
  Instance unit_op : Op () := λ x y, ().
  Instance unit_minus : Minus () := λ x y, ().
  Global Instance unit_empty : Empty () := ().
  Definition unit_ra : RA ().
  Proof. by split. Qed.
  Canonical Structure unitRA : cmraT :=
    Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
  Global Instance unit_cmra_identity : CMRAIdentity unitRA.
  Proof. by split; intros []. Qed.
End unit.
412

413
(** ** Product *)
414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
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_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.
439 440
    * by split.
    * by intros n x [??]; split; apply cmra_validN_S.
441 442
    * split; simpl; apply (associative _).
    * split; simpl; apply (commutative _).
443 444
    * split; simpl; apply cmra_unit_l.
    * split; simpl; apply cmra_unit_idempotent.
445
    * intros n x y; rewrite !prod_includedN.
446 447
      by intros [??]; split; apply cmra_unit_preservingN.
    * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
448 449 450 451 452 453 454 455 456 457 458 459
    * intros x y n; rewrite prod_includedN; intros [??].
      by split; apply cmra_op_minus.
  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.
460 461 462 463 464 465 466 467
  Global Instance prod_cmra_identity `{Empty A, Empty B} :
    CMRAIdentity A  CMRAIdentity B  CMRAIdentity prodRA.
  Proof.
    split.
    * split; apply cmra_empty_valid.
    * by split; rewrite /=left_id.
    * by intros ? [??]; split; apply (timeless _).
  Qed.
468 469 470 471 472
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).
473 474
Proof.
  split.
475
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
    by split; apply includedN_preserving.
477 478 479 480 481
  * 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
482 483
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.