cmra.v 59.7 KB
Newer Older
1
From iris.algebra Require Export ofe monoid.
2
Set Default Proof Using "Type".
3

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

Class Op (A : Type) := op : A  A  A.
9
Hint Mode Op ! : typeclass_instances.
10 11 12 13
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

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

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

31
Class Valid (A : Type) := valid : A  Prop.
32
Hint Mode Valid ! : typeclass_instances.
33
Instance: Params (@valid) 2.
34
Notation "✓ x" := (valid x) (at level 20) : C_scope.
35

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
64
(** Bundeled version *)
65
Structure cmraT := CMRAT' {
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  cmra_pcore : PCore cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
70
  cmra_op : Op cmra_car;
71
  cmra_valid : Valid cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  cmra_validN : ValidN cmra_car;
73
  cmra_ofe_mixin : OfeMixin cmra_car;
74
  cmra_mixin : CMRAMixin cmra_car;
75
  _ : Type
Robbert Krebbers's avatar
Robbert Krebbers committed
76
}.
77
Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
78 79 80 81 82
(* Given [m : CMRAMixin A], the notation [CMRAT A m] provides a smart
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. *)
Notation CMRAT A m := (CMRAT' A (ofe_mixin_of A%type) m A) (only parsing).

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

100 101 102 103
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac  A) : CMRAMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
  ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).

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

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

