cmra.v 23.5 KB
Newer Older
1
From algebra Require Export cofe.
2 3 4 5 6 7 8 9 10 11 12 13

Class Unit (A : Type) := unit : A  A.
Instance: Params (@unit) 2.

Class Op (A : Type) := op : A  A  A.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

Definition included `{Equiv A, Op A} (x y : A) :=  z, y  x  z.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
14
Hint Extern 0 (_  _) => reflexivity.
15 16 17 18 19
Instance: Params (@included) 3.

Class Minus (A : Type) := minus : A  A  A.
Instance: Params (@minus) 2.
Infix "⩪" := minus (at level 40) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22

Class ValidN (A : Type) := validN : nat  A  Prop.
Instance: Params (@validN) 3.
23 24
Notation "✓{ n } x" := (validN n x)
  (at level 20, n at level 1, format "✓{ n }  x").
Robbert Krebbers's avatar
Robbert Krebbers committed
25

26 27
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
28
Notation "✓ x" := (valid x) (at level 20) : C_scope.
29 30
Instance validN_valid `{ValidN A} : Valid A := λ x,  n, {n} x.

31
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y {n} x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
32 33 34
Notation "x ≼{ n } y" := (includedN n x y)
  (at level 70, format "x  ≼{ n }  y") : C_scope.
Instance: Params (@includedN) 4.
35
Hint Extern 0 (_ {_} _) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37
Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  (* setoids *)
39 40
  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
  mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
41
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
42
  mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  (* valid *)
44
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  (* monoid *)
46 47
  mixin_cmra_assoc : Assoc () ();
  mixin_cmra_comm : Comm () ();
48
  mixin_cmra_unit_l x : unit x  x  x;
49
  mixin_cmra_unit_idemp x : unit (unit x)  unit x;
50 51
  mixin_cmra_unit_preservingN n x y : x {n} y  unit x {n} unit y;
  mixin_cmra_validN_op_l n x y : {n} (x  y)  {n} x;
52
  mixin_cmra_op_minus n x y : x {n} y  x  y  x {n} y
