cmra.v 24.9 KB
Newer Older
1
From algebra Require Export cofe.
2 3 4 5 6 7 8 9 10 11 12 13

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.
14
Hint Extern 0 (_  _) => reflexivity.
15 16 17 18 19
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.
23
Notation "✓{ n } x" := (validN n x)
24
  (at level 20, n at next level, format "✓{ n }  x").
Robbert Krebbers's avatar
Robbert Krebbers committed
25

26 27
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
28
Notation "✓ x" := (valid x) (at level 20) : C_scope.
29

30
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y {n} x  z.
31
Notation "x ≼{ n } y" := (includedN n x y)
32
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
33
Instance: Params (@includedN) 4.
34
Hint Extern 0 (_ {_} _) => reflexivity.
35

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

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

90 91 92 93 94 95 96 97
(** 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.
98 99
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
100 101 102
  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.
103 104
  Lemma cmra_valid_validN x :  x   n, {n} x.
  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
105 106
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
107 108 109 110
  Global Instance cmra_assoc : Assoc () (@op A _).
  Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
  Global Instance cmra_comm : Comm () (@op A _).
  Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
111 112
  Lemma cmra_unit_l x : unit x  x  x.
  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
113 114
  Lemma cmra_unit_idemp x : unit (unit x)  unit x.
  Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116
  Lemma cmra_unit_preserving x y : x  y  unit x  unit y.
  Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
117 118
  Lemma cmra_validN_op_l n x y : {n} (x  y)  {n} x.
  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  Lemma cmra_op_minus x y : x  y  x  y  x  y.
120
  Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
121
  Lemma cmra_extend n x y1 y2 :
122 123
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }.
124
  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
125 126
End cmra_mixin.

127 128 129 130 131 132 133 134
(** * 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 
}.
135
Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate .
136

137 138 139 140 141 142
(** * Discrete CMRAs *)
Class CMRADiscrete (A : cmraT) : Prop := {
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
143
(** * Morphisms *)
144 145
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
  includedN_preserving n x y : x {n} y  f x {n} f y;
146
  validN_preserving n x : {n} x  {n} f x
147 148
}.

149
(** * Local updates *)
Ralf Jung's avatar
Ralf Jung committed
150 151
(** The idea is that lemams taking this class will usually have L explicit,
    and leave Lv implicit - it will be inferred by the typeclass machinery. *)
