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.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Notation "x ≼{ n } y" := (includedN n x y)
32
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Instance: Params (@includedN) 4.
34
Hint Extern 0 (_ {_} _) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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'.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 *.
Robbert Krebbers's avatar
Robbert Krebbers committed
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. }
Robbert Krebbers's avatar
Robbert Krebbers committed
326
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
    by split; apply includedN_preserving.
613
  - by intros n x [??]; split; simpl; apply validN_preserving.
614
Qed.