cmra.v 23.7 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
24
Notation "✓{ n } x" := (validN n x)
  (at level 20, n at level 1, 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
Instance validN_valid `{ValidN A} : Valid A := λ x,  n, {n} x.

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

37
Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op 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_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  (* monoid *)
46
47
  mixin_cmra_assoc : Assoc () ();
  mixin_cmra_comm : Comm () ();
48
  mixin_cmra_unit_l x : unit x  x  x;
49
  mixin_cmra_unit_idemp 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
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} :=  n x y1 y2,
55
56
  {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
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
104
105
106
107
  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.
108
109
  Lemma cmra_unit_l x : unit x  x  x.
  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
110
111
  Lemma cmra_unit_idemp x : unit (unit x)  unit x.
  Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed.
112
113
114
115
  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.
116
  Lemma cmra_op_minus n x y : x {n} y  x  y  x {n} y.
117
118
  Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
  Lemma cmra_extend_op n x y1 y2 :
119
120
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }.
121
122
123
  Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
134
(** * Morphisms *)
135
136
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
  includedN_preserving n x y : x {n} y  f x {n} f y;
137
  validN_preserving n x : {n} x  {n} f x
138
139
}.

140
(** * Local updates *)
Ralf Jung's avatar
Ralf Jung committed
141
142
(** 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. *)
143
144
145
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
146
147
148
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
159
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Section cmra.
161
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Implicit Types x y z : A.
163
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
164

165
166
167
168
169
170
(** ** 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.
171
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
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
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.
202
203
204
205
206
207
208
209
210
211
212
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.
213
214
215
216
217
218
219
220
221

(** ** 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.
222
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
223
224
225
226
227
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.
228
Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
229
Lemma cmra_unit_unit x : unit x  unit x  unit x.
230
Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
231
Lemma cmra_unit_validN x n : {n} x  {n} unit x.
232
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
233
Lemma cmra_unit_valid x :  x   unit x.
234
235
236
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
239
240
241
242
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.
243
244
245
246
247
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).
248
    by rewrite assoc -Hy -Hz.
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
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.
270
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
271
Lemma cmra_included_r x y : y  x  y.
272
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
273

274
275
276
277
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.
278
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
279
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
280
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
281
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
282
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
283
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
284
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
285
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
286
287

Lemma cmra_included_dist_l x1 x2 x1' n :
288
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
Proof.
290
291
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
Qed.
293
294
295

(** ** Minus *)
Lemma cmra_op_minus' x y : x  y  x  y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Proof.
297
  rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299

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

318
319
320
321
322
323
324
325
(** ** 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 ()  ().
326
  Proof. by intros x; rewrite (comm op) left_id. Qed.
327
328
329
  Lemma cmra_unit_empty : unit   .
  Proof. by rewrite -{2}(cmra_unit_l ) right_id. Qed.
End identity.
Robbert Krebbers's avatar
Robbert Krebbers committed
330

331
(** ** Local updates *)
332
333
Global Instance local_update_proper Lv (L : A  A) :
  LocalUpdate Lv L  Proper (() ==> ()) L.
334
335
Proof. intros; apply (ne_proper _). Qed.

336
337
338
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.
339
340

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

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

346
(** ** Updates *)
347
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
349
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =).
Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
352
353
354
Proof.
  split.
  * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
  * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
Qed.
355
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
356
Proof. by intros ? z n ?; exists x. Qed.
357
Lemma cmra_updateP_compose (P Q : A  Prop) x :
358
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
359
360
361
Proof.
  intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y).
Qed.
362
363
364
365
366
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.
367
Lemma cmra_updateP_weaken (P Q : A  Prop) x : x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
368
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
369

370
Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
371
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2))  x1  x2 ~~>: Q.
372
373
Proof.
  intros Hx1 Hx2 Hy z n ?.
374
  destruct (Hx1 (x2  z) n) as (y1&?&?); first by rewrite assoc.
375
  destruct (Hx2 (y1  z) n) as (y2&?&?);
376
377
    first by rewrite assoc (comm _ x2) -assoc.
  exists (y1  y2); split; last rewrite (comm _ y1) -assoc; auto.
378
Qed.
379
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
380
  x1 ~~>: P1  x2 ~~>: P2  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
381
Proof. eauto 10 using cmra_updateP_op. Qed.
382
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
383
Proof.
384
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
385
Qed.
386
387
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
388
389
390
391
392
393
394
395

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
396
397
End cmra.

398
(** * Properties about monotone functions *)
399
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
400
Proof. by split. Qed.
401
402
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
403
404
Proof.
  split.
405
406
  * 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
407
Qed.
408

409
410
411
412
413
414
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.
415
  Lemma valid_preserving x :  x   f x.
416
417
418
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

419

420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
(** * 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.
435
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
436
  Proof. by destruct H. Qed.
437
  Lemma cmra_transport_valid x :  T x   x.
438
439
440
441
442
443
444
445
446
447
448
  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.

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;
455
  ra_validN_ne :> Proper (() ==> impl) valid;
456
457
  ra_minus_ne :> Proper (() ==> () ==> ()) minus;
  (* monoid *)
458
459
  ra_assoc :> Assoc () ();
  ra_comm :> Comm () ();
460
  ra_unit_l x : unit x  x  x;
461
  ra_unit_idemp x : unit (unit x)  unit x;
462
463
464
465
466
  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
}.

467
Section discrete.
468
469
470
  Context {A : cofeT} `{ x : A, Timeless x}.
  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).

471
  Instance discrete_validN : ValidN A := λ n x,  x.
472
  Definition discrete_cmra_mixin : CMRAMixin A.
473
  Proof.
474
475
    by destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _ _ _).
476
  Qed.
477
  Definition discrete_extend_mixin : CMRAExtendMixin A.
478
  Proof.
479
480
    intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
    apply (timeless _), dist_le with n; auto with lia.
481
  Qed.
482
  Definition discreteRA : cmraT :=
483
    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
484
  Lemma discrete_updateP (x : discreteRA) (P : A  Prop) :
485
    ( z,  (x  z)   y, P y   (y  z))  x ~~>: P.
486
  Proof. intros Hvalid z n; apply Hvalid. Qed.
487
  Lemma discrete_update (x y : discreteRA) :
488
    ( z,  (x  z)   (y  z))  x ~~> y.
489
  Proof. intros Hvalid z n; apply Hvalid. Qed.
490
491
End discrete.

492
493
494
495
496
497
498
499
500
501
502
503
504
505
(** ** 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.
506

507
(** ** Product *)
508
509
510
511
512
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)).
513
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
  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.
533
    * by intros n x [??]; split; apply cmra_validN_S.
534
535
536
537
    * by split; rewrite /= assoc.
    * by split; rewrite /= comm.
    * by split; rewrite /= cmra_unit_l.
    * by split; rewrite /= cmra_unit_idemp.
538
    * intros n x y; rewrite !prod_includedN.
539
540
      by intros [??]; split; apply cmra_unit_preservingN.
    * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
541
542
543
544
545
546
547
548
549
550
551
552
    * 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.
553
554
555
556
557
558
559
560
  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.
561
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
562
  Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
563
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
564
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
565
566
567
568
569
  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.
570
  Lemma prod_updateP' P1 P2 x :
571
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
572
  Proof. eauto using prod_updateP. Qed.
573
574
575
576
577
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).
578
579
Proof.
  split.
580
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
581
    by split; apply includedN_preserving.
582
583
  * by intros n x [??]; split; simpl; apply validN_preserving.
Qed.