cmra.v 59.6 KB
Newer Older
1
From iris.algebra Require Export ofe monoid.
2
Set Default Proof Using "Type".
3

Robbert Krebbers's avatar
Robbert Krebbers committed
4
Class PCore (A : Type) := pcore : A  option A.
5
Hint Mode PCore ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Instance: Params (@pcore) 2.
7
8

Class Op (A : Type) := op : A  A  A.
9
Hint Mode Op ! : typeclass_instances.
10
11
12
13
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

14
15
16
17
18
(* The inclusion quantifies over [A], not [option A].  This means we do not get
   reflexivity.  However, if we used [option A], the following would no longer
   hold:
     x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
*)
19
20
21
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.
22
Hint Extern 0 (_  _) => reflexivity.
23
24
Instance: Params (@included) 3.

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Class ValidN (A : Type) := validN : nat  A  Prop.
26
Hint Mode ValidN ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Instance: Params (@validN) 3.
28
Notation "✓{ n } x" := (validN n x)
29
  (at level 20, n at next level, format "✓{ n }  x").
Robbert Krebbers's avatar
Robbert Krebbers committed
30

31
Class Valid (A : Type) := valid : A  Prop.
32
Hint Mode Valid ! : typeclass_instances.
33
Instance: Params (@valid) 2.
34
Notation "✓ x" := (valid x) (at level 20) : C_scope.
35

36
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y {n} x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Notation "x ≼{ n } y" := (includedN n x y)
38
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
Instance: Params (@includedN) 4.
40
Hint Extern 0 (_ {_} _) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

Robbert Krebbers's avatar
Robbert Krebbers committed
42
Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  (* setoids *)
44
  mixin_cmra_op_ne (x : A) : NonExpansive (op x);
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
  mixin_cmra_pcore_ne n x y cx :
    x {n} y  pcore x = Some cx   cy, pcore y = Some cy  cx {n} cy;
47
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
Robbert Krebbers's avatar
Robbert Krebbers committed
48
  (* valid *)
49
  mixin_cmra_valid_validN x :  x   n, {n} x;
50
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  (* monoid *)
52
53
  mixin_cmra_assoc : Assoc () ();
  mixin_cmra_comm : Comm () ();
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
  mixin_cmra_pcore_l x cx : pcore x = Some cx  cx  x  x;
  mixin_cmra_pcore_idemp x cx : pcore x = Some cx  pcore cx  Some cx;
56
  mixin_cmra_pcore_mono x y cx :
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    x  y  pcore x = Some cx   cy, pcore y = Some cy  cx  cy;
58
  mixin_cmra_validN_op_l n x y : {n} (x  y)  {n} x;
59
60
  mixin_cmra_extend n x y1 y2 :
    {n} x  x {n} y1  y2 
61
     z1 z2, x  z1  z2  z1 {n} y1  z2 {n} y2
Robbert Krebbers's avatar
Robbert Krebbers committed
62
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
63

Robbert Krebbers's avatar
Robbert Krebbers committed
64
(** Bundeled version *)
65
Structure cmraT := CMRAT' {
Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
68
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  cmra_pcore : PCore cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
70
  cmra_op : Op cmra_car;
71
  cmra_valid : Valid cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  cmra_validN : ValidN cmra_car;
73
  cmra_ofe_mixin : OfeMixin cmra_car;
74
  cmra_mixin : CMRAMixin cmra_car;
75
  _ : Type
