cmra.v 36.5 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
}.
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 A (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
`empty' element is the unit. *)
116 117 118 119
Record UCMRAMixin A `{Dist A, Equiv A, Op A, Valid A, Empty A} := {
  mixin_ucmra_unit_valid :  ;
  mixin_ucmra_unit_left_id : LeftId ()  ();
  mixin_ucmra_unit_timeless : Timeless 
120
}.
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166

Structure ucmraT := UCMRAT {
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
  ucmra_compl : Compl ucmra_car;
  ucmra_core : Core ucmra_car;
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_empty : Empty ucmra_car;
  ucmra_cofe_mixin : CofeMixin ucmra_car;
  ucmra_cmra_mixin : CMRAMixin ucmra_car;
  ucmra_mixin : UCMRAMixin ucmra_car
}.
Arguments UCMRAT _ {_ _ _ _ _ _ _ _} _ _ _.
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Arguments ucmra_compl : simpl never.
Arguments ucmra_core : simpl never.
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
Arguments ucmra_cofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Existing Instances ucmra_empty.
Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
Canonical Structure ucmra_cofeC.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
  CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.

(** Lifting properties from the mixin *)
Section ucmra_mixin.
  Context {A : ucmraT}.
  Implicit Types x y : A.
  Lemma ucmra_unit_valid :  ( : A).
  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
  Global Instance ucmra_unit_left_id : LeftId ()  (@op A _).
  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
  Global Instance ucmra_unit_timeless : Timeless ( : A).
  Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
167

168 169 170 171
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : core x  x.
Arguments persistent {_} _ {_}.

172
(** * Discrete CMRAs *)
173
Class CMRADiscrete (A : cmraT) := {
174 175 176 177
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
178
(** * Morphisms *)
179
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182
  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
183
}.
184 185
Arguments validN_preserving {_ _} _ {_} _ _ _.
Arguments included_preserving {_ _} _ {_} _ _ _.
186

187
(** * Local updates *)
Ralf Jung's avatar
Ralf Jung committed
188 189
(** 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. *)
190 191 192
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
193 194 195
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

196
(** * Frame preserving updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  n z,
198
  {n} (x  z)   y, P y  {n} (y  z).
199
Instance: Params (@cmra_updateP) 1.
200
Infix "~~>:" := cmra_updateP (at level 70).
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Definition cmra_update {A : cmraT} (x y : A) :=  n z,
202
  {n} (x  z)  {n} (y  z).
203
Infix "~~>" := cmra_update (at level 70).
204
Instance: Params (@cmra_update) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
205

Robbert Krebbers's avatar
Robbert Krebbers committed
206
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Section cmra.
208
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Implicit Types x y z : A.
210
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
211

212
(** ** Setoids *)
Ralf Jung's avatar
Ralf Jung committed
213
Global Instance cmra_core_proper : Proper (() ==> ()) (@core A _).
214 215 216 217
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.
218
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
219 220 221 222 223 224 225 226 227
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 _).
228 229 230 231
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
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.
250 251 252
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
254 255 256 257
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
259 260
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
261 262

(** ** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
264 265 266
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
267
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
268
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
269 270 271
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
272 273 274 275 276 277 278 279 280
(** ** 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.
281 282
Global Instance cmra_core_persistent x : Persistent (core x).
Proof. apply cmra_core_idemp. Qed.
283 284

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
Lemma cmra_included_includedN n x y : x  y  x {n} y.
Proof. intros [z ->]. by exists z. Qed.
287 288 289
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
290
  - by intros x; exists (core x); rewrite cmra_core_r.
291
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
292
    by rewrite assoc -Hy -Hz.
293 294 295
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
296 297 298 299
  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.
300
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
302
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
305

Robbert Krebbers's avatar
Robbert Krebbers committed
306
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
307
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
309 310 311 312 313 314 315
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.
316
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
317
Lemma cmra_included_r x y : y  x  y.
318
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
319

Ralf Jung's avatar
Ralf Jung committed
320
Lemma cmra_core_preservingN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322
Proof.
  intros [z ->].
Ralf Jung's avatar
Ralf Jung committed
323
  apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Qed.
Ralf Jung's avatar
Ralf Jung committed
325 326
Lemma cmra_included_core x : core x  x.
Proof. by exists x; rewrite cmra_core_l. Qed.
327
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
328
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
329
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
330
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
331
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
332
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
333
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
334
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
335

Robbert Krebbers's avatar
Robbert Krebbers committed
336
Lemma cmra_included_dist_l n x1 x2 x1' :
337
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Proof.
339 340
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Qed.
342

Robbert Krebbers's avatar
Robbert Krebbers committed
343
(** ** Timeless *)
344
Lemma cmra_timeless_included_l x y : Timeless x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
345 346
Proof.
  intros ?? [x' ?].
347
  destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Qed.
350
Lemma cmra_timeless_included_r n x y : Timeless y  x {0} y  x {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
352
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
353
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
354 355
Proof.
  intros ??? z Hz.
356
  destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
357
  { rewrite -?Hz. by apply cmra_valid_validN. }
Robbert Krebbers's avatar
Robbert Krebbers committed
358
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
359
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
360

361 362 363 364 365 366 367 368
(** ** 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
369
  split; first by apply cmra_included_includedN.
370 371 372 373 374 375 376 377 378
  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.

379
(** ** Local updates *)
380 381
Global Instance local_update_proper Lv (L : A  A) :
  LocalUpdate Lv L  Proper (() ==> ()) L.
382 383
Proof. intros; apply (ne_proper _). Qed.

384 385
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
386 387 388
Proof.
  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
Qed.
389 390

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

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

396
(** ** Updates *)
397
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
398
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
399
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =).
Robbert Krebbers's avatar
Robbert Krebbers committed
400 401
Proof.
  split.
402
  - by intros Hx z ?; exists y; split; [done|apply (Hx z)].
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Qed.
405
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
Proof. by intros ? n z ?; exists x. Qed.
407
Lemma cmra_updateP_compose (P Q : A  Prop) x :
408
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
409
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y).
411
Qed.
412 413 414 415 416
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.
417
Lemma cmra_updateP_weaken (P Q : A  Prop) x : x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
418
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
419

420
Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
421
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2))  x1  x2 ~~>: Q.
422
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
423 424 425
  intros Hx1 Hx2 Hy n z ?.
  destruct (Hx1 n (x2  z)) as (y1&?&?); first by rewrite assoc.
  destruct (Hx2 n (y1  z)) as (y2&?&?);
426 427
    first by rewrite assoc (comm _ x2) -assoc.
  exists (y1  y2); split; last rewrite (comm _ y1) -assoc; auto.
428
Qed.
429
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
430
  x1 ~~>: P1  x2 ~~>: P2  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
431
Proof. eauto 10 using cmra_updateP_op. Qed.
432
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
433
Proof.
434
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
435
Qed.
436 437
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
438 439
End cmra.

440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Context {A : ucmraT}.
Implicit Types x y z : A.

Global Instance ucmra_unit_inhabited : Inhabited A := populate .

Lemma ucmra_unit_validN n : {n} (:A).
Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Lemma ucmra_unit_leastN n x :  {n} x.
Proof. by exists x; rewrite left_id. Qed.
Lemma ucmra_unit_least x :   x.
Proof. by exists x; rewrite left_id. Qed.
Global Instance ucmra_unit_right_id : RightId ()  (@op A _).
Proof. by intros x; rewrite (comm op) left_id. Qed.
Global Instance ucmra_unit_persistent : Persistent (:A).
Proof. by rewrite /Persistent -{2}(cmra_core_l ) right_id. Qed.
Lemma ucmra_core_unit : core (:A)  .
Proof. by rewrite -{2}(cmra_core_l ) right_id. Qed.

Lemma ucmra_update_unit x : x ~~> .
Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
Lemma ucmra_update_unit_alt y :  ~~> y   x, x ~~> y.
Proof. split; [intros; trans |]; auto using ucmra_update_unit. Qed.
End ucmra.

466
(** * Properties about monotone functions *)
467
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Proof. repeat split; by try apply _. Qed.
469 470
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
471 472
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
  - apply _. 
474
  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
Qed.
477

478 479
Section cmra_monotone.
  Context {A B : cmraT} (f : A  B) `{!CMRAMonotone f}.
Robbert Krebbers's avatar
Robbert Krebbers committed
480 481
  Global Instance cmra_monotone_proper : Proper (() ==> ()) f := ne_proper _.
  Lemma includedN_preserving n x y : x {n} y  f x {n} f y.
482
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
    intros [z ->].
484
    apply cmra_included_includedN, (included_preserving f), cmra_included_l.
485
  Qed.
486
  Lemma valid_preserving x :  x   f x.
487 488 489
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

490 491
(** Functors *)
Structure rFunctor := RFunctor {
492
  rFunctor_car : cofeT  cofeT  cmraT;
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519
  rFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
  rFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
  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) 
}.
Existing Instances rFunctor_ne rFunctor_mono.
Instance: Params (@rFunctor_map) 5.

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

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.

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

520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548
Structure urFunctor := URFunctor {
  urFunctor_car : cofeT  cofeT  ucmraT;
  urFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
  urFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2);
  urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x  x;
  urFunctor_compose {A1 A2 A3 B1 B2 B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    urFunctor_map (fg, g'f') x  urFunctor_map (g,g') (urFunctor_map (f,f') x);
  urFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CMRAMonotone (urFunctor_map fg) 
}.
Existing Instances urFunctor_ne urFunctor_mono.
Instance: Params (@urFunctor_map) 5.

Class urFunctorContractive (F : urFunctor) :=
  urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).

Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A.
Coercion urFunctor_diag : urFunctor >-> Funclass.

Program Definition constURF (B : ucmraT) : urFunctor :=
  {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.

Instance constURF_contractive B : urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.

549 550 551 552 553 554 555 556 557 558 559 560 561
(** * 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
562
  Lemma cmra_transport_core x : T (core x) = core (T x).
563
  Proof. by destruct H. Qed.
564
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
565
  Proof. by destruct H. Qed.
566
  Lemma cmra_transport_valid x :  T x   x.
567 568 569
  Proof. by destruct H. Qed.
  Global Instance cmra_transport_timeless x : Timeless x  Timeless (T x).
  Proof. by destruct H. Qed.
570 571
  Global Instance cmra_transport_persistent x : Persistent x  Persistent (T x).
  Proof. by destruct H. Qed.
572 573 574 575 576 577 578 579
  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.

580 581
(** * Instances *)
(** ** Discrete CMRA *)
582
Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := {
583 584
  (* setoids *)
  ra_op_ne (x : A) : Proper (() ==> ()) (op x);
585 586
  ra_core_ne : Proper (() ==> ()) core;
  ra_validN_ne : Proper (() ==> impl) valid;
587
  (* monoid *)
588 589
  ra_assoc : Assoc () ();
  ra_comm : Comm () ();
Ralf Jung's avatar
Ralf Jung committed
590 591 592
  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
593
  ra_valid_op_l x y :  (x  y)   x
594 595
}.

596
Section discrete.
597 598 599
  Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A ()}.
  Context (ra_mix : RAMixin A).
  Existing Instances discrete_dist discrete_compl.
600

601
  Instance discrete_validN : ValidN A := λ n x,  x.
602
  Definition discrete_cmra_mixin : CMRAMixin A.
603
  Proof.
604
    destruct ra_mix; split; try done.
605
    - intros x; split; first done. by move=> /(_ 0).
606
    - intros n x y1 y2 ??; by exists (y1,y2).
607 608 609
  Qed.
End discrete.

610 611 612 613 614 615 616 617 618
Notation discreteR A ra_mix :=
  (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
Notation discreteLeibnizR A ra_mix :=
  (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).

Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A,
  @Equivalence A ()} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
Proof. split. apply _. done. Qed.

619 620 621
(** ** CMRA for the unit type *)
Section unit.
  Instance unit_valid : Valid () := λ x, True.
622
  Instance unit_validN : ValidN () := λ n x, True.
Ralf Jung's avatar
Ralf Jung committed
623
  Instance unit_core : Core () := λ x, x.
624
  Instance unit_op : Op () := λ x y, ().
625 626

  Lemma unit_cmra_mixin : CMRAMixin ().
627 628
  Proof. by split; last exists ((),()). Qed.
  Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
629 630 631 632 633 634 635

  Instance unit_empty : Empty () := ().
  Lemma unit_ucmra_mixin : UCMRAMixin ().
  Proof. done. Qed.
  Canonical Structure unitUR : ucmraT :=
    UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin.

636
  Global Instance unit_cmra_discrete : CMRADiscrete unitR.
637
  Proof. done. Qed.
638 639
  Global Instance unit_persistent (x : ()) : Persistent x.
  Proof. done. Qed.
640
End unit.
641

642
(** ** Product *)
643 644 645
Section prod.
  Context {A B : cmraT}.
  Instance prod_op : Op (A * B) := λ x y, (x.1  y.1, x.2  y.2).
Ralf Jung's avatar
Ralf Jung committed
646
  Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
647
  Instance prod_valid : Valid (A * B) := λ x,  x.1   x.2.
648
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
649

650 651 652 653 654 655 656 657 658 659
  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.
660

661 662 663
  Definition prod_cmra_mixin : CMRAMixin (A * B).
  Proof.
    split; try apply _.
664 665 666
    - 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.
667 668 669
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
670 671 672
    - by intros n x [??]; split; apply cmra_validN_S.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
Ralf Jung's avatar
Ralf Jung committed
673 674
    - by split; rewrite /= cmra_core_l.
    - by split; rewrite /= cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
675
    - intros x y; rewrite !prod_included.
Ralf Jung's avatar
Ralf Jung committed
676
      by intros [??]; split; apply cmra_core_preserving.
677
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
678 679 680 681
    - 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)).
682
  Qed.
683
  Canonical Structure prodR :=
684
    CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
685

686
  Global Instance prod_cmra_discrete :
687
    CMRADiscrete A  CMRADiscrete B  CMRADiscrete prodR.
688 689
  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.

690 691 692 693
  Global Instance pair_persistent x y :
    Persistent x  Persistent y  Persistent (x,y).
  Proof. by split. Qed.

694
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
695
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
696
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
697
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
698
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
699 700
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
701 702
    exists (a,b); repeat split; auto.
  Qed.
703
  Lemma prod_updateP' P1 P2 x :
704
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
705
  Proof. eauto using prod_updateP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
706 707 708 709 710 711 712 713 714 715

  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.
716
End prod.
Robbert Krebbers's avatar
Robbert Krebbers committed
717

718
Arguments prodR : clear implicits.
719

720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
Section prod_unit.
  Context {A B : ucmraT}.

  Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (, ).
  Lemma prod_ucmra_mixin : UCMRAMixin (A * B).
  Proof.
    split.
    - split; apply ucmra_unit_valid.
    - by split; rewrite /=left_id.
    - by intros ? [??]; split; apply (timeless _).
  Qed.
  Canonical Structure prodUR :=
    UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.

  Lemma pair_split (x : A) (y : B) : (x, y)  (x, )  (, y).
  Proof. constructor; by rewrite /= ?left_id ?right_id. Qed.
End prod_unit.

Arguments prodUR : clear implicits.

740 741
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).
742
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
743
  split; first apply _.
744
  - by intros n x [??]; split; simpl; apply validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
745 746
  - intros x y; rewrite !prod_included=> -[??] /=.
    by split; apply included_preserving.
747
Qed.
748