Robbert Krebbers's avatar
Robbert Krebbers committed
53
}.
54
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} :=  n x y1 y2,
55 56
  {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 59 60 61 62 63 64 65 66 67
(** Bundeled version *)
Structure cmraT := CMRAT {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_compl : Compl cmra_car;
  cmra_unit : Unit cmra_car;
  cmra_op : Op cmra_car;
  cmra_validN : ValidN cmra_car;
  cmra_minus : Minus cmra_car;
68 69 70
  cmra_cofe_mixin : CofeMixin cmra_car;
  cmra_mixin : CMRAMixin cmra_car;
  cmra_extend_mixin : CMRAExtendMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
71
}.
72
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _.
73 74 75 76 77 78 79 80 81 82 83
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_compl : simpl never.
Arguments cmra_unit : simpl never.
Arguments cmra_op : simpl never.
Arguments cmra_validN : simpl never.
Arguments cmra_minus : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Arguments cmra_extend_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Add Printing Constructor cmraT.
85
Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
86
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88
Canonical Structure cmra_cofeC.

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

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

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

140
(** * Local updates *)
141 142 143
Class LocalUpdate {A : cmraT} (Lv : A  Prop) (L : A  A) := {
  local_update_ne n :> Proper (dist n ==> dist n) L;
  local_updateN n x y : Lv x  {n} (x  y)  L (x  y) {n} L x  y
144 145 146
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

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

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

163 164 165 166 167 168
(** ** Setoids *)
Global Instance cmra_unit_proper : Proper (() ==> ()) (@unit A _).
Proof. apply (ne_proper _). Qed.
Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
Proof.
  intros x1 x2 Hx y1 y2 Hy.
169
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
Qed.
Global Instance ra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
Global Instance cmra_validN_proper : Proper (() ==> iff) (@validN A _ n) | 1.
Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
Global Instance cmra_minus_proper : Proper (() ==> () ==> ()) (@minus A _).
Proof. apply (ne_proper_2 _). Qed.

Global Instance cmra_valid_proper : Proper (() ==> iff) (@valid A _).
Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed.
Global Instance cmra_includedN_ne n :
  Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_includedN_proper n :
  Proper (() ==> () ==> iff) (@includedN A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
  by rewrite (Hx n) (Hy n).
Qed.
Global Instance cmra_included_proper :
  Proper (() ==> () ==> iff) (@included A _ _) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
200 201 202 203 204 205 206 207 208 209 210
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
  intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
  intros x1 x2 Hx P1 P2 HP; split=>Hup z n;
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
211 212 213 214 215 216 217 218 219

(** ** Validity *)
Lemma cmra_valid_validN x :  x   n, {n} x.
Proof. done. Qed.
Lemma cmra_validN_le x n n' : {n} x  n'  n  {n'} x.
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.
Lemma cmra_validN_op_r x y n : {n} (x  y)  {n} y.
220
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
221 222 223 224 225
Lemma cmra_valid_op_r x y :  (x  y)   y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.

(** ** Units *)
Lemma cmra_unit_r x : x  unit x  x.
226
Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
227
Lemma cmra_unit_unit x : unit x  unit x  unit x.
228
Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
229
Lemma cmra_unit_validN x n : {n} x  {n} unit x.
230
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
231
Lemma cmra_unit_valid x :  x   unit x.
232 233 234
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

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

Lemma cmra_includedN_S x y n : x {S n} y  x {n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Lemma cmra_includedN_le x y n n' : x {n} y  n'  n  x {n'} y.
Proof. induction 2; auto using cmra_includedN_S. Qed.

Lemma cmra_includedN_l n x y : x {n} x  y.
Proof. by exists y. Qed.
Lemma cmra_included_l x y : x  x  y.
Proof. by exists y. Qed.
Lemma cmra_includedN_r n x y : y {n} x  y.
268
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
269
Lemma cmra_included_r x y : y  x  y.
270
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271

272 273 274 275
Lemma cmra_unit_preserving x y : x  y  unit x  unit y.
Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
Lemma cmra_included_unit x : unit x  x.
Proof. by exists x; rewrite cmra_unit_l. Qed.
276
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
277
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
278
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
279
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
280
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
281
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
282
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
283
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
284 285

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

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

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

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

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

334 335 336
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.
337 338

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

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

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

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

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

396
(** * Properties about monotone functions *)
397
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
398
Proof. by split. Qed.
399 400
Instance cmra_monotone_compose {A B C : cmraT} (f : A  B) (g : B  C) :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
401 402
Proof.
  split.
403 404
  * move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
  * move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
Qed.
406

407 408 409 410 411 412
Section cmra_monotone.
  Context {A B : cmraT} (f : A  B) `{!CMRAMonotone f}.
  Lemma included_preserving x y : x  y  f x  f y.
  Proof.
    rewrite !cmra_included_includedN; eauto using includedN_preserving.
  Qed.
413
  Lemma valid_preserving x :  x   f x.
414 415 416
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

417

418 419 420 421 422 423 424 425 426 427 428 429 430 431 432
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
  eq_rect A id x _ H.

Section cmra_transport.
  Context {A B : cmraT} (H : A = B).
  Notation T := (cmra_transport H).
  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
  Proof. by intros ???; destruct H. Qed.
  Global Instance cmra_transport_proper : Proper (() ==> ()) T.
  Proof. by intros ???; destruct H. Qed.
  Lemma cmra_transport_op x y : T (x  y) = T x  T y.
  Proof. by destruct H. Qed.
  Lemma cmra_transport_unit x : T (unit x) = unit (T x).
  Proof. by destruct H. Qed.
433
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
434
  Proof. by destruct H. Qed.
435
  Lemma cmra_transport_valid x :  T x   x.
436 437 438 439 440 441 442 443 444 445 446
  Proof. by destruct H. Qed.
  Global Instance cmra_transport_timeless x : Timeless x  Timeless (T x).
  Proof. by destruct H. Qed.
  Lemma cmra_transport_updateP (P : A  Prop) (Q : B  Prop) x :
    x ~~>: P  ( y, P y  Q (T y))  T x ~~>: Q.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma cmra_transport_updateP' (P : A  Prop) x :
    x ~~>: P  T x ~~>: λ y,  y', y = cmra_transport H y'  P y'.
  Proof. eauto using cmra_transport_updateP. Qed.
End cmra_transport.

447 448 449 450 451 452
(** * Instances *)
(** ** Discrete CMRA *)
Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
  (* setoids *)
  ra_op_ne (x : A) : Proper (() ==> ()) (op x);
  ra_unit_ne :> Proper (() ==> ()) unit;
453
  ra_validN_ne :> Proper (() ==> impl) valid;
454 455
  ra_minus_ne :> Proper (() ==> () ==> ()) minus;
  (* monoid *)
456 457
  ra_assoc :> Assoc () ();
  ra_comm :> Comm () ();
458
  ra_unit_l x : unit x  x  x;
459
  ra_unit_idemp x : unit (unit x)  unit x;
460 461 462 463 464
  ra_unit_preserving x y : x  y  unit x  unit y;
  ra_valid_op_l x y :  (x  y)   x;
  ra_op_minus x y : x  y  x  y  x  y
}.

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

469
  Instance discrete_validN : ValidN A := λ n x,  x.
470
  Definition discrete_cmra_mixin : CMRAMixin A.
471
  Proof.
472 473
    by destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _ _ _).
474
  Qed.
475
  Definition discrete_extend_mixin : CMRAExtendMixin A.
476
  Proof.
477 478
    intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
    apply (timeless _), dist_le with n; auto with lia.
479
  Qed.
480
  Definition discreteRA : cmraT :=
481
    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
482
  Lemma discrete_updateP (x : discreteRA) (P : A  Prop) :
483
    ( z,  (x  z)   y, P y   (y  z))  x ~~>: P.
484
  Proof. intros Hvalid z n; apply Hvalid. Qed.
485
  Lemma discrete_update (x y : discreteRA) :
486
    ( z,  (x  z)   (y  z))  x ~~> y.
487
  Proof. intros Hvalid z n; apply Hvalid. Qed.
488 489
End discrete.

490 491 492 493 494 495 496 497 498 499 500 501 502 503
(** ** CMRA for the unit type *)
Section unit.
  Instance unit_valid : Valid () := λ x, True.
  Instance unit_unit : Unit () := λ x, x.
  Instance unit_op : Op () := λ x y, ().
  Instance unit_minus : Minus () := λ x y, ().
  Global Instance unit_empty : Empty () := ().
  Definition unit_ra : RA ().
  Proof. by split. Qed.
  Canonical Structure unitRA : cmraT :=
    Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
  Global Instance unit_cmra_identity : CMRAIdentity unitRA.
  Proof. by split; intros []. Qed.
End unit.
504

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