cmra.v 59.6 KB
Newer Older
 Robbert Krebbers committed Mar 24, 2017 1 ``````From iris.algebra Require Export ofe monoid. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Feb 01, 2016 3 `````` `````` Robbert Krebbers committed May 28, 2016 4 ``````Class PCore (A : Type) := pcore : A → option A. `````` Robbert Krebbers committed Sep 17, 2017 5 ``````Hint Mode PCore ! : typeclass_instances. `````` Robbert Krebbers committed May 28, 2016 6 ``````Instance: Params (@pcore) 2. `````` Robbert Krebbers committed Feb 01, 2016 7 8 `````` Class Op (A : Type) := op : A → A → A. `````` Robbert Krebbers committed Sep 17, 2017 9 ``````Hint Mode Op ! : typeclass_instances. `````` Robbert Krebbers committed Feb 01, 2016 10 11 12 13 ``````Instance: Params (@op) 2. Infix "⋅" := op (at level 50, left associativity) : C_scope. Notation "(⋅)" := op (only parsing) : C_scope. `````` Ralf Jung committed Jun 23, 2016 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 *) `````` Robbert Krebbers committed Feb 01, 2016 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. `````` Robbert Krebbers committed Feb 13, 2016 22 ``````Hint Extern 0 (_ ≼ _) => reflexivity. `````` Robbert Krebbers committed Feb 01, 2016 23 24 ``````Instance: Params (@included) 3. `````` Robbert Krebbers committed Nov 11, 2015 25 ``````Class ValidN (A : Type) := validN : nat → A → Prop. `````` Robbert Krebbers committed Sep 17, 2017 26 ``````Hint Mode ValidN ! : typeclass_instances. `````` Robbert Krebbers committed Nov 11, 2015 27 ``````Instance: Params (@validN) 3. `````` Robbert Krebbers committed Feb 11, 2016 28 ``````Notation "✓{ n } x" := (validN n x) `````` Robbert Krebbers committed Feb 19, 2016 29 `````` (at level 20, n at next level, format "✓{ n } x"). `````` Robbert Krebbers committed Nov 11, 2015 30 `````` `````` Robbert Krebbers committed Feb 01, 2016 31 ``````Class Valid (A : Type) := valid : A → Prop. `````` Robbert Krebbers committed Sep 17, 2017 32 ``````Hint Mode Valid ! : typeclass_instances. `````` Robbert Krebbers committed Feb 01, 2016 33 ``````Instance: Params (@valid) 2. `````` Robbert Krebbers committed Feb 11, 2016 34 ``````Notation "✓ x" := (valid x) (at level 20) : C_scope. `````` Robbert Krebbers committed Feb 01, 2016 35 `````` `````` Ralf Jung committed Feb 10, 2016 36 ``````Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. `````` Robbert Krebbers committed Nov 20, 2015 37 ``````Notation "x ≼{ n } y" := (includedN n x y) `````` Robbert Krebbers committed Feb 19, 2016 38 `````` (at level 70, n at next level, format "x ≼{ n } y") : C_scope. `````` Robbert Krebbers committed Nov 20, 2015 39 ``````Instance: Params (@includedN) 4. `````` Robbert Krebbers committed Feb 13, 2016 40 ``````Hint Extern 0 (_ ≼{_} _) => reflexivity. `````` Robbert Krebbers committed Nov 20, 2015 41 `````` `````` Ralf Jung committed Oct 10, 2017 42 43 ``````Section mixin. Local Set Primitive Projections. `````` Robbert Krebbers committed Oct 25, 2017 44 `````` Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { `````` Ralf Jung committed Oct 10, 2017 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 `````` (* setoids *) mixin_cmra_op_ne (x : A) : NonExpansive (op x); mixin_cmra_pcore_ne n x y cx : 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 *) mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; (* monoid *) mixin_cmra_assoc : Assoc (≡) (⋅); mixin_cmra_comm : Comm (≡) (⋅); 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; mixin_cmra_pcore_mono x y cx : x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy; mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; mixin_cmra_extend n x y1 y2 : ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 }. End mixin. `````` Robbert Krebbers committed Nov 22, 2015 66 `````` `````` Robbert Krebbers committed Nov 11, 2015 67 ``````(** Bundeled version *) `````` Robbert Krebbers committed Oct 25, 2017 68 ``````Structure cmraT := CmraT' { `````` Robbert Krebbers committed Nov 11, 2015 69 70 71 `````` cmra_car :> Type; cmra_equiv : Equiv cmra_car; cmra_dist : Dist cmra_car; `````` Robbert Krebbers committed May 28, 2016 72 `````` cmra_pcore : PCore cmra_car; `````` Robbert Krebbers committed Nov 11, 2015 73 `````` cmra_op : Op cmra_car; `````` Robbert Krebbers committed Feb 24, 2016 74 `````` cmra_valid : Valid cmra_car; `````` Robbert Krebbers committed Nov 11, 2015 75 `````` cmra_validN : ValidN cmra_car; `````` Ralf Jung committed Nov 22, 2016 76 `````` cmra_ofe_mixin : OfeMixin cmra_car; `````` Robbert Krebbers committed Oct 25, 2017 77 `````` cmra_mixin : CmraMixin cmra_car; `````` Robbert Krebbers committed Jun 15, 2016 78 `````` _ : Type `````` Robbert Krebbers committed Nov 11, 2015 79 ``````}. `````` Robbert Krebbers committed Oct 25, 2017 80 81 ``````Arguments CmraT' _ {_ _ _ _ _ _} _ _ _. (* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart `````` Robbert Krebbers committed Feb 09, 2017 82 83 ``````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. *) `````` Robbert Krebbers committed Oct 25, 2017 84 ``````Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m A) (only parsing). `````` Robbert Krebbers committed Feb 09, 2017 85 `````` `````` Robbert Krebbers committed Jan 14, 2016 86 87 88 ``````Arguments cmra_car : simpl never. Arguments cmra_equiv : simpl never. Arguments cmra_dist : simpl never. `````` Robbert Krebbers committed May 28, 2016 89 ``````Arguments cmra_pcore : simpl never. `````` Robbert Krebbers committed Jan 14, 2016 90 ``````Arguments cmra_op : simpl never. `````` Robbert Krebbers committed Feb 24, 2016 91 ``````Arguments cmra_valid : simpl never. `````` Robbert Krebbers committed Jan 14, 2016 92 ``````Arguments cmra_validN : simpl never. `````` Ralf Jung committed Nov 22, 2016 93 ``````Arguments cmra_ofe_mixin : simpl never. `````` Robbert Krebbers committed Jan 14, 2016 94 ``````Arguments cmra_mixin : simpl never. `````` Robbert Krebbers committed Nov 11, 2015 95 ``````Add Printing Constructor cmraT. `````` Robbert Krebbers committed Jun 14, 2016 96 97 98 99 ``````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. `````` Ralf Jung committed Nov 22, 2016 100 101 ``````Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A). Canonical Structure cmra_ofeC. `````` Robbert Krebbers committed Nov 11, 2015 102 `````` `````` Robbert Krebbers committed Oct 25, 2017 103 ``````Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac. `````` Robbert Krebbers committed Feb 09, 2017 104 105 106 ``````Notation cmra_mixin_of A := ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing). `````` Robbert Krebbers committed Jan 14, 2016 107 108 109 110 ``````(** Lifting properties from the mixin *) Section cmra_mixin. Context {A : cmraT}. Implicit Types x y : A. `````` Ralf Jung committed Jan 27, 2017 111 `````` Global Instance cmra_op_ne (x : A) : NonExpansive (op x). `````` Robbert Krebbers committed Jan 14, 2016 112 `````` Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed May 28, 2016 113 114 115 `````` 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. `````` Robbert Krebbers committed Feb 01, 2016 116 117 `````` Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n). Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 24, 2016 118 119 `````` Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x. Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 01, 2016 120 121 `````` Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x. Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 11, 2016 122 123 124 125 `````` 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 committed May 28, 2016 126 127 128 129 `````` 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. `````` Ralf Jung committed Jul 25, 2016 130 `````` Lemma cmra_pcore_mono x y cx : `````` Robbert Krebbers committed May 28, 2016 131 `````` x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy. `````` Ralf Jung committed Jul 25, 2016 132 `````` Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 01, 2016 133 134 `````` Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x. Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 24, 2016 135 `````` Lemma cmra_extend n x y1 y2 : `````` Ralf Jung committed Feb 10, 2016 136 `````` ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → `````` Robbert Krebbers committed Aug 14, 2016 137 `````` ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2. `````` Robbert Krebbers committed Feb 24, 2016 138 `````` Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Jan 14, 2016 139 140 ``````End cmra_mixin. `````` Robbert Krebbers committed May 28, 2016 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. `````` Robbert Krebbers committed Oct 25, 2017 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. Instance: Params (@CoreId) 1. `````` Robbert Krebbers committed May 28, 2016 150 `````` `````` Jacques-Henri Jourdan committed May 31, 2016 151 ``````(** * Exclusive elements (i.e., elements that cannot have a frame). *) `````` Robbert Krebbers committed Jun 16, 2016 152 153 ``````Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False. Arguments exclusive0_l {_} _ {_} _ _. `````` Robbert Krebbers committed Jan 22, 2017 154 ``````Hint Mode Exclusive + ! : typeclass_instances. `````` Robbert Krebbers committed Feb 11, 2017 155 ``````Instance: Params (@Exclusive) 1. `````` Jacques-Henri Jourdan committed May 31, 2016 156 `````` `````` Jacques-Henri Jourdan committed Feb 01, 2017 157 158 159 160 161 ``````(** * 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. `````` Robbert Krebbers committed Feb 11, 2017 162 ``````Instance: Params (@Cancelable) 1. `````` Jacques-Henri Jourdan committed Feb 01, 2017 163 164 165 166 167 168 `````` (** * 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. `````` Robbert Krebbers committed Feb 11, 2017 169 ``````Instance: Params (@IdFree) 1. `````` Jacques-Henri Jourdan committed Feb 01, 2017 170 `````` `````` Robbert Krebbers committed May 28, 2016 171 172 173 ``````(** * CMRAs whose core is total *) (** The function [core] may return a dummy when used on CMRAs without total core. *) `````` Robbert Krebbers committed Oct 25, 2017 174 175 ``````Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x). Hint Mode CmraTotal ! : typeclass_instances. `````` Robbert Krebbers committed May 28, 2016 176 177 `````` Class Core (A : Type) := core : A → A. `````` Robbert Krebbers committed Sep 17, 2017 178 ``````Hint Mode Core ! : typeclass_instances. `````` Robbert Krebbers committed May 28, 2016 179 180 181 182 183 ``````Instance: Params (@core) 2. Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x). Arguments core' _ _ _ /. `````` Ralf Jung committed Mar 08, 2016 184 ``````(** * CMRAs with a unit element *) `````` Robbert Krebbers committed Sep 17, 2017 185 186 187 ``````Class Unit (A : Type) := ε : A. Arguments ε {_ _}. `````` Robbert Krebbers committed Oct 25, 2017 188 ``````Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := { `````` Robbert Krebbers committed Sep 17, 2017 189 190 191 `````` mixin_ucmra_unit_valid : ✓ ε; mixin_ucmra_unit_left_id : LeftId (≡) ε (⋅); mixin_ucmra_pcore_unit : pcore ε ≡ Some ε `````` Robbert Krebbers committed Feb 01, 2016 192 ``````}. `````` Robbert Krebbers committed May 27, 2016 193 `````` `````` Robbert Krebbers committed Oct 25, 2017 194 ``````Structure ucmraT := UcmraT' { `````` Robbert Krebbers committed May 27, 2016 195 196 197 `````` ucmra_car :> Type; ucmra_equiv : Equiv ucmra_car; ucmra_dist : Dist ucmra_car; `````` Robbert Krebbers committed May 28, 2016 198 `````` ucmra_pcore : PCore ucmra_car; `````` Robbert Krebbers committed May 27, 2016 199 200 201 `````` ucmra_op : Op ucmra_car; ucmra_valid : Valid ucmra_car; ucmra_validN : ValidN ucmra_car; `````` Robbert Krebbers committed Sep 17, 2017 202 `````` ucmra_unit : Unit ucmra_car; `````` Ralf Jung committed Nov 22, 2016 203 `````` ucmra_ofe_mixin : OfeMixin ucmra_car; `````` Robbert Krebbers committed Oct 25, 2017 204 205 `````` ucmra_cmra_mixin : CmraMixin ucmra_car; ucmra_mixin : UcmraMixin ucmra_car; `````` Robbert Krebbers committed Jun 15, 2016 206 `````` _ : Type; `````` Robbert Krebbers committed May 27, 2016 207 ``````}. `````` Robbert Krebbers committed Oct 25, 2017 208 209 210 ``````Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _ _. Notation UcmraT A m := (UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing). `````` Robbert Krebbers committed May 27, 2016 211 212 213 ``````Arguments ucmra_car : simpl never. Arguments ucmra_equiv : simpl never. Arguments ucmra_dist : simpl never. `````` Robbert Krebbers committed May 28, 2016 214 ``````Arguments ucmra_pcore : simpl never. `````` Robbert Krebbers committed May 27, 2016 215 216 217 ``````Arguments ucmra_op : simpl never. Arguments ucmra_valid : simpl never. Arguments ucmra_validN : simpl never. `````` Ralf Jung committed Nov 22, 2016 218 ``````Arguments ucmra_ofe_mixin : simpl never. `````` Robbert Krebbers committed May 27, 2016 219 220 221 ``````Arguments ucmra_cmra_mixin : simpl never. Arguments ucmra_mixin : simpl never. Add Printing Constructor ucmraT. `````` Robbert Krebbers committed Sep 17, 2017 222 ``````Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances. `````` Ralf Jung committed Nov 22, 2016 223 224 ``````Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A). Canonical Structure ucmra_ofeC. `````` Robbert Krebbers committed May 27, 2016 225 ``````Coercion ucmra_cmraR (A : ucmraT) : cmraT := `````` Robbert Krebbers committed Oct 25, 2017 226 `````` CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A. `````` Robbert Krebbers committed May 27, 2016 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. `````` Robbert Krebbers committed Sep 17, 2017 233 `````` Lemma ucmra_unit_valid : ✓ (ε : A). `````` Robbert Krebbers committed May 27, 2016 234 `````` Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed. `````` Robbert Krebbers committed Sep 17, 2017 235 `````` Global Instance ucmra_unit_left_id : LeftId (≡) ε (@op A _). `````` Robbert Krebbers committed May 27, 2016 236 `````` Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed. `````` Robbert Krebbers committed Sep 17, 2017 237 `````` Lemma ucmra_pcore_unit : pcore (ε:A) ≡ Some ε. `````` Robbert Krebbers committed May 28, 2016 238 `````` Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed. `````` Robbert Krebbers committed May 27, 2016 239 ``````End ucmra_mixin. `````` Robbert Krebbers committed Jan 14, 2016 240 `````` `````` Robbert Krebbers committed Feb 24, 2016 241 ``````(** * Discrete CMRAs *) `````` Robbert Krebbers committed Oct 25, 2017 242 243 ``````Class CmraDiscrete (A : cmraT) := { cmra_discrete_ofe_discrete :> OfeDiscrete A; `````` Robbert Krebbers committed Feb 24, 2016 244 245 `````` cmra_discrete_valid (x : A) : ✓{0} x → ✓ x }. `````` Robbert Krebbers committed Oct 25, 2017 246 ``````Hint Mode CmraDiscrete ! : typeclass_instances. `````` Robbert Krebbers committed Feb 24, 2016 247 `````` `````` Robbert Krebbers committed Jan 16, 2016 248 ``````(** * Morphisms *) `````` Robbert Krebbers committed Oct 25, 2017 249 ``````Class CmraMorphism {A B : cmraT} (f : A → B) := { `````` 250 251 252 253 `````` 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) `````` Robbert Krebbers committed Jan 14, 2016 254 ``````}. `````` 255 256 257 ``````Arguments cmra_morphism_validN {_ _} _ {_} _ _ _. Arguments cmra_morphism_pcore {_ _} _ {_} _. Arguments cmra_morphism_op {_ _} _ {_} _ _. `````` Robbert Krebbers committed Jan 14, 2016 258 `````` `````` Robbert Krebbers committed Jan 16, 2016 259 ``````(** * Properties **) `````` Robbert Krebbers committed Nov 11, 2015 260 ``````Section cmra. `````` Robbert Krebbers committed Jan 14, 2016 261 ``````Context {A : cmraT}. `````` Robbert Krebbers committed Nov 11, 2015 262 ``````Implicit Types x y z : A. `````` Robbert Krebbers committed Feb 01, 2016 263 ``````Implicit Types xs ys zs : list A. `````` Robbert Krebbers committed Nov 11, 2015 264 `````` `````` Robbert Krebbers committed Feb 01, 2016 265 ``````(** ** Setoids *) `````` Ralf Jung committed Jan 27, 2017 266 ``````Global Instance cmra_pcore_ne' : NonExpansive (@pcore A _). `````` Robbert Krebbers committed May 28, 2016 267 ``````Proof. `````` Ralf Jung committed Jan 27, 2017 268 `````` intros n x y Hxy. destruct (pcore x) as [cx|] eqn:?. `````` Robbert Krebbers committed May 28, 2016 269 270 271 272 273 274 `````` { 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. `````` Robbert Krebbers committed Feb 01, 2016 275 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 276 277 278 `````` 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. `````` Robbert Krebbers committed Feb 01, 2016 279 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 280 281 ``````Global Instance cmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _). Proof. apply (ne_proper _). Qed. `````` Ralf Jung committed Jan 27, 2017 282 283 ``````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. `````` Robbert Krebbers committed Sep 28, 2016 284 ``````Global Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _). `````` Robbert Krebbers committed Feb 01, 2016 285 286 287 288 289 290 291 ``````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 _). `````` Robbert Krebbers committed Feb 24, 2016 292 293 294 295 ``````Proof. intros x y Hxy; rewrite !cmra_valid_validN. by split=> ? n; [rewrite -Hxy|rewrite Hxy]. Qed. `````` Robbert Krebbers committed Feb 01, 2016 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 ``````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. `````` Ralf Jung committed Jan 27, 2017 314 ``````Global Instance cmra_opM_ne : NonExpansive2 (@opM A). `````` Robbert Krebbers committed Feb 09, 2017 315 ``````Proof. destruct 2; by ofe_subst. Qed. `````` Robbert Krebbers committed May 28, 2016 316 317 ``````Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A). Proof. destruct 2; by setoid_subst. Qed. `````` Robbert Krebbers committed Feb 01, 2016 318 `````` `````` Robbert Krebbers committed Oct 25, 2017 319 ``````Global Instance CoreId_proper : Proper ((≡) ==> iff) (@CoreId A). `````` Robbert Krebbers committed Feb 11, 2017 320 321 322 323 324 325 326 327 ``````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 committed May 28, 2016 328 329 330 331 ``````(** ** Op *) Lemma cmra_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz). Proof. destruct mz; by rewrite /= -?assoc. Qed. `````` Robbert Krebbers committed Feb 01, 2016 332 ``````(** ** Validity *) `````` Robbert Krebbers committed Feb 18, 2016 333 ``````Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x. `````` Robbert Krebbers committed Feb 01, 2016 334 335 336 ``````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 committed Feb 18, 2016 337 ``````Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y. `````` Robbert Krebbers committed Feb 11, 2016 338 ``````Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 339 340 341 ``````Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y. Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed. `````` Ralf Jung committed Mar 08, 2016 342 ``````(** ** Core *) `````` Robbert Krebbers committed May 28, 2016 343 344 345 ``````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. `````` Jacques-Henri Jourdan committed Feb 01, 2017 346 ``````Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed. `````` Robbert Krebbers committed May 28, 2016 347 ``````Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x. `````` Jacques-Henri Jourdan committed Feb 01, 2017 348 ``````Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed. `````` Robbert Krebbers committed May 28, 2016 349 ``````Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx. `````` Jacques-Henri Jourdan committed Feb 01, 2017 350 ``````Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed. `````` Robbert Krebbers committed May 30, 2016 351 352 353 354 ``````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 committed May 28, 2016 355 356 357 358 359 360 361 362 ``````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. `````` Robbert Krebbers committed Feb 01, 2016 363 `````` `````` Robbert Krebbers committed Oct 25, 2017 364 365 ``````(** ** CoreId elements *) Lemma core_id_dup x `{!CoreId x} : x ≡ x ⋅ x. `````` Robbert Krebbers committed May 30, 2016 366 367 ``````Proof. by apply cmra_pcore_dup' with x. Qed. `````` Jacques-Henri Jourdan committed May 31, 2016 368 ``````(** ** Exclusive elements *) `````` Robbert Krebbers committed Jun 16, 2016 369 ``````Lemma exclusiveN_l n x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False. `````` Robbert Krebbers committed Aug 30, 2016 370 ``````Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed. `````` Robbert Krebbers committed Jun 16, 2016 371 372 373 374 375 376 ``````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. `````` Robbert Krebbers committed Jun 16, 2016 377 ``````Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None. `````` Robbert Krebbers committed Aug 30, 2016 378 ``````Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed. `````` Robbert Krebbers committed Oct 02, 2016 379 380 381 382 ``````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. `````` Jacques-Henri Jourdan committed May 31, 2016 383 `````` `````` Robbert Krebbers committed Feb 01, 2016 384 ``````(** ** Order *) `````` Robbert Krebbers committed Mar 11, 2016 385 386 ``````Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y. Proof. intros [z ->]. by exists z. Qed. `````` Robbert Krebbers committed May 28, 2016 387 ``````Global Instance cmra_includedN_trans n : Transitive (@includedN A _ _ n). `````` Robbert Krebbers committed Feb 01, 2016 388 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 389 `````` intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz. `````` Robbert Krebbers committed Feb 01, 2016 390 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 391 ``````Global Instance cmra_included_trans: Transitive (@included A _ _). `````` Robbert Krebbers committed Feb 01, 2016 392 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 393 `````` intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz. `````` Robbert Krebbers committed Feb 01, 2016 394 ``````Qed. `````` Robbert Krebbers committed Sep 09, 2016 395 396 ``````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 committed Feb 18, 2016 397 ``````Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x. `````` Robbert Krebbers committed Feb 09, 2017 398 ``````Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 18, 2016 399 ``````Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x. `````` Robbert Krebbers committed Mar 11, 2016 400 ``````Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 401 `````` `````` Robbert Krebbers committed Feb 18, 2016 402 ``````Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y. `````` Robbert Krebbers committed Feb 01, 2016 403 ``````Proof. by intros [z Hz]; exists z; apply dist_S. Qed. `````` Robbert Krebbers committed Feb 18, 2016 404 ``````Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y. `````` Robbert Krebbers committed Feb 01, 2016 405 406 407 408 409 410 411 ``````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. `````` Robbert Krebbers committed Feb 11, 2016 412 ``````Proof. rewrite (comm op); apply cmra_includedN_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 413 ``````Lemma cmra_included_r x y : y ≼ x ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 414 ``````Proof. rewrite (comm op); apply cmra_included_l. Qed. `````` Robbert Krebbers committed Nov 20, 2015 415 `````` `````` Ralf Jung committed Jul 25, 2016 416 ``````Lemma cmra_pcore_mono' x y cx : `````` Robbert Krebbers committed May 28, 2016 417 418 419 `````` x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy. Proof. intros ? (cx'&?&Hcx)%equiv_Some_inv_r'. `````` Ralf Jung committed Jul 25, 2016 420 `````` destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto. `````` Robbert Krebbers committed May 28, 2016 421 422 `````` exists cy; by rewrite Hcx. Qed. `````` Ralf Jung committed Jul 25, 2016 423 ``````Lemma cmra_pcore_monoN' n x y cx : `````` Robbert Krebbers committed May 28, 2016 424 `````` x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy. `````` Robbert Krebbers committed Feb 26, 2016 425 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 426 `````` intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'. `````` Ralf Jung committed Jul 25, 2016 427 `````` destruct (cmra_pcore_mono x (x ⋅ z) cx') `````` Robbert Krebbers committed May 28, 2016 428 429 430 431 432 `````` 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 committed Feb 26, 2016 433 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 434 435 ``````Lemma cmra_included_pcore x cx : pcore x = Some cx → cx ≼ x. Proof. exists x. by rewrite cmra_pcore_l. Qed. `````` Robbert Krebbers committed Sep 27, 2016 436 `````` `````` Ralf Jung committed Jul 25, 2016 437 ``````Lemma cmra_monoN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 438 ``````Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. `````` Ralf Jung committed Jul 25, 2016 439 ``````Lemma cmra_mono_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 440 ``````Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. `````` Ralf Jung committed Jul 25, 2016 441 442 443 444 ``````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. `````` Robbert Krebbers committed Sep 27, 2016 445 446 447 448 ``````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. `````` Robbert Krebbers committed Feb 01, 2016 449 `````` `````` Robbert Krebbers committed Sep 28, 2016 450 451 452 453 454 455 456 ``````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 committed Feb 18, 2016 457 ``````Lemma cmra_included_dist_l n x1 x2 x1' : `````` Ralf Jung committed Feb 10, 2016 458 `````` x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. `````` Robbert Krebbers committed Nov 11, 2015 459 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 460 461 `````` intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l. by rewrite Hx1 Hx2. `````` Robbert Krebbers committed Nov 11, 2015 462 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 463 `````` `````` Robbert Krebbers committed May 28, 2016 464 465 ``````(** ** Total core *) Section total_core. `````` Ralf Jung committed Jan 25, 2017 466 `````` Local Set Default Proof Using "Type*". `````` Robbert Krebbers committed Oct 25, 2017 467 `````` Context `{CmraTotal A}. `````` Robbert Krebbers committed May 28, 2016 468 469 470 471 472 473 474 475 476 `````` 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. `````` Ralf Jung committed Jul 25, 2016 477 `````` Lemma cmra_core_mono x y : x ≼ y → core x ≼ core y. `````` Robbert Krebbers committed May 28, 2016 478 479 `````` Proof. intros; destruct (cmra_total x) as [cx Hcx]. `````` Ralf Jung committed Jul 25, 2016 480 `````` destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto. `````` Robbert Krebbers committed May 28, 2016 481 482 483 `````` by rewrite /core /= Hcx Hcy. Qed. `````` Ralf Jung committed Jan 27, 2017 484 `````` Global Instance cmra_core_ne : NonExpansive (@core A _). `````` Robbert Krebbers committed May 28, 2016 485 `````` Proof. `````` Ralf Jung committed Jan 27, 2017 486 `````` intros n x y Hxy. destruct (cmra_total x) as [cx Hcx]. `````` Robbert Krebbers committed May 28, 2016 487 488 489 490 491 492 493 `````` 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. `````` Robbert Krebbers committed May 30, 2016 494 495 `````` 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 committed May 28, 2016 496 497 498 499 500 `````` 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. `````` Robbert Krebbers committed Oct 25, 2017 501 `````` Lemma core_id_total x : CoreId x ↔ core x ≡ x. `````` Robbert Krebbers committed May 28, 2016 502 `````` Proof. `````` Robbert Krebbers committed Oct 25, 2017 503 504 `````` split; [intros; by rewrite /core /= (core_id x)|]. rewrite /CoreId /core /=. `````` Robbert Krebbers committed May 28, 2016 505 506 `````` destruct (cmra_total x) as [? ->]. by constructor. Qed. `````` Robbert Krebbers committed Oct 25, 2017 507 508 `````` Lemma core_id_core x `{!CoreId x} : core x ≡ x. Proof. by apply core_id_total. Qed. `````` Robbert Krebbers committed May 28, 2016 509 `````` `````` Robbert Krebbers committed Oct 25, 2017 510 `````` Global Instance cmra_core_core_id x : CoreId (core x). `````` Robbert Krebbers committed May 28, 2016 511 512 `````` Proof. destruct (cmra_total x) as [cx Hcx]. `````` Robbert Krebbers committed Oct 25, 2017 513 `````` rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp. `````` Robbert Krebbers committed May 28, 2016 514 515 516 517 518 519 520 521 522 523 524 525 `````` 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. `````` Ralf Jung committed Jul 25, 2016 526 `````` Lemma cmra_core_monoN n x y : x ≼{n} y → core x ≼{n} core y. `````` Robbert Krebbers committed May 28, 2016 527 528 `````` Proof. intros [z ->]. `````` Ralf Jung committed Jul 25, 2016 529 `````` apply cmra_included_includedN, cmra_core_mono, cmra_included_l. `````` Robbert Krebbers committed May 28, 2016 530 531 532 `````` Qed. End total_core. `````` Robbert Krebbers committed Oct 25, 2017 533 534 ``````(** ** Discrete *) Lemma cmra_discrete_included_l x y : Discrete x → ✓{0} y → x ≼{0} y → x ≼ y. `````` Robbert Krebbers committed Dec 11, 2015 535 536 ``````Proof. intros ?? [x' ?]. `````` Robbert Krebbers committed Aug 14, 2016 537 `````` destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *. `````` Robbert Krebbers committed Oct 25, 2017 538 `````` by exists z'; rewrite Hy (discrete x z). `````` Robbert Krebbers committed Dec 11, 2015 539 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 540 541 542 543 ``````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 committed Nov 18, 2015 544 545 ``````Proof. intros ??? z Hz. `````` Robbert Krebbers committed Aug 14, 2016 546 `````` destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *. `````` Robbert Krebbers committed Feb 24, 2016 547 `````` { rewrite -?Hz. by apply cmra_valid_validN. } `````` Robbert Krebbers committed Oct 25, 2017 548 `````` by rewrite Hz' (discrete x1 y1) // (discrete x2 y2). `````` Robbert Krebbers committed Nov 18, 2015 549 ``````Qed. `````` Robbert Krebbers committed Nov 20, 2015 550 `````` `````` Robbert Krebbers committed Feb 24, 2016 551 ``````(** ** Discrete *) `````` Robbert Krebbers committed Oct 25, 2017 552 ``````Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x : ✓ x ↔ ✓{n} x. `````` Robbert Krebbers committed Feb 24, 2016 553 554 555 556 ``````Proof. split; first by rewrite cmra_valid_validN. eauto using cmra_discrete_valid, cmra_validN_le with lia. Qed. `````` Robbert Krebbers committed Oct 25, 2017 557 ``````Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y. `````` Robbert Krebbers committed Feb 24, 2016 558 ``````Proof. `````` Robbert Krebbers committed Mar 11, 2016 559 `````` split; first by apply cmra_included_includedN. `````` Robbert Krebbers committed Oct 25, 2017 560 `````` intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l. `````` Robbert Krebbers committed Feb 24, 2016 561 ``````Qed. `````` Jacques-Henri Jourdan committed Feb 01, 2017 562 563 564 `````` (** Cancelable elements *) Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A). `````` Robbert Krebbers committed Feb 03, 2017 565 566 ``````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. `````` Jacques-Henri Jourdan committed Feb 01, 2017 567 ``````Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed. `````` Robbert Krebbers committed Oct 25, 2017 568 ``````Lemma discrete_cancelable x `{CmraDiscrete A}: `````` Jacques-Henri Jourdan committed Feb 01, 2017 569 `````` (∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x. `````` Robbert Krebbers committed Oct 25, 2017 570 ``````Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed. `````` Jacques-Henri Jourdan committed Feb 01, 2017 571 572 573 ``````Global Instance cancelable_op x y : Cancelable x → Cancelable y → Cancelable (x ⋅ y). Proof. `````` Robbert Krebbers committed Feb 03, 2017 574 `````` intros ?? n z z' ??. apply (cancelableN y), (cancelableN x). `````` Jacques-Henri Jourdan committed Feb 01, 2017 575 576 577 578 579 `````` - 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. `````` Robbert Krebbers committed Feb 03, 2017 580 ``````Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed. `````` Jacques-Henri Jourdan committed Feb 01, 2017 581 582 `````` (** Id-free elements *) `````` Robbert Krebbers committed Feb 03, 2017 583 ``````Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A). `````` Jacques-Henri Jourdan committed Feb 01, 2017 584 ``````Proof. `````` Robbert Krebbers committed Feb 03, 2017 585 586 `````` intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree. split=> y ?; (rewrite -EQ || rewrite EQ); eauto. `````` Jacques-Henri Jourdan committed Feb 01, 2017 587 588 ``````Qed. Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A). `````` Robbert Krebbers committed Feb 03, 2017 589 ``````Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed. `````` Jacques-Henri Jourdan committed Feb 01, 2017 590 591 592 593 594 595 596 597 ``````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. `````` Robbert Krebbers committed Oct 25, 2017 598 ``````Lemma discrete_id_free x `{CmraDiscrete A}: `````` Robbert Krebbers committed Feb 03, 2017 599 `````` (∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x. `````` Robbert Krebbers committed Oct 25, 2017 600 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2017 601 `````` intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid. `````` Robbert Krebbers committed Oct 25, 2017 602 ``````Qed. `````` Robbert Krebbers committed Feb 03, 2017 603 ``````Global Instance id_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y). `````` Jacques-Henri Jourdan committed Feb 01, 2017 604 ``````Proof. `````` Robbert Krebbers committed Feb 03, 2017 605 `````` intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?. `````` Jacques-Henri Jourdan committed Feb 01, 2017 606 607 `````` eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto]. Qed. `````` Robbert Krebbers committed Feb 03, 2017 608 ``````Global Instance id_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y). `````` Jacques-Henri Jourdan committed Feb 01, 2017 609 610 611 ``````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 committed Nov 11, 2015 612 613 ``````End cmra. `````` Robbert Krebbers committed May 27, 2016 614 615 ``````(** * Properties about CMRAs with a unit element **) Section ucmra. `````` Robbert Krebbers committed May 28, 2016 616 617 618 `````` Context {A : ucmraT}. Implicit Types x y z : A. `````` Robbert Krebbers committed Sep 17, 2017 619 `````` Lemma ucmra_unit_validN n : ✓{n} (ε:A). `````` Robbert Krebbers committed May 28, 2016 620 `````` Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed. `````` Robbert Krebbers committed Sep 17, 2017 621 `````` Lemma ucmra_unit_leastN n x : ε ≼{n} x. `````` Robbert Krebbers committed May 28, 2016 622 `````` Proof. by exists x; rewrite left_id. Qed. `````` Robbert Krebbers committed Sep 17, 2017 623 `````` Lemma ucmra_unit_least x : ε ≼ x. `````` Robbert Krebbers committed May 28, 2016 624 `````` Proof. by exists x; rewrite left_id. Qed. `````` Robbert Krebbers committed Sep 17, 2017 625 `````` Global Instance ucmra_unit_right_id : RightId (≡) ε (@op A _). `````` Robbert Krebbers committed May 28, 2016 626 `````` Proof. by intros x; rewrite (comm op) left_id. Qed. `````` Robbert Krebbers committed Oct 25, 2017 627 `````` Global Instance ucmra_unit_core_id : CoreId (ε:A). `````` Robbert Krebbers committed May 28, 2016 628 629 `````` Proof. apply ucmra_pcore_unit. Qed. `````` Robbert Krebbers committed Oct 25, 2017 630 `````` Global Instance cmra_unit_cmra_total : CmraTotal A. `````` Robbert Krebbers committed May 28, 2016 631 `````` Proof. `````` Robbert Krebbers committed Sep 17, 2017 632 `````` intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?); `````` Robbert Krebbers committed Oct 25, 2017 633 `````` eauto using ucmra_unit_least, (core_id (ε:A)). `````` Robbert Krebbers committed May 28, 2016 634 `````` Qed. `````` Robbert Krebbers committed Sep 17, 2017 635 `````` Global Instance empty_cancelable : Cancelable (ε:A). `````` Jacques-Henri Jourdan committed Feb 01, 2017 636 `````` Proof. intros ???. by rewrite !left_id. Qed. `````` Robbert Krebbers committed Mar 24, 2017 637 638 `````` (* For big ops *) `````` Robbert Krebbers committed Sep 17, 2017 639 `````` Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}. `````` Robbert Krebbers committed May 27, 2016 640 ``````End ucmra. `````` Robbert Krebbers committed May 28, 2016 641 `````` `````` Robbert Krebbers committed Oct 25, 2017 642 ``````Hint Immediate cmra_unit_cmra_total. `````` Robbert Krebbers committed Sep 01, 2016 643 644 645 `````` (** * Properties about CMRAs with Leibniz equality *) Section cmra_leibniz. `````` Ralf Jung committed Jan 25, 2017 646 `````` Local Set Default Proof Using "Type*". `````` Robbert Krebbers committed Sep 01, 2016 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 `````` 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. `````` Robbert Krebbers committed Oct 25, 2017 669 670 671 `````` (** ** CoreId elements *) Lemma core_id_dup_L x `{!CoreId x} : x = x ⋅ x. Proof. unfold_leibniz. by apply core_id_dup. Qed. `````` Robbert Krebbers committed Sep 01, 2016 672 673 674 `````` (** ** Total core *) Section total_core. `````` Robbert Krebbers committed Oct 25, 2017 675 `````` Context `{CmraTotal A}. `````` Robbert Krebbers committed Sep 01, 2016 676 677 678 679 680 681 682 683 684 `````` 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. `````` Robbert Krebbers committed Oct 25, 2017 685 686 687 688 `````` Lemma core_id_total_L x : CoreId x ↔ core x = x. Proof. unfold_leibniz. apply core_id_total. Qed. Lemma core_id_core_L x `{!CoreId x} : core x = x. Proof. by apply core_id_total_L. Qed. `````` Robbert Krebbers committed Sep 01, 2016 689 690 691 692 `````` End total_core. End cmra_leibniz. Section ucmra_leibniz. `````` Ralf Jung committed Jan 25, 2017 693 `````` Local Set Default Proof Using "Type*". `````` Robbert Krebbers committed Sep 01, 2016 694 695 696 `````` Context {A : ucmraT} `{!LeibnizEquiv A}. Implicit Types x y z : A. `````` Robbert Krebbers committed Sep 17, 2017 697 `````` Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _). `````` Robbert Krebbers committed Sep 01, 2016 698 `````` Proof. intros x. unfold_leibniz. by rewrite left_id. Qed. `````` Robbert Krebbers committed Sep 17, 2017 699 `````` Global Instance ucmra_unit_right_id_L : RightId (=) ε (@op A _). `````` Robbert Krebbers committed Sep 01, 2016 700 701 702 `````` Proof. intros x. unfold_leibniz. by rewrite right_id. Qed. End ucmra_leibniz. `````` Robbert Krebbers committed May 28, 2016 703 704 705 ``````(** * Constructing a CMRA with total core *) Section cmra_total. Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}. `````` Robbert Krebbers committed Sep 17, 2017 706 707 `````` Context (total : ∀ x : A, is_Some (pcore x)). Context (op_ne : ∀ x : A, NonExpansive (op x)). `````` Ralf Jung committed Jan 27, 2017 708 `````` Context (core_ne : NonExpansive (@core A _)). `````` Robbert Krebbers committed May 28, 2016 709 710 711 712 713 714 715 `````` 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). `````` Ralf Jung committed Jul 25, 2016 716 `````` Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y). `````` Robbert Krebbers committed May 28, 2016 717 718 719 `````` 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 → `````` Robbert Krebbers committed Aug 14, 2016 720 `````` ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2). `````` Robbert Krebbers committed Oct 25, 2017 721 `````` Lemma cmra_total_mixin : CmraMixin A. `````` Ralf Jung committed Jan 25, 2017 722 `````` Proof using Type*. ``````