cmra.v 69.5 KB
Newer Older
1
From stdpp Require Import finite.
2
From iris.algebra Require Export ofe monoid.
3
Set Default Proof Using "Type".
4

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

Class Op (A : Type) := op : A  A  A.
10
Hint Mode Op ! : typeclass_instances.
11
Instance: Params (@op) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
14

15
16
17
18
19
(* 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
*)
20
Definition included `{Equiv A, Op A} (x y : A) :=  z, y  x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Tej Chajed's avatar
Tej Chajed committed
23
Hint Extern 0 (_  _) => reflexivity : core.
24
Instance: Params (@included) 3 := {}.
25

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

32
Class Valid (A : Type) := valid : A  Prop.
33
Hint Mode Valid ! : typeclass_instances.
34
Instance: Params (@valid) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
36

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
68
(** Bundled version *)
69
Structure cmraT := CmraT' {
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  cmra_pcore : PCore cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  cmra_op : Op cmra_car;
75
  cmra_valid : Valid cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  cmra_validN : ValidN cmra_car;
77
  cmra_ofe_mixin : OfeMixin cmra_car;
78
  cmra_mixin : CmraMixin cmra_car;
79
  (* always same as [cmra_car], but by also having this as last field unification sometimes gets faster *)
80
  _ : Type
Robbert Krebbers's avatar
Robbert Krebbers committed
81
}.
82
83
Arguments CmraT' _ {_ _ _ _ _ _} _ _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
84
85
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. *)
86
Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m A) (only parsing).
87

88
89
90
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Arguments cmra_pcore : simpl never.
92
Arguments cmra_op : simpl never.
93
Arguments cmra_valid : simpl never.
94
Arguments cmra_validN : simpl never.
95
Arguments cmra_ofe_mixin : simpl never.
96
Arguments cmra_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Add Printing Constructor cmraT.
98
99
100
101
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.
102
103
Coercion cmra_ofeO (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
Robbert Krebbers's avatar
Robbert Krebbers committed
104

105
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac  A) : CmraMixin Ac := cmra_mixin Ac.
106
107
108
Notation cmra_mixin_of A :=
  ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).

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

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

147
148
149
150
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x  Some x.
Arguments core_id {_} _ {_}.
Hint Mode CoreId + ! : typeclass_instances.
151
Instance: Params (@CoreId) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
152

153
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
154
155
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x  y)  False.
Arguments exclusive0_l {_} _ {_} _ _.
156
Hint Mode Exclusive + ! : typeclass_instances.
157
Instance: Params (@Exclusive) 1 := {}.
158

159
160
161
162
163
(** * 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.
164
Instance: Params (@Cancelable) 1 := {}.
165
166
167
168
169
170

(** * 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.
171
Instance: Params (@IdFree) 1 := {}.
172

Robbert Krebbers's avatar
Robbert Krebbers committed
173
(** * CMRAs whose core is total *)
174
175
Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Hint Mode CmraTotal ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
176

177
178
(** The function [core] returns a dummy when used on CMRAs without total
core. *)
Ralf Jung's avatar
Ralf Jung committed
179
Definition core `{PCore A} (x : A) : A := default x (pcore x).
180
Instance: Params (@core) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
181

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

186
Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
187
  mixin_ucmra_unit_valid :  (ε : A);
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
  mixin_ucmra_unit_left_id : LeftId () ε ();
  mixin_ucmra_pcore_unit : pcore ε  Some ε
190
}.
191

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

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

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

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

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

317
Global Instance CoreId_proper : Proper (() ==> iff) (@CoreId A).
318
319
320
321
322
323
324
325
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
326
(** ** Op *)
327
Lemma cmra_op_opM_assoc x y mz : (x  y) ? mz  x  (y ? mz).
Robbert Krebbers's avatar
Robbert Krebbers committed
328
329
Proof. destruct mz; by rewrite /= -?assoc. Qed.

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

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

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

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
458
459
460
461
462
463
464
465
466
467
468
469
470
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x  x  x.
Proof. by apply cmra_pcore_dup' with x. Qed.

