cmra.v 26.9 KB
Newer Older
1
From iris.algebra Require Export cofe.
2

Ralf Jung's avatar
Ralf Jung committed
3
4
Class Core (A : Type) := core : A  A.
Instance: Params (@core) 2.
5
6
7
8
9
10
11
12
13

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
Instance: Params (@included) 3.

17
18
19
Class Div (A : Type) := div : A  A  A.
Instance: Params (@div) 2.
Infix "÷" := div : 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
Record CMRAMixin A
Ralf Jung's avatar
Ralf Jung committed
37
    `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A, Div A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  (* setoids *)
39
  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
Ralf Jung's avatar
Ralf Jung committed
40
  mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
41
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
42
  mixin_cmra_div_ne n : Proper (dist n ==> dist n ==> dist n) div;
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 () ();
Ralf Jung's avatar
Ralf Jung committed
49
50
51
  mixin_cmra_core_l x : core x  x  x;
  mixin_cmra_core_idemp x : core (core x)  core x;
  mixin_cmra_core_preserving x y : x  y  core x  core y;
52
  mixin_cmra_validN_op_l n x y : {n} (x  y)  {n} x;
53
  mixin_cmra_op_div 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
(** Bundeled version *)
Structure cmraT := CMRAT {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_compl : Compl cmra_car;
Ralf Jung's avatar
Ralf Jung committed
65
  cmra_core : Core cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  cmra_op : Op cmra_car;
67
  cmra_valid : Valid cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  cmra_validN : ValidN cmra_car;
69
  cmra_div : Div 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
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_compl : simpl never.
Ralf Jung's avatar
Ralf Jung committed
78
Arguments cmra_core : simpl never.
79
Arguments cmra_op : simpl never.
80
Arguments cmra_valid : simpl never.
81
Arguments cmra_validN : simpl never.
82
Arguments cmra_div : simpl never.
83
84
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Add Printing Constructor cmraT.
Ralf Jung's avatar
Ralf Jung committed
86
Existing Instances cmra_core cmra_op cmra_valid cmra_validN cmra_div.
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
(** 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.
Ralf Jung's avatar
Ralf Jung committed
96
97
  Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
  Proof. apply (mixin_cmra_core_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_div_ne n :
    Proper (dist n ==> dist n ==> dist n) (@div A _).
  Proof. apply (mixin_cmra_div_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.
Ralf Jung's avatar
Ralf Jung committed
111
112
113
114
115
116
  Lemma cmra_core_l x : core x  x  x.
  Proof. apply (mixin_cmra_core_l _ (cmra_mixin A)). Qed.
  Lemma cmra_core_idemp x : core (core x)  core x.
  Proof. apply (mixin_cmra_core_idemp _ (cmra_mixin A)). Qed.
  Lemma cmra_core_preserving x y : x  y  core x  core y.
  Proof. apply (mixin_cmra_core_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.
119
120
  Lemma cmra_op_div x y : x  y  x  y ÷ x  y.
  Proof. apply (mixin_cmra_op_div _ (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.

Ralf Jung's avatar
Ralf Jung committed
127
(** * CMRAs with a unit element *)
128
(** We use the notation  because for most instances (maps, sets, etc) the
Ralf Jung's avatar
Ralf Jung committed
129
130
131
132
133
`empty' element is the unit. *)
Class CMRAUnit (A : cmraT) `{Empty A} := {
  cmra_unit_valid :  ;
  cmra_unit_left_id :> LeftId ()  ();
  cmra_unit_timeless :> Timeless 
134
}.
Ralf Jung's avatar
Ralf Jung committed
135
Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate .
136

137
(** * Discrete CMRAs *)
138
Class CMRADiscrete (A : cmraT) := {
139
140
141
142
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
143
(** * Morphisms *)
144
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
147
  cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
  validN_preserving n x : {n} x  {n} f x;
  included_preserving x y : x  y  f x  f y
148
}.
149
150
Arguments validN_preserving {_ _} _ {_} _ _ _.
Arguments included_preserving {_ _} _ {_} _ _ _.
151

152
(** * Local updates *)
Ralf Jung's avatar
Ralf Jung committed
153
154
(** 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. *)
155
156
157
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
158
159
160
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

161
(** * Frame preserving updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  n z,
163
  {n} (x  z)   y, P y  {n} (y  z).
164
Instance: Params (@cmra_updateP) 1.
165
Infix "~~>:" := cmra_updateP (at level 70).
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Definition cmra_update {A : cmraT} (x y : A) :=  n z,
167
  {n} (x  z)  {n} (y  z).
168
Infix "~~>" := cmra_update (at level 70).
169
Instance: Params (@cmra_update) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
170

Robbert Krebbers's avatar
Robbert Krebbers committed
171
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Section cmra.
173
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Implicit Types x y z : A.
175
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
176

177
(** ** Setoids *)
Ralf Jung's avatar
Ralf Jung committed
178
Global Instance cmra_core_proper : Proper (() ==> ()) (@core A _).
179
180
181
182
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.
183
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
184
185
186
187
188
189
190
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.
191
Global Instance cmra_div_proper : Proper (() ==> () ==> ()) (@div A _).
192
193
194
Proof. apply (ne_proper_2 _). Qed.

Global Instance cmra_valid_proper : Proper (() ==> iff) (@valid A _).
195
196
197
198
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
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.
217
218
219
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
221
222
223
224
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
226
227
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
228
229

(** ** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
231
232
233
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
234
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
235
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
236
237
238
Lemma cmra_valid_op_r x y :  (x  y)   y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.

Ralf Jung's avatar
Ralf Jung committed
239
240
241
242
243
244
245
246
247
(** ** Core *)
Lemma cmra_core_r x : x  core x  x.
Proof. by rewrite (comm _ x) cmra_core_l. Qed.
Lemma cmra_core_core x : core x  core x  core x.
Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
Lemma cmra_core_validN n x : {n} x  {n} core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_core_valid x :  x   core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
248

249
250
251
(** ** Div *)
Lemma cmra_op_div' n x y : x {n} y  x  y ÷ x {n} y.
Proof. intros [z ->]. by rewrite cmra_op_div; last exists z. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
252

253
(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
256
Lemma cmra_included_includedN x y : x  y   n, x {n} y.
Proof.
  split; [by intros [z Hz] n; exists z; rewrite Hz|].
257
258
  intros Hxy; exists (y ÷ x); apply equiv_dist=> n.
  by rewrite cmra_op_div'.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
Qed.
260
261
262
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
263
  - by intros x; exists (core x); rewrite cmra_core_r.
264
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
265
    by rewrite assoc -Hy -Hz.
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.
270
  intros; etrans; eauto.
271
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
273
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
275
276
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
277
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
278
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
280
281
282
283
284
285
286
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.
287
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
288
Lemma cmra_included_r x y : y  x  y.
289
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
290

Ralf Jung's avatar
Ralf Jung committed
291
Lemma cmra_core_preservingN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
293
Proof.
  intros [z ->].
Ralf Jung's avatar
Ralf Jung committed
294
  apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Qed.
Ralf Jung's avatar
Ralf Jung committed
296
297
Lemma cmra_included_core x : core x  x.
Proof. by exists x; rewrite cmra_core_l. Qed.
298
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
299
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
300
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
301
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
302
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
303
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
304
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
305
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
306

Robbert Krebbers's avatar
Robbert Krebbers committed
307
Lemma cmra_included_dist_l n x1 x2 x1' :
308
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof.
310
311
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
312
Qed.
313

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

332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
(** ** 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.

Ralf Jung's avatar
Ralf Jung committed
350
351
352
353
354
355
(** ** RAs with a unit element *)
Section unit.
  Context `{Empty A, !CMRAUnit A}.
  Lemma cmra_unit_validN n : {n} .
  Proof. apply cmra_valid_validN, cmra_unit_valid. Qed.
  Lemma cmra_unit_leastN n x :  {n} x.
