cmra.v 67.2 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
  (* 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
179
Class Core (A : Type) := core : A  A.
180
Hint Mode Core ! : typeclass_instances.
181
Instance: Params (@core) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
182

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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