cmra.v 66.1 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
(** Bundeled 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_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeC.
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_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeC.
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 366
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x  x  x.
367 368
Proof. by apply cmra_pcore_dup' with x. Qed.

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

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

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

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

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

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

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

  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.
478
  Lemma cmra_core_mono x y : x  y  core x  core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
479 480
  Proof.
    intros; destruct (cmra_total x) as [cx Hcx].
481
    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483 484
    by rewrite /core /= Hcx Hcy.
  Qed.

485
  Global Instance cmra_core_ne : NonExpansive (@core A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
486
  Proof.
487
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489 490 491 492 493 494
    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.
495 496
  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
497 498 499 500 501
  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.

502
  Lemma core_id_total x : CoreId x  core x  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
  Proof.
504 505
    split; [intros; by rewrite /core /= (core_id x)|].
    rewrite /CoreId /core /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
506 507
    destruct (cmra_total x) as [? ->]. by constructor.
  Qed.
508 509
  Lemma core_id_core x `{!CoreId x} : core x  x.
  Proof. by apply core_id_total. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
510

511
  Global Instance cmra_core_core_id x : CoreId (core x).
Robbert Krebbers's avatar
Robbert Krebbers committed
512 513
  Proof.
    destruct (cmra_total x) as [cx Hcx].
514
    rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516 517 518 519 520 521 522 523 524 525 526
  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.
527
  Lemma cmra_core_monoN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529
  Proof.
    intros [z ->].
530
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
531 532 533
  Qed.
End total_core.

534 535
(** ** Discrete *)
Lemma cmra_discrete_included_l x y : Discrete x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
536 537
Proof.
  intros ?? [x' ?].
538
  destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
539
  by exists z'; rewrite Hy (discrete x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
540
Qed.
541 542 543 544
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
545 546
Proof.
  intros ??? z Hz.
547
  destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
548
  { rewrite -?Hz. by apply cmra_valid_validN. }
549
  by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551

552
(** ** Discrete *)
553
Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x :  x  {n} x.
554 555 556 557
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
558 559
Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : {0} x  {n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
560
Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x  y  x {n} y.
561
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
  split; first by apply cmra_included_includedN.
563
  intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
564
Qed.
565 566
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.
567 568 569

(** Cancelable elements  *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
570 571
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.
572
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
573
Lemma discrete_cancelable x `{CmraDiscrete A}:
574
  ( y z, (x  y)  x  y  x  z  y  z)  Cancelable x.
575
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
576 577 578
Global Instance cancelable_op x y :
  Cancelable x  Cancelable y  Cancelable (x  y).
Proof.
579
  intros ?? n z z' ??. apply (cancelableN y), (cancelableN x).
580 581 582 583 584
  - 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.
585
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
586 587

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

619 620
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
621 622 623
  Context {A : ucmraT}.
  Implicit Types x y z : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
624
  Lemma ucmra_unit_validN n : {n} (ε:A).
Robbert Krebbers's avatar
Robbert Krebbers committed
625
  Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
  Lemma ucmra_unit_leastN n x : ε {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
627
  Proof. by exists x; rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
628
  Lemma ucmra_unit_least x : ε  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
629
  Proof. by exists x; rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
  Global Instance ucmra_unit_right_id : RightId () ε (@op A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
631
  Proof. by intros x; rewrite (comm op) left_id. Qed.
632
  Global Instance ucmra_unit_core_id : CoreId (ε:A).
Robbert Krebbers's avatar
Robbert Krebbers committed
633 634
  Proof. apply ucmra_pcore_unit. Qed.

635
  Global Instance cmra_unit_cmra_total : CmraTotal A.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
638
      eauto using ucmra_unit_least, (core_id (ε:A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
639
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
  Global Instance empty_cancelable : Cancelable (ε:A).
641
  Proof. intros ???. by rewrite !left_id. Qed.
642 643

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

Tej Chajed's avatar
Tej Chajed committed