356
  Proof. by exists x; rewrite left_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
357
  Lemma cmra_unit_least x :   x.
358
  Proof. by exists x; rewrite left_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
359
  Global Instance cmra_unit_right_id : RightId ()  ().
360
  Proof. by intros x; rewrite (comm op) left_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
361
  Lemma cmra_core_unit : core   .
Ralf Jung's avatar
Ralf Jung committed
362
  Proof. by rewrite -{2}(cmra_core_l ) right_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
363
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
364

365
(** ** Local updates *)
366
367
Global Instance local_update_proper Lv (L : A  A) :
  LocalUpdate Lv L  Proper (() ==> ()) L.
368
369
Proof. intros; apply (ne_proper _). Qed.

370
371
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
372
373
374
Proof.
  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
Qed.
375
376

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
425
426
427
Section unit_updates.
  Context `{Empty A, !CMRAUnit A}.
  Lemma cmra_update_unit x : x ~~> .
Robbert Krebbers's avatar
Robbert Krebbers committed
428
  Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
429
430
431
  Lemma cmra_update_unit_alt y :  ~~> y   x, x ~~> y.
  Proof. split; [intros; trans |]; auto using cmra_update_unit. Qed.
End unit_updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
433
End cmra.

434
(** * Properties about monotone functions *)
435
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Robbert Krebbers's avatar
Robbert Krebbers committed
436
Proof. repeat split; by try apply _. Qed.
437
438
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
439
440
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
  - apply _. 
442
  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
Qed.
445

446
447
Section cmra_monotone.
  Context {A B : cmraT} (f : A  B) `{!CMRAMonotone f}.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
