cmra.v 26.8 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Notation "x ≼{ n } y" := (includedN n x y)
28
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Instance: Params (@includedN) 4.
30
Hint Extern 0 (_ {_} _) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

Ralf Jung's avatar
Ralf Jung committed
113
(** * CMRAs with a unit element *)
114
(** We use the notation ∅ because for most instances (maps, sets, etc) the
Ralf Jung's avatar
Ralf Jung committed
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
}.
Ralf Jung's avatar
Ralf Jung committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 *.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Qed.
305
Lemma cmra_timeless_included_r n x y : Timeless y  x {0} y  x {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
307
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
308
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310
Proof.
  intros ??? z Hz.
311
  destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
312
  { rewrite -?Hz. by apply cmra_valid_validN. }
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
315

316 317 318 319 320 321 322 323
(** ** 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.

Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
341
  Lemma cmra_unit_least x :   x.
342
  Proof. by exists x; rewrite left_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348
  Lemma cmra_core_unit : core (:A)  .
  Proof. by rewrite -{2}(cmra_core_l ) right_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
349
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
350

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

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

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

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

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

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

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

420
(** * Properties about monotone functions *)
421
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Robbert Krebbers's avatar
Robbert Krebbers committed
422
Proof. repeat split; by try apply _. Qed.
423 424
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
425 426
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  - apply _. 
428
  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
429
  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
Qed.
431

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

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

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

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

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

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

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

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

583 584 585 586
  Lemma pair_split `{CMRAUnit A, CMRAUnit B} (x : A) (y : B) :
    (x, y)  (x, )  (, y).
  Proof. constructor; by rewrite /= ?left_id ?right_id. Qed.

587
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
588
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
589
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
590
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
591
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
592 593
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
594 595
    exists (a,b); repeat split; auto.
  Qed.
596
  Lemma prod_updateP' P1 P2 x :
597
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
598
  Proof. eauto using prod_updateP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
599 600 601 602 603 604 605 606 607 608

  Global Instance prod_local_update
      (LA : A  A) `{!LocalUpdate LvA LA} (LB : B  B) `{!LocalUpdate LvB LB} :
    LocalUpdate (λ x, LvA (x.1)  LvB (x.2)) (prod_map LA LB).
  Proof.
    constructor.
    - intros n x y [??]; constructor; simpl; by apply local_update_ne.
    - intros n ?? [??] [??];
        constructor; simpl in *; eapply local_updateN; eauto.
  Qed.
609
End prod.
Robbert Krebbers's avatar
Robbert Krebbers committed
610

611
Arguments prodR : clear implicits.
612 613 614

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).
615
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
  split; first apply _.
617
  - by intros n x [??]; split; simpl; apply validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
618 619
  - intros x y; rewrite !prod_included=> -[??] /=.
    by split; apply included_preserving.
620
Qed.
621 622 623 624 625 626

(** 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;
627 628
  rFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
629 630 631 632 633 634 635
  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) 
}.
636
Existing Instances rFunctor_ne rFunctor_mono.
637 638
Instance: Params (@rFunctor_map) 5.

639 640 641
Class rFunctorContractive (F : rFunctor) :=
  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).

642 643 644 645 646 647 648
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.

649
Instance constRF_contractive B : rFunctorContractive (constRF B).
650
Proof. rewrite /rFunctorContractive; apply _. Qed.
651

652 653 654 655 656
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)
|}.
657 658 659
Next Obligation.
  intros F1 F2 A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_ne.
Qed.
660 661 662 663 664
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.
665 666 667 668 669 670 671 672

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.