Robbert Krebbers's avatar
Robbert Krebbers committed
76
}.
77
Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
78
79
80
81
82
(* Given [m : CMRAMixin A], the notation [CMRAT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation CMRAT A m := (CMRAT' A (ofe_mixin_of A%type) m A) (only parsing).

83
84
85
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Arguments cmra_pcore : simpl never.
87
Arguments cmra_op : simpl never.
88
Arguments cmra_valid : simpl never.
89
Arguments cmra_validN : simpl never.
90
Arguments cmra_ofe_mixin : simpl never.
91
Arguments cmra_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Add Printing Constructor cmraT.
93
94
95
96
Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
97
98
Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeC.
Robbert Krebbers's avatar
Robbert Krebbers committed
99

100
101
102
103
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac  A) : CMRAMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
  ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).

104
105
106
107
(** Lifting properties from the mixin *)
Section cmra_mixin.
  Context {A : cmraT}.
  Implicit Types x y : A.
108
  Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
109
  Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
  Lemma cmra_pcore_ne n x y cx :
    x {n} y  pcore x = Some cx   cy, pcore y = Some cy  cx {n} cy.
  Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.
113
114
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
115
116
  Lemma cmra_valid_validN x :  x   n, {n} x.
  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
117
118
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
119
120
121
122
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
125
126
  Lemma cmra_pcore_l x cx : pcore x = Some cx  cx  x  x.
  Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
  Lemma cmra_pcore_idemp x cx : pcore x = Some cx  pcore cx  Some cx.
  Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
127
  Lemma cmra_pcore_mono x y cx :
Robbert Krebbers's avatar
Robbert Krebbers committed
128
    x  y  pcore x = Some cx   cy, pcore y = Some cy  cx  cy.
129
  Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.
130
131
  Lemma cmra_validN_op_l n x y : {n} (x  y)  {n} x.
  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
132
  Lemma cmra_extend n x y1 y2 :
133
    {n} x  x {n} y1  y2 
134
     z1 z2, x  z1  z2  z1 {n} y1  z2 {n} y2.
135
  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
136
137
End cmra_mixin.

Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
140
141
142
143
144
Definition opM {A : cmraT} (x : A) (my : option A) :=
  match my with Some y => x  y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : C_scope.

(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : pcore x  Some x.
Arguments persistent {_} _ {_}.
145
Hint Mode Persistent + ! : typeclass_instances.
146
Instance: Params (@Persistent) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
147

148
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
149
150
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x  y)  False.
Arguments exclusive0_l {_} _ {_} _ _.
151
Hint Mode Exclusive + ! : typeclass_instances.
152
Instance: Params (@Exclusive) 1.
153

154
155
156
157
158
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
  cancelableN n y z : {n}(x  y)  x  y {n} x  z  y {n} z.
Arguments cancelableN {_} _ {_} _ _ _ _.
Hint Mode Cancelable + ! : typeclass_instances.
159
Instance: Params (@Cancelable) 1.
160
161
162
163
164
165

(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
  id_free0_r y : {0}x  x  y {0} x  False.
Arguments id_free0_r {_} _ {_} _ _.
Hint Mode IdFree + ! : typeclass_instances.
166
Instance: Params (@IdFree) 1.
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
171
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
core. *)
Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
172
Hint Mode CMRATotal ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
174

Class Core (A : Type) := core : A  A.
175
Hint Mode Core ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
178
179
180
Instance: Params (@core) 2.

Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
Arguments core' _ _ _ /.

Ralf Jung's avatar
Ralf Jung committed
181
(** * CMRAs with a unit element *)
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
185
186
187
188
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.

Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
  mixin_ucmra_unit_valid :  ε;
  mixin_ucmra_unit_left_id : LeftId () ε ();
  mixin_ucmra_pcore_unit : pcore ε  Some ε
189
}.
190

191
Structure ucmraT := UCMRAT' {
192
193
194
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
195
  ucmra_pcore : PCore ucmra_car;
196
197
198
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  ucmra_unit : Unit ucmra_car;
200
  ucmra_ofe_mixin : OfeMixin ucmra_car;
201
  ucmra_cmra_mixin : CMRAMixin ucmra_car;
202
  ucmra_mixin : UCMRAMixin ucmra_car;
203
  _ : Type;
