cmra.v 72.6 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
    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);