152 153 154
Class LocalUpdate {A : cmraT} (Lv : A  Prop) (L : A  A) := {
  local_update_ne n :> Proper (dist n ==> dist n) L;
  local_updateN n x y : Lv x  {n} (x  y)  L (x  y) {n} L x  y
155 156 157
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

158
(** * Frame preserving updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  n z,
160
  {n} (x  z)   y, P y  {n} (y  z).
161
Instance: Params (@cmra_updateP) 1.
162
Infix "~~>:" := cmra_updateP (at level 70).
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Definition cmra_update {A : cmraT} (x y : A) :=  n z,
164
  {n} (x  z)  {n} (y  z).
165
Infix "~~>" := cmra_update (at level 70).
166
Instance: Params (@cmra_update) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
169
Section cmra.
170
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
Implicit Types x y z : A.
172
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
173

174 175 176 177 178 179
(** ** 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.
180
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
181 182 183 184 185 186 187 188 189 190 191
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 _).
192 193 194 195
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
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.
214 215 216
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
218 219 220 221
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
  intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
223 224
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
225 226

(** ** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
228 229 230
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
232
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
233 234 235 236 237
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.
238
Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
239
Lemma cmra_unit_unit x : unit x  unit x  unit x.
240
Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
Lemma cmra_unit_validN n x : {n} x  {n} unit x.
242
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
243
Lemma cmra_unit_valid x :  x   unit x.
244 245
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
246 247 248 249
(** ** Minus *)
Lemma cmra_op_minus' n x y : x {n} y  x  y  x {n} y.
Proof. intros [z ->]. by rewrite cmra_op_minus; last exists z. Qed.

250
(** ** Order *)
251 252 253
Lemma cmra_included_includedN x y : x  y   n, x {n} y.
Proof.
  split; [by intros [z Hz] n; exists z; rewrite Hz|].
Robbert Krebbers's avatar
Robbert Krebbers committed
254
  intros Hxy; exists (y  x); apply equiv_dist=> n.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  by rewrite cmra_op_minus'.
256
Qed.
257 258 259
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
260 261
  - by intros x; exists (unit x); rewrite cmra_unit_r.
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
262
    by rewrite assoc -Hy -Hz.
263 264 265 266
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
  split; red; intros until 0; rewrite !cmra_included_includedN; first done.
267
  intros; etrans; eauto.
268
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
270
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
272 273
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
274
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
275
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
276
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
277 278 279 280 281 282 283
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.
284
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
285
Lemma cmra_included_r x y : y  x  y.
286
Proof. rewrite (comm op); apply cmra_included_l. Qed.
287

Robbert Krebbers's avatar
Robbert Krebbers committed
288 289 290 291 292
Lemma cmra_unit_preservingN n x y : x {n} y  unit x {n} unit y.
Proof.
  intros [z ->].
  apply cmra_included_includedN, cmra_unit_preserving, cmra_included_l.
Qed.
293 294
Lemma cmra_included_unit x : unit x  x.
Proof. by exists x; rewrite cmra_unit_l. Qed.
295
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
296
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
297
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
298
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
299
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
300
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
301
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
302
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
303

Robbert Krebbers's avatar
Robbert Krebbers committed
304
Lemma cmra_included_dist_l n x1 x2 x1' :
305
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Proof.
307 308
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Qed.
310

Robbert Krebbers's avatar
Robbert Krebbers committed
311
(** ** Timeless *)
312
Lemma cmra_timeless_included_l x y : Timeless x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314
Proof.
  intros ?? [x' ?].
315
  destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
316
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
317
Qed.
318
Lemma cmra_timeless_included_r n x y : Timeless y  x {0} y  x {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
320
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
321
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
322 323
Proof.
  intros ??? z Hz.
324
  destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
325
  { rewrite -?Hz. by apply cmra_valid_validN. }
326
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Qed.
328

329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346
(** ** Discrete *)
Lemma cmra_discrete_valid_iff `{CMRADiscrete A} n x :  x  {n} x.
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x  y  x {n} y.
Proof.
  split; first by rewrite cmra_included_includedN.
  intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A  Prop) :
  ( z,  (x  z)   y, P y   (y  z))  x ~~>: P.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
  ( z,  (x  z)   (y  z))  x ~~> y.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.

347 348 349
(** ** RAs with an empty element *)
Section identity.
  Context `{Empty A, !CMRAIdentity A}.
350 351
  Lemma cmra_empty_validN n : {n} .
  Proof. apply cmra_valid_validN, cmra_empty_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
  Lemma cmra_empty_leastN n x :  {n} x.
353 354 355 356
  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 ()  ().
357
  Proof. by intros x; rewrite (comm op) left_id. Qed.
358 359 360
  Lemma cmra_unit_empty : unit   .
  Proof. by rewrite -{2}(cmra_unit_l ) right_id. Qed.
End identity.
361

362
(** ** Local updates *)
363 364
Global Instance local_update_proper Lv (L : A  A) :
  LocalUpdate Lv L  Proper (() ==> ()) L.
365 366
Proof. intros; apply (ne_proper _). Qed.

367 368
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
369 370 371
Proof.
  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
Qed.
372 373

Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
374
Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
375

Ralf Jung's avatar
Ralf Jung committed
376 377 378
Global Instance local_update_id : LocalUpdate (λ _, True) (@id A).
Proof. split; auto with typeclass_instances. Qed.

379
(** ** Updates *)
380
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
381
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
382
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =).
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384
Proof.
  split.
385
  - by intros Hx z ?; exists y; split; [done|apply (Hx z)].
Robbert Krebbers's avatar
Robbert Krebbers committed
386
  - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
387
Qed.
388
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
Robbert Krebbers's avatar
Robbert Krebbers committed
389
Proof. by intros ? n z ?; exists x. Qed.
390
Lemma cmra_updateP_compose (P Q : A  Prop) x :
391
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
392
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
393
  intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y).
394
Qed.
395 396 397 398 399
Lemma cmra_updateP_compose_l (Q : A  Prop) x y : x ~~> y  y ~~>: Q  x ~~>: Q.
Proof.
  rewrite cmra_update_updateP.
  intros; apply cmra_updateP_compose with (y =); intros; subst; auto.
Qed.
400
Lemma cmra_updateP_weaken (P Q : A  Prop) x : x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
401
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
402

403
Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
404
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2))  x1  x2 ~~>: Q.
405
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
406 407 408
  intros Hx1 Hx2 Hy n z ?.
  destruct (Hx1 n (x2  z)) as (y1&?&?); first by rewrite assoc.
  destruct (Hx2 n (y1  z)) as (y2&?&?);
409 410
    first by rewrite assoc (comm _ x2) -assoc.
  exists (y1  y2); split; last rewrite (comm _ y1) -assoc; auto.
411
Qed.
412
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
413
  x1 ~~>: P1  x2 ~~>: P2  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
414
Proof. eauto 10 using cmra_updateP_op. Qed.
415
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
416
Proof.
417
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
418
Qed.
419 420
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
421 422 423 424

Section identity_updates.
  Context `{Empty A, !CMRAIdentity A}.
  Lemma cmra_update_empty x : x ~~> .
Robbert Krebbers's avatar
Robbert Krebbers committed
425
  Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
426
  Lemma cmra_update_empty_alt y :  ~~> y   x, x ~~> y.
427
  Proof. split; [intros; trans |]; auto using cmra_update_empty. Qed.
428
End identity_updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
429 430
End cmra.

431
(** * Properties about monotone functions *)
432
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
433
Proof. by split. Qed.
434 435
Instance cmra_monotone_compose {A B C : cmraT} (f : A  B) (g : B  C) :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (g  f).
436 437
Proof.
  split.
438 439
  - move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
440
Qed.
441

442 443 444 445 446 447
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.
448
  Lemma valid_preserving x :  x   f x.
449 450 451
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

452

453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
  eq_rect A id x _ H.

Section cmra_transport.
  Context {A B : cmraT} (H : A = B).
  Notation T := (cmra_transport H).
  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
  Proof. by intros ???; destruct H. Qed.
  Global Instance cmra_transport_proper : Proper (() ==> ()) T.
  Proof. by intros ???; destruct H. Qed.
  Lemma cmra_transport_op x y : T (x  y) = T x  T y.
  Proof. by destruct H. Qed.
  Lemma cmra_transport_unit x : T (unit x) = unit (T x).
  Proof. by destruct H. Qed.
468
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
469
  Proof. by destruct H. Qed.
470
  Lemma cmra_transport_valid x :  T x   x.
471 472 473 474 475 476 477 478 479 480 481
  Proof. by destruct H. Qed.
  Global Instance cmra_transport_timeless x : Timeless x  Timeless (T x).
  Proof. by destruct H. Qed.
  Lemma cmra_transport_updateP (P : A  Prop) (Q : B  Prop) x :
    x ~~>: P  ( y, P y  Q (T y))  T x ~~>: Q.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma cmra_transport_updateP' (P : A  Prop) x :
    x ~~>: P  T x ~~>: λ y,  y', y = cmra_transport H y'  P y'.
  Proof. eauto using cmra_transport_updateP. Qed.
End cmra_transport.

482 483 484 485 486 487
(** * 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;
488
  ra_validN_ne :> Proper (() ==> impl) valid;
489 490
  ra_minus_ne :> Proper (() ==> () ==> ()) minus;
  (* monoid *)
491 492
  ra_assoc :> Assoc () ();
  ra_comm :> Comm () ();
493
  ra_unit_l x : unit x  x  x;
494
  ra_unit_idemp x : unit (unit x)  unit x;
495 496 497 498 499
  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
}.

500
Section discrete.
501
  Context {A : cofeT} `{Discrete A}.
502
  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
503

504
  Instance discrete_validN : ValidN A := λ n x,  x.
505
  Definition discrete_cmra_mixin : CMRAMixin A.
506
  Proof.
507 508
    destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _); try done.