204
}.
205
Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
206
207
Notation UCMRAT A m :=
  (UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
208
209
210
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
Arguments ucmra_pcore : simpl never.
212
213
214
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
215
Arguments ucmra_ofe_mixin : simpl never.
216
217
218
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
220
221
Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeC.
222
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
223
  CMRAT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
224
225
226
227
228
229
Canonical Structure ucmra_cmraR.

(** Lifting properties from the mixin *)
Section ucmra_mixin.
  Context {A : ucmraT}.
  Implicit Types x y : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
  Lemma ucmra_unit_valid :  (ε : A).
231
  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
  Global Instance ucmra_unit_left_id : LeftId () ε (@op A _).
233
  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
  Lemma ucmra_pcore_unit : pcore (ε:A)  Some ε.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
  Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
236
End ucmra_mixin.
237

238
(** * Discrete CMRAs *)
239
Class CMRADiscrete (A : cmraT) := {
240
241
242
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.
243
Hint Mode CMRADiscrete ! : typeclass_instances.
244

Robbert Krebbers's avatar
Robbert Krebbers committed
245
(** * Morphisms *)
246
247
248
249
250
Class CMRAMorphism {A B : cmraT} (f : A  B) := {
  cmra_morphism_ne :> NonExpansive f;
  cmra_morphism_validN n x : {n} x  {n} f x;
  cmra_morphism_pcore x : pcore (f x)  f <$> pcore x;
  cmra_morphism_op x y : f x  f y  f (x  y)
251
}.
252
253
254
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
255

Robbert Krebbers's avatar
Robbert Krebbers committed
256
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Section cmra.
258
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
Implicit Types x y z : A.
260
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
261

262
(** ** Setoids *)
263
Global Instance cmra_pcore_ne' : NonExpansive (@pcore A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
264
Proof.
265
  intros n x y Hxy. destruct (pcore x) as [cx|] eqn:?.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
269
270
271
  { destruct (cmra_pcore_ne n x y cx) as (cy&->&->); auto. }
  destruct (pcore y) as [cy|] eqn:?; auto.
  destruct (cmra_pcore_ne n y x cy) as (cx&?&->); simplify_eq/=; auto.
Qed.
Lemma cmra_pcore_proper x y cx :
  x  y  pcore x = Some cx   cy, pcore y = Some cy  cx  cy.
272
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
  intros. destruct (cmra_pcore_ne 0 x y cx) as (cy&?&?); auto.
  exists cy; split; [done|apply equiv_dist=> n].
  destruct (cmra_pcore_ne n x y cx) as (cy'&?&?); naive_solver.
276
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
278
Global Instance cmra_pcore_proper' : Proper (() ==> ()) (@pcore A _).
Proof. apply (ne_proper _). Qed.
279
280
Global Instance cmra_op_ne' : NonExpansive2 (@op A _).
Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
281
Global Instance cmra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
282
283
284
285
286
287
288
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 _).
289
290
291
292
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
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.
311
Global Instance cmra_opM_ne : NonExpansive2 (@opM A).
312
Proof. destruct 2; by ofe_subst. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A).
Proof. destruct 2; by setoid_subst. Qed.
315

316
317
318
319
320
321
322
323
324
Global Instance Persistent_proper : Proper (() ==> iff) (@Persistent A).
Proof. solve_proper. Qed.
Global Instance Exclusive_proper : Proper (() ==> iff) (@Exclusive A).
Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
Global Instance Cancelable_proper : Proper (() ==> iff) (@Cancelable A).
Proof. intros x y Hxy. rewrite /Cancelable. by setoid_rewrite Hxy. Qed.
Global Instance IdFree_proper : Proper (() ==> iff) (@IdFree A).
Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
325
326
327
328
(** ** Op *)
Lemma cmra_opM_assoc x y mz : (x  y) ? mz  x  (y ? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.

329
(** ** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
331
332
333
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
334
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
335
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
336
337
338
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
339
(** ** Core *)
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
Lemma cmra_pcore_l' x cx : pcore x  Some cx  cx  x  x.
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
Lemma cmra_pcore_r x cx : pcore x = Some cx  x  cx  x.
343
Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Lemma cmra_pcore_r' x cx : pcore x  Some cx  x  cx  x.
345
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
346
Lemma cmra_pcore_idemp' x cx : pcore x  Some cx  pcore cx  Some cx.
347
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
348
349
350
351
Lemma cmra_pcore_dup x cx : pcore x = Some cx  cx  cx  cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
Lemma cmra_pcore_dup' x cx : pcore x  Some cx  cx  cx  cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
353
354
355
356
357
358
359
Lemma cmra_pcore_validN n x cx : {n} x  pcore x = Some cx  {n} cx.
Proof.
  intros Hvx Hx%cmra_pcore_l. move: Hvx; rewrite -Hx. apply cmra_validN_op_l.
Qed.
Lemma cmra_pcore_valid x cx :  x  pcore x = Some cx   cx.
Proof.
  intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
360

361
362
363
364
(** ** Persistent elements *)
Lemma persistent_dup x `{!Persistent x} : x  x  x.
Proof. by apply cmra_pcore_dup' with x. Qed.

365
(** ** Exclusive elements *)
366
Lemma exclusiveN_l n x `{!Exclusive x} y : {n} (x  y)  False.
367
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
368
369
370
371
372
373
Lemma exclusiveN_r n x `{!Exclusive x} y : {n} (y  x)  False.
Proof. rewrite comm. by apply exclusiveN_l. Qed.
Lemma exclusive_l x `{!Exclusive x} y :  (x  y)  False.
Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
Lemma exclusive_r x `{!Exclusive x} y :  (y  x)  False.
Proof. rewrite comm. by apply exclusive_l. Qed.
374
Lemma exclusiveN_opM n x `{!Exclusive x} my : {n} (x ? my)  my = None.
375
Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
376
377
378
379
Lemma exclusive_includedN n x `{!Exclusive x} y : x {n} y  {n} y  False.
Proof. intros [? ->]. by apply exclusiveN_l. Qed.
Lemma exclusive_included x `{!Exclusive x} y : x  y   y  False.
Proof. intros [? ->]. by apply exclusive_l. Qed.
380

381
(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
Lemma cmra_included_includedN n x y : x  y  x {n} y.
Proof. intros [z ->]. by exists z. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
384
Global Instance cmra_includedN_trans n : Transitive (@includedN A _ _ n).
385
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
  intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2). by rewrite assoc -Hy -Hz.
387
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
388
Global Instance cmra_included_trans: Transitive (@included A _ _).
389
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
  intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2). by rewrite assoc -Hy -Hz.
391
Qed.
392
393
Lemma cmra_valid_included x y :  y  x  y   x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
394
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
395
Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
398

Robbert Krebbers's avatar
Robbert Krebbers committed
399
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
400
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
402
403
404
405
406
407
408
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.
409
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
410
Lemma cmra_included_r x y : y  x  y.
411
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
412

413
Lemma cmra_pcore_mono' x y cx :
Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
416
  x  y  pcore x  Some cx   cy, pcore y = Some cy  cx  cy.
Proof.
  intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
417
  destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
419
  exists cy; by rewrite Hcx.
Qed.
420
Lemma cmra_pcore_monoN' n x y cx :
Robbert Krebbers's avatar
Robbert Krebbers committed
421
  x {n} y  pcore x {n} Some cx   cy, pcore y = Some cy  cx {n} cy.
Robbert Krebbers's avatar
Robbert Krebbers committed
422
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
  intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
424
  destruct (cmra_pcore_mono x (x  z) cx')
Robbert Krebbers's avatar
Robbert Krebbers committed
425
426
427
428
429
    as (cy&Hxy&?); auto using cmra_included_l.
  assert (pcore y {n} Some cy) as (cy'&?&Hcy')%dist_Some_inv_r'.
  { by rewrite Hy Hxy. }
  exists cy'; split; first done.
  rewrite Hcx -Hcy'; auto using cmra_included_includedN.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
431
432
Lemma cmra_included_pcore x cx : pcore x = Some cx  cx  x.
Proof. exists x. by rewrite cmra_pcore_l. Qed.
433

434
Lemma cmra_monoN_l n x y z : x {n} y  z  x {n} z  y.
435
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
436
Lemma cmra_mono_l x y z : x  y  z  x  z  y.
437
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
438
439
440
441
Lemma cmra_monoN_r n x y z : x {n} y  x  z {n} y  z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_monoN_l. Qed.
Lemma cmra_mono_r x y z : x  y  x  z  y  z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_mono_l. Qed.
442
443
444
445
Lemma cmra_monoN n x1 x2 y1 y2 : x1 {n} y1  x2 {n} y2  x1  x2 {n} y1  y2.
Proof. intros; etrans; eauto using cmra_monoN_l, cmra_monoN_r. Qed.
Lemma cmra_mono x1 x2 y1 y2 : x1  y1  x2  y2  x1  x2  y1  y2.
Proof. intros; etrans; eauto using cmra_mono_l, cmra_mono_r. Qed.
446

447
448
449
450
451
452
453
Global Instance cmra_monoN' n :
  Proper (includedN n ==> includedN n ==> includedN n) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_monoN. Qed.
Global Instance cmra_mono' :
  Proper (included ==> included ==> included) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
454
Lemma cmra_included_dist_l n x1 x2 x1' :
455
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
Proof.
457
458
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
459
Qed.
460

Robbert Krebbers's avatar
Robbert Krebbers committed
461
462
(** ** Total core *)
Section total_core.
463
  Local Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
464
465
466
467
468
469
470
471
472
473
  Context `{CMRATotal A}.

  Lemma cmra_core_l x : core x  x  x.
  Proof.
    destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
  Qed.
  Lemma cmra_core_idemp x : core (core x)  core x.
  Proof.
    destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
  Qed.
474
  Lemma cmra_core_mono x y : x  y  core x  core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
476
  Proof.
    intros; destruct (cmra_total x) as [cx Hcx].
477
    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
479
480
    by rewrite /core /= Hcx Hcy.
  Qed.

481
  Global Instance cmra_core_ne : NonExpansive (@core A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
482
  Proof.
483
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
Robbert Krebbers's avatar
Robbert Krebbers committed
484
485
486
487
488
489
490
    by rewrite /core /= -Hxy Hcx.
  Qed.
  Global Instance cmra_core_proper : Proper (() ==> ()) (@core A _).
  Proof. apply (ne_proper _). Qed.

  Lemma cmra_core_r x : x  core x  x.
  Proof. by rewrite (comm _ x) cmra_core_l. Qed.
491
492
  Lemma cmra_core_dup x : core x  core x  core x.
  Proof. by rewrite -{3}(cmra_core_idemp x) cmra_core_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
520
521
522
  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.

  Lemma persistent_total x : Persistent x  core x  x.
  Proof.
    split; [intros; by rewrite /core /= (persistent x)|].
    rewrite /Persistent /core /=.
    destruct (cmra_total x) as [? ->]. by constructor.
  Qed.
  Lemma persistent_core x `{!Persistent x} : core x  x.
  Proof. by apply persistent_total. Qed.

  Global Instance cmra_core_persistent x : Persistent (core x).
  Proof.
    destruct (cmra_total x) as [cx Hcx].
    rewrite /Persistent /core /= Hcx /=. eauto using cmra_pcore_idemp.
  Qed.

  Lemma cmra_included_core x : core x  x.
  Proof. by exists x; rewrite cmra_core_l. Qed.
  Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
  Proof.
    split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
  Qed.
  Global Instance cmra_included_preorder : PreOrder (@included A _ _).
  Proof.
    split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
  Qed.
523
  Lemma cmra_core_monoN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
  Proof.
    intros [z ->].
526
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
529
  Qed.
End total_core.

Robbert Krebbers's avatar
Robbert Krebbers committed
530
(** ** Timeless *)
531
Lemma cmra_timeless_included_l x y : Timeless x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
Proof.
  intros ?? [x' ?].
534
  destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Qed.
537
538
Lemma cmra_timeless_included_r x y : Timeless y  x {0} y  x  y.
Proof. intros ? [x' ?]. exists x'. by apply (timeless y). Qed.
539
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
540
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
Proof.
  intros ??? z Hz.
543
  destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
544
  { rewrite -?Hz. by apply cmra_valid_validN. }
Robbert Krebbers's avatar
Robbert Krebbers committed
545
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
546
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
547

548
549
550
551
552
553
554
555
(** ** 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
556
  split; first by apply cmra_included_includedN.
557
558
  intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
559
560
561

(** Cancelable elements  *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
562
563
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
Lemma cancelable x `{!Cancelable x} y z : (x  y)  x  y  x  z  y  z.
564
565
566
567
568
569
570
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
Lemma discrete_cancelable x `{CMRADiscrete A}:
  ( y z, (x  y)  x  y  x  z  y  z)  Cancelable x.
Proof. intros ????. rewrite -!timeless_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
  Cancelable x  Cancelable y  Cancelable (x  y).
Proof.
571
  intros ?? n z z' ??. apply (cancelableN y), (cancelableN x).
572
573
574
575
576
  - eapply cmra_validN_op_r. by rewrite assoc.
  - by rewrite assoc.
  - by rewrite !assoc.
Qed.
Global Instance exclusive_cancelable (x : A) : Exclusive x  Cancelable x.
577
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
578
579

(** Id-free elements  *)
580
Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
581
Proof.
582
583
  intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
  split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
584
585
Qed.
Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
586
Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
587
588
589
590
591
592
593
594
595
Lemma id_freeN_r n n' x `{!IdFree x} y : {n}x  x  y {n'} x  False.
Proof. eauto using cmra_validN_le, dist_le with lia. Qed.
Lemma id_freeN_l n n' x `{!IdFree x} y : {n}x  y  x {n'} x  False.
Proof. rewrite comm. eauto using id_freeN_r. Qed.
Lemma id_free_r x `{!IdFree x} y : x  x  y  x  False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
Lemma id_free_l x `{!IdFree x} y : x  y  x  x  False.
Proof. rewrite comm. eauto using id_free_r. Qed.
Lemma discrete_id_free x `{CMRADiscrete A}:
596
  ( y,  x  x  y  x  False)  IdFree x.
597
Proof. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
598
Global Instance id_free_op_r x y : IdFree y  Cancelable x  IdFree (x  y).
599
Proof.
600
  intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
601
602
  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
Qed.
603
Global Instance id_free_op_l x y : IdFree x  Cancelable y  IdFree (x  y).
604
605
606
Proof. intros. rewrite comm. apply _. Qed.
Global Instance exclusive_id_free x : Exclusive x  IdFree x.
Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
607
608
End cmra.

609
610
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
612
613
  Context {A : ucmraT}.
  Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
614
  Lemma ucmra_unit_validN n : {n} (ε:A).
Robbert Krebbers's avatar
Robbert Krebbers committed
615
  Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
  Lemma ucmra_unit_leastN n x : ε {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
  Proof. by exists x; rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
618
  Lemma ucmra_unit_least x : ε  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
  Proof. by exists x; rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
  Global Instance ucmra_unit_right_id : RightId () ε (@op A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
621
  Proof. by intros x; rewrite (comm op) left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
  Global Instance ucmra_unit_persistent : Persistent (ε:A).
Robbert Krebbers's avatar
Robbert Krebbers committed
623
624
625
626
  Proof. apply ucmra_pcore_unit. Qed.

  Global Instance cmra_unit_total : CMRATotal A.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
627
628
    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
      eauto using ucmra_unit_least, (persistent (ε:A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
629
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
  Global Instance empty_cancelable : Cancelable (ε:A).
631
  Proof. intros ???. by rewrite !left_id. Qed.
632
633

  (* For big ops *)
Robbert Krebbers's avatar
Robbert Krebbers committed
634
  Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
635
End ucmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
636

637
Hint Immediate cmra_unit_total.
638
639
640

(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
641
  Local Set Default Proof Using "Type*".
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
  Context {A : cmraT} `{!LeibnizEquiv A}.
  Implicit Types x y : A.

  Global Instance cmra_assoc_L : Assoc (=) (@op A _).
  Proof. intros x y z. unfold_leibniz. by rewrite assoc. Qed.
  Global Instance cmra_comm_L : Comm (=) (@op A _).
  Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.

  Lemma cmra_pcore_l_L x cx : pcore x = Some cx  cx  x = x.
  Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.
  Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx  pcore cx = Some cx.
  Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.

  Lemma cmra_opM_assoc_L x y mz : (x  y) ? mz = x  (y ? mz).
  Proof. unfold_leibniz. apply cmra_opM_assoc. Qed.

  (** ** Core *)
  Lemma cmra_pcore_r_L x cx : pcore x = Some cx  x  cx = x.
  Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.
  Lemma cmra_pcore_dup_L x cx : pcore x = Some cx  cx = cx  cx.
  Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.

  (** ** Persistent elements *)
Robbert Krebbers's avatar
Robbert Krebbers committed
665
  Lemma persistent_dup_L x `{!Persistent x} : x = x  x.
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
  Proof. unfold_leibniz. by apply persistent_dup. Qed.

  (** ** Total core *)
  Section total_core.
    Context `{CMRATotal A}.

    Lemma cmra_core_r_L x : x  core x = x.
    Proof. unfold_leibniz. apply cmra_core_r. Qed.
    Lemma cmra_core_l_L x : core x  x = x.
    Proof. unfold_leibniz. apply cmra_core_l. Qed.
    Lemma cmra_core_idemp_L x : core (core x) = core x.
    Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
    Lemma cmra_core_dup_L x : core x = core x  core x.
    Proof. unfold_leibniz. apply cmra_core_dup. Qed.
    Lemma persistent_total_L x : Persistent x  core x = x.
    Proof. unfold_leibniz. apply persistent_total. Qed.
    Lemma persistent_core_L x `{!Persistent x} : core x = x.
    Proof. by apply persistent_total_L. Qed.
  End total_core.
End cmra_leibniz.

Section ucmra_leibniz.
688
  Local Set Default Proof Using "Type*".
689
690
691
  Context {A : ucmraT} `{!LeibnizEquiv A}.
  Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
692
  Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
693
  Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
694
  Global Instance ucmra_unit_right_id_L : RightId (=) ε (@op A _).
695
696
697
  Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
End ucmra_leibniz.

Robbert Krebbers's avatar
Robbert Krebbers committed
698
699
700
(** * Constructing a CMRA with total core *)
Section cmra_total.
  Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
701
702
  Context (total :  x : A, is_Some (pcore x)).
  Context (op_ne :  x : A, NonExpansive (op x)).
703
  Context (core_ne : NonExpansive (@core A _)).
Robbert Krebbers's avatar
Robbert Krebbers committed
704
705
706
707
708
709
710
  Context (validN_ne :  n, Proper (dist n ==> impl) (@validN A _ n)).
  Context (valid_validN :  (x : A),  x   n, {n} x).
  Context (validN_S :  n (x : A), {S n} x  {n} x).
  Context (op_assoc : Assoc () (@op A _)).
  Context (op_comm : Comm () (@op A _)).
  Context (core_l :  x : A, core x  x  x).
  Context (core_idemp :  x : A, core (core x)  core x).
711
  Context (core_mono :  x y : A, x  y  core x  core y).
Robbert Krebbers's avatar
Robbert Krebbers committed
712
713
714
  Context (validN_op_l :  n (x y : A), {n} (x  y)  {n} x).
  Context (extend :  n (x y1 y2 : A),
    {n} x  x {n} y1  y2 
715
     z1 z2, x  z1  z2  z1 {n} y1  z2 {n} y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
716
  Lemma cmra_total_mixin : CMRAMixin A.
717
  Proof using Type*.
Robbert Krebbers's avatar
Robbert Krebbers committed
718
719
720
721
722
723
    split; auto.
    - intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
      case (total y)=> [cy ->]; eauto.
    - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
    - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
      case (total cx)=>[ccx ->]; by constructor.
724
    - intros x y cx Hxy%core_mono Hx. move: Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
725
726
727
      rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
  Qed.
End cmra_total.
728

729
730
731
732
733
734
735
(** * Properties about morphisms *)
Instance cmra_morphism_id {A : cmraT} : CMRAMorphism (@id A).
Proof. split=>//=. apply _. intros. by rewrite option_fmap_id. Qed.
Instance cmra_morphism_proper {A B : cmraT} (f : A  B) `{!CMRAMorphism f} :
  Proper (() ==> ()) f := ne_proper _.
Instance cmra_morphism_compose {A B C : cmraT} (f : A  B) (g : B  C) :
  CMRAMorphism f  CMRAMorphism g  CMRAMorphism (g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
736
737
Proof.
  split.
738
  - apply _.
739
740
741
  - move=> n x Hx /=. by apply cmra_morphism_validN, cmra_morphism_validN.
  - move=> x /=. by rewrite 2!cmra_morphism_pcore option_fmap_compose.
  - move=> x y /=. by rewrite !cmra_morphism_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
742
Qed.