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;
51
52
  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;
53
54
55
56
  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
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.
115
116
117
118
  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.
119
  Lemma cmra_op_minus n x y : x {n} y  x  y  x {n} 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
246
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

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

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

284
285
286
287
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.
288
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
289
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
290
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
291
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
292
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
293
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
294
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
295
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
296

Robbert Krebbers's avatar
Robbert Krebbers committed
297
Lemma cmra_included_dist_l n x1 x2 x1' :
298
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Proof.
300
301
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
Qed.
303
304
305

(** ** Minus *)
Lemma cmra_op_minus' x y : x  y  x  y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Proof.
307
  rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
309

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

328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
(** ** 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.

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

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

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

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

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

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

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

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

430
(** * Properties about monotone functions *)
431
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
432
Proof. by split. Qed.
433
434
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
435
436
Proof.
  split.
437
438
  - 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
439
Qed.
440

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

451

452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
(** * 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.
467
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
468
  Proof. by destruct H. Qed.
469
  Lemma cmra_transport_valid x :  T x   x.
470
471
472
473
474
475
476
477
478
479
480
  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.

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

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

503
  Instance discrete_validN : ValidN A := λ n x,  x.
504
  Definition discrete_cmra_mixin : CMRAMixin A.
505
  Proof.
506
507
    destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _); try done.
508
509
510
    - 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.
511
  Qed.
512
  Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
513
514
  Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
515
516
End discrete.

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

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

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