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

127
(** * CMRAs with a unit element *)
128
(** We use the notation ∅ because for most instances (maps, sets, etc) the
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
}.
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 *)
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'.
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.
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 *.
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. }
329
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Qed.
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.

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.
357
  Lemma cmra_unit_least x :   x.
358
  Proof. by exists x; rewrite left_id. Qed.
359
  Global Instance cmra_unit_right_id : RightId ()  ().
360
  Proof. by intros x; rewrite (comm op) left_id. Qed.
361
  Lemma cmra_core_unit : core   .
Ralf Jung's avatar
Ralf Jung committed
362
  Proof. by rewrite -{2}(cmra_core_l ) right_id. Qed.
363
End unit.
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

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.
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).
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.
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.
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.
585 586
  Global Instance prod_cmra_unit `{Empty A, Empty B} :
    CMRAUnit A  CMRAUnit B  CMRAUnit prodR.
587 588
  Proof.
    split.
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.