cmra.v 23.6 KB
Newer Older
1
Require Export algebra.cofe.
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19

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.
Hint Extern 0 (?x  ?y) => reflexivity.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
Robbert Krebbers's avatar
Robbert Krebbers committed
24

25 26
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
Ralf Jung's avatar
Ralf Jung committed
27
Notation "✓" := valid (at level 1) : C_scope.
28 29
Instance validN_valid `{ValidN A} : Valid A := λ x,  n, {n} x.

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 32 33
Notation "x ≼{ n } y" := (includedN n x y)
  (at level 70, format "x  ≼{ n }  y") : C_scope.
Instance: Params (@includedN) 4.
34
Hint Extern 0 (?x {_} ?y) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
35

36
Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  (* setoids *)
38 39
  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;
40
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) ({n});
41
  mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  (* valid *)
43
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  (* monoid *)
45 46 47 48
  mixin_cmra_associative : Associative () ();
  mixin_cmra_commutative : Commutative () ();
  mixin_cmra_unit_l x : unit x  x  x;
  mixin_cmra_unit_idempotent x : unit (unit x)  unit x;
49 50
  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;
51
  mixin_cmra_op_minus n x y : x {n} y  x  y  x {n} y
Robbert Krebbers's avatar
Robbert Krebbers committed
52
}.
53
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} :=  n x y1 y2,
54 55
  {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
56

Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 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;
  cmra_validN : ValidN cmra_car;
  cmra_minus : Minus cmra_car;
67 68 69
  cmra_cofe_mixin : CofeMixin cmra_car;
  cmra_mixin : CMRAMixin cmra_car;
  cmra_extend_mixin : CMRAExtendMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
70
}.
71
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _.
72 73 74 75 76 77 78 79 80 81 82
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
83
Add Printing Constructor cmraT.
84
Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
85
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87
Canonical Structure cmra_cofeC.

88 89 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.
  Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _).
  Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
96 97
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
98 99 100
  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.
101 102 103 104 105 106 107 108 109 110 111 112 113 114
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
  Global Instance cmra_associative : Associative () (@op A _).
  Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed.
  Global Instance cmra_commutative : Commutative () (@op A _).
  Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_l x : unit x  x  x.
  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_idempotent x : unit (unit x)  unit x.
  Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed.
  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.
115
  Lemma cmra_op_minus n x y : x {n} y  x  y  x {n} y.
116 117
  Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
  Lemma cmra_extend_op n x y1 y2 :
118 119
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }.
120 121 122
  Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.

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

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

139
(** * Local updates *)
140 141 142
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
143 144 145
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

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

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

162 163 164 165 166 167 168 169 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
(** ** 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.
  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
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.
199 200 201 202 203 204 205 206 207 208 209
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.
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233

(** ** 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.
Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed.
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.
Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
Lemma cmra_unit_unit x : unit x  unit x  unit x.
Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed.
Lemma cmra_unit_validN x n : {n} x  {n} (unit x).
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_unit_valid x :  x   (unit x).
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235 236 237 238 239
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.
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
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).
    by rewrite (associative _) -Hy -Hz.
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.
Proof. rewrite (commutative op); apply cmra_includedN_l. Qed.
Lemma cmra_included_r x y : y  x  y.
Proof. rewrite (commutative op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
270

271 272 273 274
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.
275 276
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
277 278
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
279 280
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
Proof. by intros; rewrite -!(commutative _ z); apply cmra_preservingN_l. Qed.
281 282 283 284
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.

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

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

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

315 316 317 318 319 320 321 322 323 324 325 326
(** ** 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 ()  ().
  Proof. by intros x; rewrite (commutative op) left_id. Qed.
  Lemma cmra_unit_empty : unit   .
  Proof. by rewrite -{2}(cmra_unit_l ) right_id. Qed.
End identity.
Robbert Krebbers's avatar
Robbert Krebbers committed
327

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

333 334 335
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.
336 337 338 339

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

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

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

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
388 389
End cmra.

390
(** * Properties about monotone functions *)
391
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
392
Proof. by split. Qed.
393 394
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
395 396
Proof.
  split.
397 398
  * 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
399
Qed.
400

401 402 403 404 405 406 407 408 409 410
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.
  Lemma valid_preserving x :  x   (f x).
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

411

412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440
(** * 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.
  Lemma cmra_transport_validN n x : {n} (T x)  {n} x.
  Proof. by destruct H. Qed.
  Lemma cmra_transport_valid x :  (T x)   x.
  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.

441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458
(** * 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;
  ra_validN_ne :> Proper (() ==> impl) ;
  ra_minus_ne :> Proper (() ==> () ==> ()) minus;
  (* monoid *)
  ra_associative :> Associative () ();
  ra_commutative :> Commutative () ();
  ra_unit_l x : unit x  x  x;
  ra_unit_idempotent x : unit (unit x)  unit x;
  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
}.

459
Section discrete.
460 461 462
  Context {A : cofeT} `{ x : A, Timeless x}.
  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).

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

484 485 486 487 488 489 490 491 492 493 494 495 496 497
(** ** 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.
498

499
(** ** Product *)
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524
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)).
  Instance prod_validN : ValidN (A * B) := λ n x, {n} (x.1)  {n} (x.2).
  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.
525
    * by intros n x [??]; split; apply cmra_validN_S.
526 527
    * split; simpl; apply (associative _).
    * split; simpl; apply (commutative _).
528 529
    * split; simpl; apply cmra_unit_l.
    * split; simpl; apply cmra_unit_idempotent.
530
    * intros n x y; rewrite !prod_includedN.
531 532
      by intros [??]; split; apply cmra_unit_preservingN.
    * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
533 534 535 536 537 538 539 540 541 542 543 544
    * 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.
545 546 547 548 549 550 551 552
  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.
553
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
554
  Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
555
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
556
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
557 558 559 560 561
  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.
562
  Lemma prod_updateP' P1 P2 x :
563
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
564
  Proof. eauto using prod_updateP. Qed.
565 566 567 568 569
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).
570 571
Proof.
  split.
572
  * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
    by split; apply includedN_preserving.
574 575
  * by intros n x [??]; split; simpl; apply validN_preserving.
Qed.