(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : pcore x  Some x.
Arguments persistent {_} _ {_}.
145
Hint Mode Persistent + ! : typeclass_instances.
146
Instance: Params (@Persistent) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
147

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

154 155 156 157 158
(** * 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.
159
Instance: Params (@Cancelable) 1.
160 161 162 163 164 165

(** * 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.
166
Instance: Params (@IdFree) 1.
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170 171
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
core. *)
Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
172
Hint Mode CMRATotal ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174

Class Core (A : Type) := core : A  A.
175
Hint Mode Core ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177 178 179 180
Instance: Params (@core) 2.

Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
Arguments core' _ _ _ /.

Ralf Jung's avatar
Ralf Jung committed
181
(** * CMRAs with a unit element *)
182
(** We use the notation ∅ because for most instances (maps, sets, etc) the
Ralf Jung's avatar
Ralf Jung committed
183
`empty' element is the unit. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
184
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
185 186
  mixin_ucmra_unit_valid :  ;
  mixin_ucmra_unit_left_id : LeftId ()  ();
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  mixin_ucmra_pcore_unit : pcore   Some 
188
}.
189

190
Structure ucmraT := UCMRAT' {
191 192 193
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
194
  ucmra_pcore : PCore ucmra_car;
195 196 197 198
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_empty : Empty ucmra_car;
199
  ucmra_ofe_mixin : OfeMixin ucmra_car;
200
  ucmra_cmra_mixin : CMRAMixin ucmra_car;
201
  ucmra_mixin : UCMRAMixin ucmra_car;
202
  _ : Type;
203
}.
204
Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
205 206
Notation UCMRAT A m :=
  (UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
207 208 209
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Arguments ucmra_pcore : simpl never.
211 212 213
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
214
Arguments ucmra_ofe_mixin : simpl never.
215 216 217
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
218
Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
219 220
Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeC.
221
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
222
  CMRAT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
223 224 225 226 227 228 229 230 231 232
Canonical Structure ucmra_cmraR.

(** Lifting properties from the mixin *)
Section ucmra_mixin.
  Context {A : ucmraT}.
  Implicit Types x y : A.
  Lemma ucmra_unit_valid :  ( : A).
  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
  Global Instance ucmra_unit_left_id : LeftId ()  (@op A _).
  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234
  Lemma ucmra_pcore_unit : pcore (:A)  Some .
  Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
235
End ucmra_mixin.
236

237
(** * Discrete CMRAs *)
238
Class CMRADiscrete (A : cmraT) := {
239 240 241
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.
242
Hint Mode CMRADiscrete ! : typeclass_instances.
243

Robbert Krebbers's avatar
Robbert Krebbers committed
244
(** * Morphisms *)
245 246 247 248 249
Class CMRAMorphism {A B : cmraT} (f : A  B) := {
  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)
250
}.
251 252 253
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
254

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

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

315 316 317 318 319 320 321 322 323
Global Instance Persistent_proper : Proper (() ==> iff) (@Persistent A).
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
324 325 326 327
(** ** Op *)
Lemma cmra_opM_assoc x y mz : (x  y) ? mz  x  (y ? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.

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

360 361 362 363
(** ** Persistent elements *)
Lemma persistent_dup x `{!Persistent x} : x  x  x.
Proof. by apply cmra_pcore_dup' with x. Qed.

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
460 461
(** ** Total core *)
Section total_core.
462
  Local Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
463 464 465 466 467 468 469 470 471 472
  Context `{CMRATotal A}.

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

480
  Global Instance cmra_core_ne : NonExpansive (@core A _).
Robbert Krebbers's avatar
Robbert Krebbers committed
481
  Proof.
482
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
Robbert Krebbers's avatar
Robbert Krebbers committed
483 484 485 486 487 488 489
    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.
490 491
  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
492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
  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.

  Lemma persistent_total x : Persistent x  core x  x.
  Proof.
    split; [intros; by rewrite /core /= (persistent x)|].
    rewrite /Persistent /core /=.
    destruct (cmra_total x) as [? ->]. by constructor.
  Qed.
  Lemma persistent_core x `{!Persistent x} : core x  x.
  Proof. by apply persistent_total. Qed.

  Global Instance cmra_core_persistent x : Persistent (core x).
  Proof.
    destruct (cmra_total x) as [cx Hcx].
    rewrite /Persistent /core /= Hcx /=. eauto using cmra_pcore_idemp.
  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.
522
  Lemma cmra_core_monoN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524
  Proof.
    intros [z ->].
525
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
526 527 528
  Qed.
End total_core.

Robbert Krebbers's avatar
Robbert Krebbers committed
529
(** ** Timeless *)
530
Lemma cmra_timeless_included_l x y : Timeless x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
531 532
Proof.
  intros ?? [x' ?].
533
  destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
534
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
535
Qed.
536 537
Lemma cmra_timeless_included_r x y : Timeless y  x {0} y  x  y.
Proof. intros ? [x' ?]. exists x'. by apply (timeless y). Qed.
538
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
539
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541
Proof.
  intros ??? z Hz.
542
  destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
543
  { rewrite -?Hz. by apply cmra_valid_validN. }
Robbert Krebbers's avatar
Robbert Krebbers committed
544
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
545
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
546

547 548 549 550 551 552 553 554
(** ** Discrete *)
Lemma cmra_discrete_valid_iff `{CMRADiscrete A} n x :  x  {n} x.
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x  y  x {n} y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
  split; first by apply cmra_included_includedN.
556 557
  intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
558 559 560

(** Cancelable elements  *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
561 562
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.
563 564 565 566 567 568 569
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
Lemma discrete_cancelable x `{CMRADiscrete A}:
  ( y z, (x  y)  x  y  x  z  y  z)  Cancelable x.
Proof. intros ????. rewrite -!timeless_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
  Cancelable x  Cancelable y  Cancelable (x  y).
Proof.
570
  intros ?? n z z' ??. apply (cancelableN y), (cancelableN x).
571 572 573 574 575
  - 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.
576
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
577 578

(** Id-free elements  *)
579
Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
580
Proof.
581 582
  intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
  split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
583 584
Qed.
Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
585
Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
586 587 588 589 590 591 592 593 594
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.
Lemma discrete_id_free x `{CMRADiscrete A}:
595
  ( y,  x  x  y  x  False)  IdFree x.
596
Proof. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
597
Global Instance id_free_op_r x y : IdFree y  Cancelable x  IdFree (x  y).
598
Proof.
599
  intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
600 601
  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
Qed.
602
Global Instance id_free_op_l x y : IdFree x  Cancelable y  IdFree (x  y).
603 604 605
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
606 607
End cmra.

608 609
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625
  Context {A : ucmraT}.
  Implicit Types x y z : A.

  Lemma ucmra_unit_validN n : {n} (:A).
  Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
  Lemma ucmra_unit_leastN n x :  {n} x.
  Proof. by exists x; rewrite left_id. Qed.
  Lemma ucmra_unit_least x :   x.
  Proof. by exists x; rewrite left_id. Qed.
  Global Instance ucmra_unit_right_id : RightId ()  (@op A _).
  Proof. by intros x; rewrite (comm op) left_id. Qed.
  Global Instance ucmra_unit_persistent : Persistent (:A).
  Proof. apply ucmra_pcore_unit. Qed.

  Global Instance cmra_unit_total : CMRATotal A.
  Proof.
626
    intros x. destruct (cmra_pcore_mono'  x ) as (cx&->&?);
627
      eauto using ucmra_unit_least, (persistent (:A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
628
  Qed.
629 630
  Global Instance empty_cancelable : Cancelable (:A).
  Proof. intros ???. by rewrite !left_id. Qed.
631 632 633

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

636
Hint Immediate cmra_unit_total.
637 638 639

(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
640
  Local Set Default Proof Using "Type*".
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663
  Context {A : cmraT} `{!LeibnizEquiv A}.
  Implicit Types x y : A.

  Global Instance cmra_assoc_L : Assoc (=) (@op A _).
  Proof. intros x y z. unfold_leibniz. by rewrite assoc. Qed.
  Global Instance cmra_comm_L : Comm (=) (@op A _).
  Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.

  Lemma cmra_pcore_l_L x cx : pcore x = Some cx  cx  x = x.
  Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.
  Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx  pcore cx = Some cx.
  Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.

  Lemma cmra_opM_assoc_L x y mz : (x  y) ? mz = x  (y ? mz).
  Proof. unfold_leibniz. apply cmra_opM_assoc. Qed.

  (** ** Core *)
  Lemma cmra_pcore_r_L x cx : pcore x = Some cx  x  cx = x.
  Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.
  Lemma cmra_pcore_dup_L x cx : pcore x = Some cx  cx = cx  cx.
  Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.

  (** ** Persistent elements *)
Robbert Krebbers's avatar
Robbert Krebbers committed
664
  Lemma persistent_dup_L x `{!Persistent x} : x = x  x.
665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686
  Proof. unfold_leibniz. by apply persistent_dup. Qed.

  (** ** Total core *)
  Section total_core.
    Context `{CMRATotal A}.

    Lemma cmra_core_r_L x : x  core x = x.
    Proof. unfold_leibniz. apply cmra_core_r. Qed.
    Lemma cmra_core_l_L x : core x  x = x.
    Proof. unfold_leibniz. apply cmra_core_l. Qed.
    Lemma cmra_core_idemp_L x : core (core x) = core x.
    Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
    Lemma cmra_core_dup_L x : core x = core x  core x.
    Proof. unfold_leibniz. apply cmra_core_dup. Qed.
    Lemma persistent_total_L x : Persistent x  core x = x.
    Proof. unfold_leibniz. apply persistent_total. Qed.
    Lemma persistent_core_L x `{!Persistent x} : core x = x.
    Proof. by apply persistent_total_L. Qed.
  End total_core.
End cmra_leibniz.

Section ucmra_leibniz.
687
  Local Set Default Proof Using "Type*".
688 689 690 691 692 693 694 695 696
  Context {A : ucmraT} `{!LeibnizEquiv A}.
  Implicit Types x y z : A.

  Global Instance ucmra_unit_left_id_L : LeftId (=)  (@op A _).
  Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
  Global Instance ucmra_unit_right_id_L : RightId (=)  (@op A _).
  Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
End ucmra_leibniz.

Robbert Krebbers's avatar
Robbert Krebbers committed
697 698 699
(** * Constructing a CMRA with total core *)
Section cmra_total.
  Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
700 701
  Context (total :  x : A, is_Some (pcore x)).
  Context (op_ne :  x : A, NonExpansive (op x)).
702
  Context (core_ne : NonExpansive (@core A _)).
Robbert Krebbers's avatar
Robbert Krebbers committed
703 704 705 706 707 708 709
  Context (validN_ne :  n, Proper (dist n ==> impl) (@validN A _ n)).
  Context (valid_validN :  (x : A),  x   n, {n} x).
  Context (validN_S :  n (x : A), {S n} x  {n} x).
  Context (op_assoc : Assoc () (@op A _)).
  Context (op_comm : Comm () (@op A _)).
  Context (core_l :  x : A, core x  x  x).
  Context (core_idemp :  x : A, core (core x)  core x).
710
  Context (core_mono :  x y : A, x  y  core x  core y).
Robbert Krebbers's avatar
Robbert Krebbers committed
711 712 713
  Context (validN_op_l :  n (x y : A), {n} (x  y)  {n} x).
  Context (extend :  n (x y1 y2 : A),
    {n} x  x {n} y1  y2 
714
     z1 z2, x  z1  z2  z1 {n} y1  z2 {n} y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
715
  Lemma cmra_total_mixin : CMRAMixin A.
716
  Proof using Type*.
Robbert Krebbers's avatar
Robbert Krebbers committed
717 718 719 720 721 722
    split; auto.
    - intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
      case (total y)=> [cy ->]; eauto.
    - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
    - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
      case (total cx)=>[ccx ->]; by constructor.
723
    - intros x y cx Hxy%core_mono Hx. move: Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
724 725 726
      rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
  Qed.
End cmra_total.