cmra.v 59.7 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 *)
182
(** We use the notation ∅ because for most instances (maps, sets, etc) the
Ralf Jung's avatar
Ralf Jung committed
183
`empty' element is the unit. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
184
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
185
186
  mixin_ucmra_unit_valid :  ;
  mixin_ucmra_unit_left_id : LeftId ()  ();
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  mixin_ucmra_pcore_unit : pcore   Some 
188
}.
189

190
Structure ucmraT := UCMRAT' {
191
192
193
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
194
  ucmra_pcore : PCore ucmra_car;
195
196
197
198
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_empty : Empty ucmra_car;
199
  ucmra_ofe_mixin : OfeMixin ucmra_car;
200
  ucmra_cmra_mixin : CMRAMixin ucmra_car;
201
  ucmra_mixin : UCMRAMixin ucmra_car;
202
  _ : Type;
203
}.
204
Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
205
206
Notation UCMRAT A m :=
  (UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
207
208
209
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Arguments ucmra_pcore : simpl never.
211
212
213
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
214
Arguments ucmra_ofe_mixin : simpl never.
215
216
217
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
218
Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
219
220
Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeC.
221
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
222
  CMRAT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
223
224
225
226
227
228
229
230
231
232
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
  Lemma ucmra_pcore_unit : pcore (:A)  Some .
  Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
235
End ucmra_mixin.
236

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

Robbert Krebbers's avatar
Robbert Krebbers committed
244
(** * Morphisms *)
245
246
247
248
249
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)
250
}.
251
252
253
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
254

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

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

315
316
317
318
319
320
321
322
323
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
324
325
326
327
(** ** Op *)
Lemma cmra_opM_assoc x y mz : (x  y) ? mz  x  (y ? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.

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

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

364
(** ** Exclusive elements *)
365
Lemma exclusiveN_l n x `{!Exclusive x} y : {n} (x  y)  False.
366
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
367
368
369
370
371
372
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.
373
Lemma exclusiveN_opM n x `{!Exclusive x} my : {n} (x ? my)  my = None.
374
Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
375
376
377
378
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.
379

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

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

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

433
Lemma cmra_monoN_l n x y z : x {n} y  z  x {n} z  y.
434
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
435
Lemma cmra_mono_l x y z : x  y  z  x  z  y.
436
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
437
438
439
440
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.
441
442
443
444
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.
445

446
447
448
449
450
451
452
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
453
Lemma cmra_included_dist_l n x1 x2 x1' :
454
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
455
Proof.
456
457
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
458
Qed.
459

Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
(** ** Total core *)
Section total_core.
462
  Local Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
466
467
468
469
470
471
472
  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.
473
  Lemma cmra_core_mono x y : x  y  core x  core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
  Proof.
    intros; destruct (cmra_total x) as [cx Hcx].
476
    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
478
479
    by rewrite /core /= Hcx Hcy.
  Qed.

480
  Global Instance cmra_core_ne : NonExpansive (@core A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
481
  Proof.
482
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
Robbert Krebbers's avatar
Robbert Krebbers committed
483
484
485
486
487
488
489
    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.
490
491
  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
492
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
  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.
522
  Lemma cmra_core_monoN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
523
524
  Proof.
    intros [z ->].
525
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
527
528
  Qed.
End total_core.

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

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

(** Cancelable elements  *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
561
562
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.
563
564
565
566
567
568
569
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.
570
  intros ?? n z z' ??. apply (cancelableN y), (cancelableN x).
571
572
573
574
575
  - 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.
576
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
577
578

(** Id-free elements  *)
579
Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
580
Proof.
581
582
  intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
  split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
583
584
Qed.
Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
585
Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
586
587
588
589
590
591
592
593
594
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}:
595
  ( y,  x  x  y  x  False)  IdFree x.
596
Proof. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
597
Global Instance id_free_op_r x y : IdFree y  Cancelable x  IdFree (x  y).
598
Proof.
599
  intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
600
601
  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
Qed.
602
Global Instance id_free_op_l x y : IdFree x  Cancelable y  IdFree (x  y).
603
604
605
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
606
607
End cmra.

608
609
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
  Context {A : ucmraT}.
  Implicit Types x y z : A.

  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. apply ucmra_pcore_unit. Qed.

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

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

636
Hint Immediate cmra_unit_total.
637
638
639

(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
640
  Local Set Default Proof Using "Type*".
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
  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
664
  Lemma persistent_dup_L x `{!Persistent x} : x = x  x.
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
  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.
687
  Local Set Default Proof Using "Type*".
688
689
690
691
692
693
694
695
696
  Context {A : ucmraT} `{!LeibnizEquiv A}.
  Implicit Types x y z : A.

  Global Instance ucmra_unit_left_id_L : LeftId (=)  (@op A _).
  Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
  Global Instance ucmra_unit_right_id_L : RightId (=)  (@op A _).
  Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
End ucmra_leibniz.

Robbert Krebbers's avatar
Robbert Krebbers committed
697
698
699
(** * Constructing a CMRA with total core *)
Section cmra_total.
  Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
700
701
  Context (total :  x : A, is_Some (pcore x)).
  Context (op_ne :  x : A, NonExpansive (op x)).
702
  Context (core_ne : NonExpansive (@core A _)).
Robbert Krebbers's avatar
Robbert Krebbers committed
703
704
705
706
707
708
709
  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).
710
  Context (core_mono :  x y : A, x  y  core x  core y).
Robbert Krebbers's avatar
Robbert Krebbers committed
711
712
713
  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 
714
     z1 z2, x  z1  z2  z1 {n} y1  z2 {n} y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
715
  Lemma cmra_total_mixin : CMRAMixin A.
716
  Proof using Type*.
Robbert Krebbers's avatar
Robbert Krebbers committed
717
718
719
720
721
722
    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.
723
    - intros x y cx Hxy%core_mono Hx. move: Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
725
726
      rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
  Qed.
End cmra_total.
727

728
729
730
731
732
733
734
(** * 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
735
736
Proof.
  split.
737
  - apply _.
738
739
740
  - 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
741
Qed.
742

743
Section cmra_morphism.
744
  Local Set Default Proof Using "Type*".
745
746
747
748
749
750
751
  Context {A B : cmraT} (f : A  B) `{!CMRAMorphism f}.
  Lemma cmra_morphism_core x : core (f x)  f (core x).
  Proof. unfold core, core'. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed.
  Lemma cmra_morphism_monotone x y : x  y  f x  f y.
  Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
  Lemma cmra_morphism_monotoneN n x y : x {n} y  f x {n} f y.
  Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
752
  Lemma cmra_monotone_valid x :  x   f x.
753
754
  Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
End cmra_morphism.
755

756
757
(** Functors *)
Structure rFunctor := RFunctor {
758
  rFunctor_car : ofeT  ofeT  cmraT;
Robbert Krebbers's avatar