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

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
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
Ralf Jung's avatar
Ralf Jung committed
27
Notation "✓" := valid (at level 1) : C_scope.
28
29
Instance validN_valid `{ValidN A} : Valid A := λ x,  n, {n} x.

30
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y {n} x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
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
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  (* monoid *)
45
46
47
48
  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;
49
50
  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;
51
  mixin_cmra_op_minus n x y : x {n} y  x  y  x {n} y
Robbert Krebbers's avatar
Robbert Krebbers committed
52
}.
53
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} :=  n x y1 y2,
54
55
  {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
56

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

88
89
90
91
92
93
94
95
(** 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.
96
97
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
98
99
100
  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.
101
102
103
104
105
106
107
108
109
110
111
112
113
114
  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.
115
  Lemma cmra_op_minus n x y : x {n} y  x  y  x {n} y.
116
117
  Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
  Lemma cmra_extend_op n x y1 y2 :
118
119
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }.
120
121
122
  Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.

123
124
125
126
127
128
129
130
(** * 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 
}.
131
Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate .
132

Robbert Krebbers's avatar
Robbert Krebbers committed
133
(** * Morphisms *)
134
135
136
137
138
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)
}.

139
140
141
142
143
144
145
(** * Local updates *)
Class LocalUpdate {A : cmraT} (P : A  Prop) (f : A  A) := {
  local_update_ne n :> Proper (dist n ==> dist n) f;
  local_updateN n x y : P x  {n} (x  y)  f (x  y) {n} f x  y
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
156
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Section cmra.
158
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Implicit Types x y z : A.
160
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
(** ** 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.
199
200
201
202
203
204
205
206
207
208
209
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
  intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
  intros x1 x2 Hx P1 P2 HP; split=>Hup z n;
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233

(** ** 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
234
235
236
237
238
239
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.
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
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_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
270

271
272
273
274
275
276
277
278
279
280
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 :
281
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
Proof.
283
284
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
Qed.
286
287
288

(** ** Minus *)
Lemma cmra_op_minus' x y : x  y  x  y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
Proof.
290
  rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
292

Robbert Krebbers's avatar
Robbert Krebbers committed
293
(** ** Timeless *)
294
Lemma cmra_timeless_included_l x y : Timeless x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296
Proof.
  intros ?? [x' ?].
297
  destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Qed.
300
Lemma cmra_timeless_included_r n x y : Timeless y  x {0} y  x {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
302
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
303
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
Proof.
  intros ??? z Hz.
306
  destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
307
  { by rewrite -?Hz. }
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310

311
312
313
314
315
316
317
318
319
320
321
322
(** ** 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
323

324
325
326
327
328
329
330
331
332
333
334
335
(** ** Local updates *)
Global Instance local_update_proper P (f : A  A) :
  LocalUpdate P f  Proper (() ==> ()) f.
Proof. intros; apply (ne_proper _). Qed.

Lemma local_update f `{!LocalUpdate P f} x y :
  P x   (x  y)  f (x  y)  f x  y.
Proof. by rewrite equiv_dist=>?? n; apply (local_updateN f). Qed.

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

336
(** ** Updates *)
337
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
339
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =).
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
343
344
Proof.
  split.
  * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
  * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
Qed.
345
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
346
Proof. by intros ? z n ?; exists x. Qed.
347
Lemma cmra_updateP_compose (P Q : A  Prop) x :
348
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
349
350
351
Proof.
  intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y).
Qed.
352
353
354
355
356
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.
357
Lemma cmra_updateP_weaken (P Q : A  Prop) x : x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
358
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
359

360
Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
361
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2))  x1  x2 ~~>: Q.
362
363
364
365
366
367
368
Proof.
  intros Hx1 Hx2 Hy z n ?.
  destruct (Hx1 (x2  z) n) as (y1&?&?); first by rewrite associative.
  destruct (Hx2 (y1  z) n) as (y2&?&?);
    first by rewrite associative (commutative _ x2) -associative.
  exists (y1  y2); split; last rewrite (commutative _ y1) -associative; auto.
Qed.
369
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
370
  x1 ~~>: P1  x2 ~~>: P2  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
371
Proof. eauto 10 using cmra_updateP_op. Qed.
372
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
373
Proof.
374
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
375
Qed.
376
377
378
379
380
381
382
383

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

386
(** * Properties about monotone functions *)
387
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
388
Proof. by split. Qed.
389
390
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
391
392
Proof.
  split.
393
394
  * 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
395
Qed.
396

397
398
399
400
401
402
403
404
405
406
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.

407

408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
(** * 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.
  Lemma cmra_transport_validN n x : {n} (T x)  {n} x.
  Proof. by destruct H. Qed.
  Lemma cmra_transport_valid x :  (T x)   x.
  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.

437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
(** * 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
}.

455
Section discrete.
456
457
458
  Context {A : cofeT} `{ x : A, Timeless x}.
  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).

459
  Instance discrete_validN : ValidN A := λ n x,  x.
460
  Definition discrete_cmra_mixin : CMRAMixin A.
461
  Proof.
462
463
    by destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _ _ _).
464
  Qed.
465
  Definition discrete_extend_mixin : CMRAExtendMixin A.
466
  Proof.
467
468
    intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
    apply (timeless _), dist_le with n; auto with lia.
469
  Qed.
470
  Definition discreteRA : cmraT :=
471
    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
472
  Lemma discrete_updateP (x : discreteRA) (P : A  Prop) :
473
    ( z,  (x  z)   y, P y   (y  z))  x ~~>: P.
474
  Proof. intros Hvalid z n; apply Hvalid. Qed.
475
  Lemma discrete_update (x y : discreteRA) :
476
    ( z,  (x  z)   (y  z))  x ~~> y.
477
  Proof. intros Hvalid z n; apply Hvalid. Qed.
478
479
End discrete.

480
481
482
483
484
485
486
487
488
489
490
491
492
493
(** ** 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.
494

495
(** ** Product *)
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
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.
521
    * by intros n x [??]; split; apply cmra_validN_S.
522
523
    * split; simpl; apply (associative _).
    * split; simpl; apply (commutative _).
524
525
    * split; simpl; apply cmra_unit_l.
    * split; simpl; apply cmra_unit_idempotent.
526
    * intros n x y; rewrite !prod_includedN.
527
528
      by intros [??]; split; apply cmra_unit_preservingN.
    * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
529
530
531
532
533
534
535
536
537
538
539
540
    * 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.
541
542
543
544
545
546
547
548
  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.
549
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
550
  Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
551
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
552
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
553
554
555
556
557
  Proof.
    intros Hx1 Hx2 HP z n [??]; simpl in *.
    destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto.
    exists (a,b); repeat split; auto.
  Qed.
558
  Lemma prod_updateP' P1 P2 x :
559
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
560
  Proof. eauto using prod_updateP. Qed.
561
562
563
564
565
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).
566
567
Proof.
  split.
568
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
    by split; apply includedN_preserving.
570
571
  * by intros n x [??]; split; simpl; apply validN_preserving.
Qed.