Lemma core_id_extract x y `{!CoreId x} :
  x  y  y  y  x.
Proof.
  intros ?.
  destruct (cmra_pcore_mono' x y x) as (cy & Hcy & [x' Hx']); [done|exact: core_id|].
  rewrite -(cmra_pcore_r y) //. rewrite Hx' -!assoc. f_equiv.
  rewrite [x'  x]comm assoc -core_id_dup. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
471
472
(** ** Total core *)
Section total_core.
473
  Local Set Default Proof Using "Type*".
474
  Context `{CmraTotal A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
475

476
477
  Lemma cmra_pcore_core x : pcore x = Some (core x).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
478
    rewrite /core. destruct (cmra_total x) as [cx ->]. done.
479
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
481
482
483
484
485
486
487
  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.
488
  Lemma cmra_core_mono x y : x  y  core x  core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
490
  Proof.
    intros; destruct (cmra_total x) as [cx Hcx].
491
    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
494
    by rewrite /core /= Hcx Hcy.
  Qed.

495
  Global Instance cmra_core_ne : NonExpansive (@core A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
496
  Proof.
497
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
500
501
502
503
504
    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.
505
506
  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
507
508
509
510
511
  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.

512
  Lemma core_id_total x : CoreId x  core x  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
  Proof.
514
515
    split; [intros; by rewrite /core /= (core_id x)|].
    rewrite /CoreId /core /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
516
517
    destruct (cmra_total x) as [? ->]. by constructor.
  Qed.
518
519
  Lemma core_id_core x `{!CoreId x} : core x  x.
  Proof. by apply core_id_total. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520

521
  Global Instance cmra_core_core_id x : CoreId (core x).
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
  Proof.
    destruct (cmra_total x) as [cx Hcx].
524
    rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
527
528
529
530
531
532
533
534
535
536
  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.
537
  Lemma cmra_core_monoN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
539
  Proof.
    intros [z ->].
540
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
543
  Qed.
End total_core.

544
545
(** ** Discrete *)
Lemma cmra_discrete_included_l x y : Discrete x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
546
547
Proof.
  intros ?? [x' ?].
548
  destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
549
  by exists z'; rewrite Hy (discrete x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Qed.
551
552
553
554
Lemma cmra_discrete_included_r x y : Discrete y  x {0} y  x  y.
Proof. intros ? [x' ?]. exists x'. by apply (discrete y). Qed.
Lemma cmra_op_discrete x1 x2 :
   (x1  x2)  Discrete x1  Discrete x2  Discrete (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
555
556
Proof.
  intros ??? z Hz.
557
  destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
558
  { rewrite -?Hz. by apply cmra_valid_validN. }
559
  by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
560
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
561

562
(** ** Discrete *)
563
Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x :  x  {n} x.
564
565
566
567
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
568
569
Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : {0} x  {n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
570
Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x  y  x {n} y.
571
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
  split; first by apply cmra_included_includedN.
573
  intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
574
Qed.
575
576
Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x {0} y  x {n} y.
Proof. by rewrite -!cmra_discrete_included_iff. Qed.
577
578
579

(** Cancelable elements  *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
580
581
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.
582
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
583
Lemma discrete_cancelable x `{CmraDiscrete A}:
584
  ( y z, (x  y)  x  y  x  z  y  z)  Cancelable x.
585
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
586
587
588
Global Instance cancelable_op x y :
  Cancelable x  Cancelable y  Cancelable (x  y).
Proof.
589
  intros ?? n z z' ??. apply (cancelableN y), (cancelableN x).
590
591
592
593
594
  - 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.
595
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
596
597

(** Id-free elements  *)
598
Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
599
Proof.
600
601
  intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
  split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
602
603
Qed.
Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
604
Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
605
606
607
608
609
610
611
612
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.
613
Lemma discrete_id_free x `{CmraDiscrete A}:
614
  ( y,  x  x  y  x  False)  IdFree x.
615
Proof.
616
  intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
617
Qed.
618
Global Instance id_free_op_r x y : IdFree y  Cancelable x  IdFree (x  y).
619
Proof.
620
  intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
621
  eapply (id_free0_r y); [by eapply cmra_validN_op_r |symmetry; eauto].
622
Qed.
623
Global Instance id_free_op_l x y : IdFree x  Cancelable y  IdFree (x  y).
624
625
626
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
627
628
End cmra.

629
630
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
632
633
  Context {A : ucmraT}.
  Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
634
  Lemma ucmra_unit_validN n : {n} (ε:A).
Robbert Krebbers's avatar
Robbert Krebbers committed
635
  Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
  Lemma ucmra_unit_leastN n x : ε {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  Proof. by exists x; rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
638
  Lemma ucmra_unit_least x : ε  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
639
  Proof. by exists x; rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
  Global Instance ucmra_unit_right_id : RightId () ε (@op A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
641
  Proof. by intros x; rewrite (comm op) left_id. Qed.
642
  Global Instance ucmra_unit_core_id : CoreId (ε:A).
Robbert Krebbers's avatar
Robbert Krebbers committed
643
644
  Proof. apply ucmra_pcore_unit. Qed.

645
  Global Instance cmra_unit_cmra_total : CmraTotal A.
Robbert Krebbers's avatar
Robbert Krebbers committed
646
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
647
648
649
    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?); [..|by eauto].
    - apply ucmra_unit_least.
    - apply (core_id _).
Robbert Krebbers's avatar
Robbert Krebbers committed
650
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
651
  Global Instance empty_cancelable : Cancelable (ε:A).
652
  Proof. intros ???. by rewrite !left_id. Qed.
653
654

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

Tej Chajed's avatar
Tej Chajed committed
658
Hint Immediate cmra_unit_cmra_total : core.