449
  Global Instance cmra_monotone_proper : Proper (() ==> ()) f := ne_proper _.
  Lemma includedN_preserving n x y : x {n} y  f x {n} f y.
450
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
451
    intros [z ->].
452
    apply cmra_included_includedN, (included_preserving f), cmra_included_l.
453
  Qed.
454
  Lemma valid_preserving x :  x   f x.
455
456
457
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

458
459
460
461
462
463
464
465
466
467
468
469
470
(** * 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.
Ralf Jung's avatar
Ralf Jung committed
471
  Lemma cmra_transport_core x : T (core x) = core (T x).
472
  Proof. by destruct H. Qed.
473
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
474
  Proof. by destruct H. Qed.
475
  Lemma cmra_transport_valid x :  T x   x.
476
477
478
479
480
481
482
483
484
485
486
  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.

487
488
(** * Instances *)
(** ** Discrete CMRA *)
Ralf Jung's avatar
Ralf Jung committed
489
Class RA A `{Equiv A, Core A, Op A, Valid A, Div A} := {
490
491
  (* setoids *)
  ra_op_ne (x : A) : Proper (() ==> ()) (op x);
Ralf Jung's avatar
Ralf Jung committed
492
  ra_core_ne :> Proper (() ==> ()) core;
493
  ra_validN_ne :> Proper (() ==> impl) valid;
494
  ra_div_ne :> Proper (() ==> () ==> ()) div;
495
  (* monoid *)
496
497
  ra_assoc :> Assoc () ();
  ra_comm :> Comm () ();
Ralf Jung's avatar
Ralf Jung committed
498
499
500
  ra_core_l x : core x  x  x;
  ra_core_idemp x : core (core x)  core x;
  ra_core_preserving x y : x  y  core x  core y;
501
  ra_valid_op_l x y :  (x  y)   x;
502
  ra_op_div x y : x  y  x  y ÷ x  y
503
504
}.

505
Section discrete.
506
  Context {A : cofeT} `{Discrete A}.
Ralf Jung's avatar
Ralf Jung committed
507
  Context `{Core A, Op A, Valid A, Div A} (ra : RA A).
508

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

523
524
525
(** ** CMRA for the unit type *)
Section unit.
  Instance unit_valid : Valid () := λ x, True.
Ralf Jung's avatar
Ralf Jung committed
526
  Instance unit_core : Core () := λ x, x.
527
  Instance unit_op : Op () := λ x y, ().
528
  Instance unit_div : Div () := λ x y, ().
529
530
531
  Global Instance unit_empty : Empty () := ().
  Definition unit_ra : RA ().
  Proof. by split. Qed.
532
533
  Canonical Structure unitR : cmraT :=
    Eval cbv [unitC discreteR cofe_car] in discreteR unit_ra.
Ralf Jung's avatar
Ralf Jung committed
534
  Global Instance unit_cmra_unit : CMRAUnit unitR.
535
  Global Instance unit_cmra_discrete : CMRADiscrete unitR.
536
  Proof. by apply discrete_cmra_discrete. Qed.
537
End unit.
538

539
(** ** Product *)
540
541
542
543
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) := (, ).
Ralf Jung's avatar
Ralf Jung committed
544
  Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
545
  Instance prod_valid : Valid (A * B) := λ x,  x.1   x.2.
546
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
547
  Instance prod_div : Div (A * B) := λ x y, (x.1 ÷ y.1, x.2 ÷ y.2).
548
549
550
551
552
553
554
555
556
557
558
559
560
  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 _.
561
562
563
564
    - 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];
565
        split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
566
567
568
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
569
570
571
    - by intros n x [??]; split; apply cmra_validN_S.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
Ralf Jung's avatar
Ralf Jung committed
572
573
    - by split; rewrite /= cmra_core_l.
    - by split; rewrite /= cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
574
    - intros x y; rewrite !prod_included.
Ralf Jung's avatar
Ralf Jung committed
575
      by intros [??]; split; apply cmra_core_preserving.
576
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
    - intros x y; rewrite prod_included; intros [??].
578
      by split; apply cmra_op_div.
579
580
581
582
    - 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)).
583
  Qed.
584
  Canonical Structure prodR : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
Ralf Jung's avatar
Ralf Jung committed
585
586
  Global Instance prod_cmra_unit `{Empty A, Empty B} :
    CMRAUnit A  CMRAUnit B  CMRAUnit prodR.
587
588
  Proof.
    split.
Ralf Jung's avatar
Ralf Jung committed
589
    - split; apply cmra_unit_valid.
590
591
    - by split; rewrite /=left_id.
    - by intros ? [??]; split; apply (timeless _).
592
  Qed.
593
  Global Instance prod_cmra_discrete :
594
    CMRADiscrete A  CMRADiscrete B  CMRADiscrete prodR.
595
596
  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.

597
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
599
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
600
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
601
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
603
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
604
605
    exists (a,b); repeat split; auto.
  Qed.
606
  Lemma prod_updateP' P1 P2 x :
607
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
608
  Proof. eauto using prod_updateP. Qed.
609
End prod.
610
Arguments prodR : clear implicits.
611
612
613

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).
614
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
  split; first apply _.
