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

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

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

175 176 177 178 179 180
(** ** 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.
181
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
182 183 184 185 186 187 188 189 190 191 192
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 _).
193 194 195 196
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
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.
215 216 217
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
219 220 221 222
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
224 225
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
226 227

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

(** ** Units *)
Lemma cmra_unit_r x : x  unit x  x.
239
Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
240
Lemma cmra_unit_unit x : unit x  unit x  unit x.
241
Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
Lemma cmra_unit_validN n x : {n} x  {n} unit x.
243
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
244
Lemma cmra_unit_valid x :  x   unit x.
245 246
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
247 248 249 250
(** ** 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.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
289 290 291 292 293
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.
294 295
Lemma cmra_included_unit x : unit x  x.
Proof. by exists x; rewrite cmra_unit_l. Qed.
296
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
297
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
298
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
299
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
300
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
301
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
302
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
303
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
304

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

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

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

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

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

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

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

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

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

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

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

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

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

456 457 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.
  Lemma cmra_transport_unit x : T (unit x) = unit (T x).
  Proof. by destruct H. Qed.
471
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
472
  Proof. by destruct H. Qed.
473
  Lemma cmra_transport_valid x :  T x   x.
474 475 476 477 478 479 480 481 482 483 484
  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.

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

503
Section discrete.
504
  Context {A : cofeT} `{Discrete A}.
505
  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
506

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

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

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

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