cmra.v 67 KB
Newer Older
1
From iris.algebra Require Export ofe monoid.
2
From stdpp Require Import finite.
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
  _ : Type
Robbert Krebbers's avatar
Robbert Krebbers committed
80
}.
81 82
Arguments CmraT' _ {_ _ _ _ _ _} _ _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
83 84
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. *)
85
Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m A) (only parsing).
86

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
142 143
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
144
Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
145

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

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

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

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

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

176 177
(** The function [core] returns a dummy when used on CMRAs without total
core. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Class Core (A : Type) := core : A  A.
179
Hint Mode Core ! : typeclass_instances.
180
Instance: Params (@core) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
181

182
Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
Robbert Krebbers's avatar
Robbert Krebbers committed
183 184
Arguments core' _ _ _ /.

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
249
(** * Morphisms *)
250
Class CmraMorphism {A B : cmraT} (f : A  B) := {
251 252 253 254
  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)
255
}.
256 257 258
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
259

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

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
461 462 463 464 465 466 467 468 469 470 471 472 473
(** ** 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
474 475
(** ** Total core *)
Section total_core.
476
  Local Set Default Proof Using "Type*".
477
  Context `{CmraTotal A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
478

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

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

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

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

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

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

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

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

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

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

648
  Global Instance cmra_unit_cmra_total : CmraTotal A.
Robbert Krebbers's avatar
Robbert Krebbers committed
649
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
650
    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
651
      eauto using ucmra_unit_least, (core_id (ε:A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
652
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
653
  Global Instance empty_cancelable : Cancelable (ε:A).
654
  Proof. intros