cmra.v 26.2 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
17 18
Class ValidN (A : Type) := validN : nat  A  Prop.
Instance: Params (@validN) 3.
19
Notation "✓{ n } x" := (validN n x)
20
  (at level 20, n at next level, format "✓{ n }  x").
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22 23
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
24
Notation "✓ x" := (valid x) (at level 20) : C_scope.
25

26
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y {n} x  z.
27
Notation "x ≼{ n } y" := (includedN n x y)
28
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
29
Instance: Params (@includedN) 4.
30
Hint Extern 0 (_ {_} _) => reflexivity.
31

Robbert Krebbers's avatar
Robbert Krebbers committed
32
Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  (* setoids *)
34
  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
Ralf Jung's avatar
Ralf Jung committed
35
  mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
36
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  (* valid *)
38
  mixin_cmra_valid_validN x :  x   n, {n} x;
39
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
40
  (* monoid *)
41 42
  mixin_cmra_assoc : Assoc () ();
  mixin_cmra_comm : Comm () ();
Ralf Jung's avatar
Ralf Jung committed
43 44 45
  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;
46
  mixin_cmra_validN_op_l n x y : {n} (x  y)  {n} x;
47 48 49
  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
50
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54 55 56 57
(** 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
58
  cmra_core : Core cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  cmra_op : Op cmra_car;
60
  cmra_valid : Valid cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  cmra_validN : ValidN cmra_car;
62
  cmra_cofe_mixin : CofeMixin cmra_car;
63
  cmra_mixin : CMRAMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
64
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
66 67 68 69
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
70
Arguments cmra_core : simpl never.
71
Arguments cmra_op : simpl never.
72
Arguments cmra_valid : simpl never.
73 74 75
Arguments cmra_validN : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Add Printing Constructor cmraT.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
78
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80
Canonical Structure cmra_cofeC.

81 82 83 84 85 86
(** 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
87 88
  Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
  Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed.
89 90
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
91 92
  Lemma cmra_valid_validN x :  x   n, {n} x.
  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
93 94
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
95 96 97 98
  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
99 100 101 102 103 104
  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.
105 106
  Lemma cmra_validN_op_l n x y : {n} (x  y)  {n} x.
  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
107
  Lemma cmra_extend n x y1 y2 :
108 109
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }.
110
  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
111 112
End cmra_mixin.

113
(** * CMRAs with a unit element *)
114
(** We use the notation ∅ because for most instances (maps, sets, etc) the
115 116 117 118 119
`empty' element is the unit. *)
Class CMRAUnit (A : cmraT) `{Empty A} := {
  cmra_unit_valid :  ;
  cmra_unit_left_id :> LeftId ()  ();
  cmra_unit_timeless :> Timeless 
120
}.
121
Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate .
122

123 124 125 126
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : core x  x.
Arguments persistent {_} _ {_}.

127
(** * Discrete CMRAs *)
128
Class CMRADiscrete (A : cmraT) := {
129 130 131 132
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
133
(** * Morphisms *)
134
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137
  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
138
}.
139 140
Arguments validN_preserving {_ _} _ {_} _ _ _.
Arguments included_preserving {_ _} _ {_} _ _ _.
141

142
(** * Local updates *)
Ralf Jung's avatar
Ralf Jung committed
143 144
(** 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. *)
145 146 147
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
148 149 150
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
161
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Section cmra.
163
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Implicit Types x y z : A.
165
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
166

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

(** ** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
218
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
219 220 221
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
222
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
223
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
224 225 226
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
227 228 229 230 231 232 233 234 235
(** ** 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.
236 237
Global Instance cmra_core_persistent x : Persistent (core x).
Proof. apply cmra_core_idemp. Qed.
238 239

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241
Lemma cmra_included_includedN n x y : x  y  x {n} y.
Proof. intros [z ->]. by exists z. Qed.
242 243 244
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
245
  - by intros x; exists (core x); rewrite cmra_core_r.
246
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
247
    by rewrite assoc -Hy -Hz.
248 249 250
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
251 252 253 254
  split.
  - by intros x; exists (core x); rewrite cmra_core_r.
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
    by rewrite assoc -Hy -Hz.
255
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
257
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
260

Robbert Krebbers's avatar
Robbert Krebbers committed
261
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
262
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
264 265 266 267 268 269 270
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.
271
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
272
Lemma cmra_included_r x y : y  x  y.
273
Proof. rewrite (comm op); apply cmra_included_l. Qed.
274

Ralf Jung's avatar
Ralf Jung committed
275
Lemma cmra_core_preservingN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277
Proof.
  intros [z ->].
Ralf Jung's avatar
Ralf Jung committed
278
  apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
Qed.
Ralf Jung's avatar
Ralf Jung committed
280 281
Lemma cmra_included_core x : core x  x.
Proof. by exists x; rewrite cmra_core_l. Qed.
282
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
283
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
284
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
285
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
286
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
287
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
288
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
289
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
290

Robbert Krebbers's avatar
Robbert Krebbers committed
291
Lemma cmra_included_dist_l n x1 x2 x1' :
292
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
Proof.
294 295
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Qed.
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 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
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 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
312
  { rewrite -?Hz. by apply cmra_valid_validN. }
313
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Qed.
315

316 317 318 319 320 321 322 323
(** ** 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
  split; first by apply cmra_included_includedN.
325 326 327 328 329 330 331 332 333
  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.

334 335 336 337 338 339
(** ** 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.
340
  Proof. by exists x; rewrite left_id. Qed.
341
  Lemma cmra_unit_least x :   x.
342
  Proof. by exists x; rewrite left_id. Qed.
343
  Global Instance cmra_unit_right_id : RightId ()  ().
344
  Proof. by intros x; rewrite (comm op) left_id. Qed.
345 346
  Global Instance cmra_unit_persistent : Persistent .
  Proof. by rewrite /Persistent -{2}(cmra_core_l ) right_id. Qed.
347
End unit.
348

349
(** ** Local updates *)
350 351
Global Instance local_update_proper Lv (L : A  A) :
  LocalUpdate Lv L  Proper (() ==> ()) L.
352 353
Proof. intros; apply (ne_proper _). Qed.

354 355
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
356 357 358
Proof.
  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
Qed.
359 360

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

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

366
(** ** Updates *)
367
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
368
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
369
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =).
Robbert Krebbers's avatar
Robbert Krebbers committed
370 371
Proof.
  split.
372
  - by intros Hx z ?; exists y; split; [done|apply (Hx z)].
Robbert Krebbers's avatar
Robbert Krebbers committed
373
  - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
374
Qed.
375
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Proof. by intros ? n z ?; exists x. Qed.
377
Lemma cmra_updateP_compose (P Q : A  Prop) x :
378
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
379
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
380
  intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y).
381
Qed.
382 383 384 385 386
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.
387
Lemma cmra_updateP_weaken (P Q : A  Prop) x : x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
388
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
389

390
Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
391
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2))  x1  x2 ~~>: Q.
392
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394 395
  intros Hx1 Hx2 Hy n z ?.
  destruct (Hx1 n (x2  z)) as (y1&?&?); first by rewrite assoc.
  destruct (Hx2 n (y1  z)) as (y2&?&?);
396 397
    first by rewrite assoc (comm _ x2) -assoc.
  exists (y1  y2); split; last rewrite (comm _ y1) -assoc; auto.
398
Qed.
399
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
400
  x1 ~~>: P1  x2 ~~>: P2  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
401
Proof. eauto 10 using cmra_updateP_op. Qed.
402
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
403
Proof.
404
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
405
Qed.
406 407
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
408

409 410 411
Section unit_updates.
  Context `{Empty A, !CMRAUnit A}.
  Lemma cmra_update_unit x : x ~~> .
Robbert Krebbers's avatar
Robbert Krebbers committed
412
  Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
413 414 415
  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
416 417
End cmra.

418
(** * Properties about monotone functions *)
419
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Robbert Krebbers's avatar
Robbert Krebbers committed
420
Proof. repeat split; by try apply _. Qed.
421 422
Instance cmra_monotone_compose {A B C : cmraT} (f : A  B) (g : B  C) :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (g  f).
423 424
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
  - apply _. 
426
  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
428
Qed.
429

430 431
Section cmra_monotone.
  Context {A B : cmraT} (f : A  B) `{!CMRAMonotone f}.
Robbert Krebbers's avatar
Robbert Krebbers committed
432 433
  Global Instance cmra_monotone_proper : Proper (() ==> ()) f := ne_proper _.
  Lemma includedN_preserving n x y : x {n} y  f x {n} f y.
434
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
435
    intros [z ->].
436
    apply cmra_included_includedN, (included_preserving f), cmra_included_l.
437
  Qed.
438
  Lemma valid_preserving x :  x   f x.
439 440 441
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

442 443 444 445 446 447 448 449 450 451 452 453 454
(** * 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
455
  Lemma cmra_transport_core x : T (core x) = core (T x).
456
  Proof. by destruct H. Qed.
457
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
458
  Proof. by destruct H. Qed.
459
  Lemma cmra_transport_valid x :  T x   x.
460 461 462
  Proof. by destruct H. Qed.
  Global Instance cmra_transport_timeless x : Timeless x  Timeless (T x).
  Proof. by destruct H. Qed.
463 464
  Global Instance cmra_transport_persistent x : Persistent x  Persistent (T x).
  Proof. by destruct H. Qed.
465 466 467 468 469 470 471 472
  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.

473 474
(** * Instances *)
(** ** Discrete CMRA *)
Robbert Krebbers's avatar
Robbert Krebbers committed
475
Class RA A `{Equiv A, Core A, Op A, Valid A} := {
476 477
  (* setoids *)
  ra_op_ne (x : A) : Proper (() ==> ()) (op x);
Ralf Jung's avatar
Ralf Jung committed
478
  ra_core_ne :> Proper (() ==> ()) core;
479
  ra_validN_ne :> Proper (() ==> impl) valid;
480
  (* monoid *)
481 482
  ra_assoc :> Assoc () ();
  ra_comm :> Comm () ();
Ralf Jung's avatar
Ralf Jung committed
483 484 485
  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;
Robbert Krebbers's avatar
Robbert Krebbers committed
486
  ra_valid_op_l x y :  (x  y)   x
487 488
}.

489
Section discrete.
490
  Context {A : cofeT} `{Discrete A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
491
  Context `{Core A, Op A, Valid A} (ra : RA A).
492

493
  Instance discrete_validN : ValidN A := λ n x,  x.
494
  Definition discrete_cmra_mixin : CMRAMixin A.
495
  Proof.
496 497
    destruct ra; split; unfold Proper, respectful, includedN;
      try setoid_rewrite <-(timeless_iff _ _); try done.
498 499 500
    - 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.
501
  Qed.
502 503
  Definition discreteR : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
  Global Instance discrete_cmra_discrete : CMRADiscrete discreteR.
504
  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
505 506
End discrete.

507 508 509
(** ** CMRA for the unit type *)
Section unit.
  Instance unit_valid : Valid () := λ x, True.
Ralf Jung's avatar
Ralf Jung committed
510
  Instance unit_core : Core () := λ x, x.
511 512 513 514
  Instance unit_op : Op () := λ x y, ().
  Global Instance unit_empty : Empty () := ().
  Definition unit_ra : RA ().
  Proof. by split. Qed.
515 516
  Canonical Structure unitR : cmraT :=
    Eval cbv [unitC discreteR cofe_car] in discreteR unit_ra.
517
  Global Instance unit_cmra_unit : CMRAUnit unitR.
518
  Global Instance unit_cmra_discrete : CMRADiscrete unitR.
519
  Proof. by apply discrete_cmra_discrete. Qed.
520 521
  Global Instance unit_persistent (x : ()) : Persistent x.
  Proof. done. Qed.
522
End unit.
523

524
(** ** Product *)
525 526 527 528
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
529
  Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
530
  Instance prod_valid : Valid (A * B) := λ x,  x.1   x.2.
531
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
532 533 534 535 536 537 538 539 540 541 542 543 544
  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 _.
545 546 547
    - 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.
548 549 550
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
551 552 553
    - by intros n x [??]; split; apply cmra_validN_S.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
Ralf Jung's avatar
Ralf Jung committed
554 555
    - by split; rewrite /= cmra_core_l.
    - by split; rewrite /= cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
    - intros x y; rewrite !prod_included.
Ralf Jung's avatar
Ralf Jung committed
557
      by intros [??]; split; apply cmra_core_preserving.
558
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
559 560 561 562
    - 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)).
563
  Qed.
564
  Canonical Structure prodR : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
565 566
  Global Instance prod_cmra_unit `{Empty A, Empty B} :
    CMRAUnit A  CMRAUnit B  CMRAUnit prodR.
567 568
  Proof.
    split.
569
    - split; apply cmra_unit_valid.
570 571
    - by split; rewrite /=left_id.
    - by intros ? [??]; split; apply (timeless _).
572
  Qed.
573
  Global Instance prod_cmra_discrete :
574
    CMRADiscrete A  CMRADiscrete B  CMRADiscrete prodR.
575 576
  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.

577 578 579 580
  Global Instance pair_persistent x y :
    Persistent x  Persistent y  Persistent (x,y).
  Proof. by split. Qed.

581
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
582
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
583
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
584
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
585
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
586 587
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
588 589
    exists (a,b); repeat split; auto.
  Qed.
590
  Lemma prod_updateP' P1 P2 x :
591
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
592
  Proof. eauto using prod_updateP. Qed.
593
End prod.
594
Arguments prodR : clear implicits.
595 596 597

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).
598
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
  split; first apply _.
600
  - by intros n x [??]; split; simpl; apply validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
601 602
  - intros x y; rewrite !prod_included=> -[??] /=.
    by split; apply included_preserving.
603
Qed.
604 605 606 607 608 609

(** 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;
610 611
  rFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
612 613 614 615 616 617 618
  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) 
}.
619
Existing Instances rFunctor_ne rFunctor_mono.
620 621
Instance: Params (@rFunctor_map) 5.

622 623 624
Class rFunctorContractive (F : rFunctor) :=
  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).

625 626 627 628 629 630 631
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.

632
Instance constRF_contractive B : rFunctorContractive (constRF B).
633
Proof. rewrite /rFunctorContractive; apply _. Qed.
634

635 636 637 638 639
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)
|}.
640 641 642
Next Obligation.
  intros F1 F2 A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_ne.
Qed.
643 644 645 646 647
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.
648 649 650 651 652 653 654 655

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.