cmra.v 23.5 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
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
Notation "x ≼{ n } y" := (includedN n x y)
33
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
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
53
54
55
  mixin_cmra_op_minus n x y : x {n} y  x  y  x {n} y;
  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
56
}.
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
  cmra_cofe_mixin : CofeMixin cmra_car;
69
  cmra_mixin : CMRAMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
70
}.
71
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
72
73
74
75
76
77
78
79
80
81
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Add Printing Constructor cmraT.
83
Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
84
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
Canonical Structure cmra_cofeC.

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

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

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

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

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

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

163
164
165
166
167
168
(** ** 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.
169
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
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
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.
200
201
202
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
204
205
206
207
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
  intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
209
210
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
211
212
213
214

(** ** Validity *)
Lemma cmra_valid_validN x :  x   n, {n} x.
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
216
217
218
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
219
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
220
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
221
222
223
224
225
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.
226
Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
227
Lemma cmra_unit_unit x : unit x  unit x  unit x.
228
Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Lemma cmra_unit_validN n x : {n} x  {n} unit x.
230
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
231
Lemma cmra_unit_valid x :  x   unit x.
232
233
234
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
237
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
238
  intros Hxy; exists (y  x); apply equiv_dist=> n.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
  symmetry; apply cmra_op_minus, Hxy.
Qed.
241
242
243
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
244
245
  - by intros x; exists (unit x); rewrite cmra_unit_r.
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
246
    by rewrite assoc -Hy -Hz.
247
248
249
250
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
  split; red; intros until 0; rewrite !cmra_included_includedN; first done.
251
  intros; etrans; eauto.
252
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
254
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
256
257
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
258
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
259
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
261
262
263
264
265
266
267
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.
268
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
269
Lemma cmra_included_r x y : y  x  y.
270
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271

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

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

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

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

316
317
318
(** ** RAs with an empty element *)
Section identity.
  Context `{Empty A, !CMRAIdentity A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
  Lemma cmra_empty_leastN n x :  {n} x.
320
321
322
323
  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 ()  ().
324
  Proof. by intros x; rewrite (comm op) left_id. Qed.
325
326
327
  Lemma cmra_unit_empty : unit   .
  Proof. by rewrite -{2}(cmra_unit_l ) right_id. Qed.
End identity.
Robbert Krebbers's avatar
Robbert Krebbers committed
328

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

334
335
336
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.
337
338

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

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

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

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

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

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

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

417

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

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

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

469
  Instance discrete_validN : ValidN A := λ n x,  x.
470
  Definition discrete_cmra_mixin : CMRAMixin A.
471
  Proof.
472
473
    destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _); try done.
474
    intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
475
    apply (timeless _), dist_le with n; auto with lia.
476
  Qed.
477
  Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
478
  Lemma discrete_updateP (x : discreteRA) (P : A  Prop) :
479
    ( z,  (x  z)   y, P y   (y  z))  x ~~>: P.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
  Proof. intros Hvalid n z; apply Hvalid. Qed.
481
  Lemma discrete_update (x y : discreteRA) :
482
    ( z,  (x  z)   (y  z))  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
  Proof. intros Hvalid n z; apply Hvalid. Qed.
484
485
  Lemma discrete_valid (x : discreteRA) : v x  validN_valid x.
  Proof. move=>Hx n. exact Hx. Qed.
486
487
End discrete.

488
489
490
491
492
493
494
495
496
497
498
499
500
501
(** ** 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.
502

503
(** ** Product *)
504
505
506
507
508
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)).
509
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
510
511
512
513
514
515
516
517
518
519
520
521
522
523
  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 _.
524
525
526
527
    - 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];
528
        split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
529
530
531
532
533
534
    - 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.
    - intros n x y; rewrite !prod_includedN.
535
      by intros [??]; split; apply cmra_unit_preservingN.
536
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
    - intros n x y; rewrite prod_includedN; intros [??].
538
      by split; apply cmra_op_minus.
539
540
541
542
    - 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)).
543
  Qed.
544
  Canonical Structure prodRA : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
545
546
547
548
  Global Instance prod_cmra_identity `{Empty A, Empty B} :
    CMRAIdentity A  CMRAIdentity B  CMRAIdentity prodRA.
  Proof.
    split.
549
550
551
    - split; apply cmra_empty_valid.
    - by split; rewrite /=left_id.
    - by intros ? [??]; split; apply (timeless _).
552
  Qed.
553
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
555
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
556
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
557
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
559
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
560
561
    exists (a,b); repeat split; auto.
  Qed.
562
  Lemma prod_updateP' P1 P2 x :
563
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
564
  Proof. eauto using prod_updateP. Qed.
565
566
567
568
569
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).
570
571
Proof.
  split.
572
  - intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
    by split; apply includedN_preserving.
574
  - by intros n x [??]; split; simpl; apply validN_preserving.
575
Qed.