616
  - by intros n x [??]; split; simpl; apply validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
618
  - intros x y; rewrite !prod_included=> -[??] /=.
    by split; apply included_preserving.
619
Qed.
620
621
622
623
624
625

(** Functors *)
Structure rFunctor := RFunctor {
  rFunctor_car : cofeT  cofeT -> cmraT;
  rFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
626
627
  rFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
628
629
630
631
632
633
634
  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x  x;
  rFunctor_compose {A1 A2 A3 B1 B2 B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    rFunctor_map (fg, g'◎f') x  rFunctor_map (g,g') (rFunctor_map (f,f') x);
  rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CMRAMonotone (rFunctor_map fg) 
}.
635
Existing Instances rFunctor_ne rFunctor_mono.
636
637
Instance: Params (@rFunctor_map) 5.

638
639
640
Class rFunctorContractive (F : rFunctor) :=
  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).

641
642
643
644
645
646
647
Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
Coercion rFunctor_diag : rFunctor >-> Funclass.

Program Definition constRF (B : cmraT) : rFunctor :=
  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.

648
Instance constRF_contractive B : rFunctorContractive (constRF B).
649
Proof. rewrite /rFunctorContractive; apply _. Qed.
650

651
652
653
654
655
Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
  rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
  rFunctor_map A1 A2 B1 B2 fg :=
    prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
656
657
658
Next Obligation.
  intros F1 F2 A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_ne.
Qed.
659
660
661
662
663
Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
Next Obligation.
  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
  by rewrite !rFunctor_compose.
Qed.
664
665
666
667
668
669
670
671

Instance prodRF_contractive F1 F2 :
  rFunctorContractive F1  rFunctorContractive F2 
  rFunctorContractive (prodRF F1 F2).
Proof.
  intros ?? A1 A2 B1 B2 n ???;
    by apply prodC_map_ne; apply rFunctor_contractive.
Qed.