509 510 511
    - intros x; split; first done. by move=> /(_ 0).
    - intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
      apply (timeless _), dist_le with n; auto with lia.
512
  Qed.
513
  Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
514 515
  Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
516 517
End discrete.

518 519 520 521 522 523 524 525 526 527 528 529
(** ** 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.
530 531
  Global Instance unit_cmra_discrete : CMRADiscrete unitRA.
  Proof. by apply discrete_cmra_discrete. Qed.
532
End unit.
533

534
(** ** Product *)
535 536 537 538 539
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)).
540
  Instance prod_valid : Valid (A * B) := λ x,  x.1   x.2.
541
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
542 543 544 545 546 547 548 549 550 551 552 553 554 555
  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 _.
556 557 558 559
    - 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];
560
        split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
561 562 563
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
564 565 566 567 568
    - by intros n x [??]; split; apply cmra_validN_S.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
    - by split; rewrite /= cmra_unit_l.
    - by split; rewrite /= cmra_unit_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
569 570
    - intros x y; rewrite !prod_included.
      by intros [??]; split; apply cmra_unit_preserving.
571
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
    - intros x y; rewrite prod_included; intros [??].
573
      by split; apply cmra_op_minus.
574 575 576 577
    - intros n x y1 y2 [??] [??]; simpl in *.
      destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
      destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
      by exists ((z1.1,z2.1),(z1.2,z2.2)).
578
  Qed.
579
  Canonical Structure prodRA : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
580 581 582 583
  Global Instance prod_cmra_identity `{Empty A, Empty B} :
    CMRAIdentity A  CMRAIdentity B  CMRAIdentity prodRA.
  Proof.
    split.
584 585 586
    - split; apply cmra_empty_valid.
    - by split; rewrite /=left_id.
    - by intros ? [??]; split; apply (timeless _).
587
  Qed.
588 589 590 591
  Global Instance prod_cmra_discrete :
    CMRADiscrete A  CMRADiscrete B  CMRADiscrete prodRA.
  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.

592
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
593
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
594
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
595
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
596
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
597 598
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
599 600
    exists (a,b); repeat split; auto.
  Qed.
601
  Lemma prod_updateP' P1 P2 x :
602
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
603
  Proof. eauto using prod_updateP. Qed.
604 605 606 607 608
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).
609 610
Proof.
  split.
611
  - intros n x y; rewrite !prod_includedN; intros [??]; simpl.
612
    by split; apply includedN_preserving.
613
  - by intros n x [??]; split; simpl; apply validN_preserving.
614
Qed.