cmra.v 36.5 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.algebra Require Export cofe. `````` Robbert Krebbers committed Feb 01, 2016 2 `````` `````` Ralf Jung committed Mar 08, 2016 3 4 ``````Class Core (A : Type) := core : A → A. Instance: Params (@core) 2. `````` Robbert Krebbers committed Feb 01, 2016 5 6 7 8 9 10 11 12 13 `````` Class Op (A : Type) := op : A → A → A. Instance: Params (@op) 2. Infix "⋅" := op (at level 50, left associativity) : C_scope. Notation "(⋅)" := op (only parsing) : C_scope. 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 14 ``````Hint Extern 0 (_ ≼ _) => reflexivity. `````` Robbert Krebbers committed Feb 01, 2016 15 16 ``````Instance: Params (@included) 3. `````` Robbert Krebbers committed Nov 11, 2015 17 18 ``````Class ValidN (A : Type) := validN : nat → A → Prop. Instance: Params (@validN) 3. `````` Robbert Krebbers committed Feb 11, 2016 19 ``````Notation "✓{ n } x" := (validN n x) `````` Robbert Krebbers committed Feb 19, 2016 20 `````` (at level 20, n at next level, format "✓{ n } x"). `````` Robbert Krebbers committed Nov 11, 2015 21 `````` `````` Robbert Krebbers committed Feb 01, 2016 22 23 ``````Class Valid (A : Type) := valid : A → Prop. Instance: Params (@valid) 2. `````` Robbert Krebbers committed Feb 11, 2016 24 ``````Notation "✓ x" := (valid x) (at level 20) : C_scope. `````` Robbert Krebbers committed Feb 01, 2016 25 `````` `````` Ralf Jung committed Feb 10, 2016 26 ``````Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. `````` Robbert Krebbers committed Nov 20, 2015 27 ``````Notation "x ≼{ n } y" := (includedN n x y) `````` Robbert Krebbers committed Feb 19, 2016 28 `````` (at level 70, n at next level, format "x ≼{ n } y") : C_scope. `````` Robbert Krebbers committed Nov 20, 2015 29 ``````Instance: Params (@includedN) 4. `````` Robbert Krebbers committed Feb 13, 2016 30 ``````Hint Extern 0 (_ ≼{_} _) => reflexivity. `````` Robbert Krebbers committed Nov 20, 2015 31 `````` `````` Robbert Krebbers committed Mar 11, 2016 32 ``````Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := { `````` Robbert Krebbers committed Nov 11, 2015 33 `````` (* setoids *) `````` Robbert Krebbers committed Jan 14, 2016 34 `````` mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x); `````` Ralf Jung committed Mar 08, 2016 35 `````` mixin_cmra_core_ne n : Proper (dist n ==> dist n) core; `````` Robbert Krebbers committed Feb 11, 2016 36 `````` mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); `````` Robbert Krebbers committed Nov 11, 2015 37 `````` (* valid *) `````` Robbert Krebbers committed Feb 24, 2016 38 `````` mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; `````` Robbert Krebbers committed Feb 01, 2016 39 `````` mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; `````` Robbert Krebbers committed Nov 11, 2015 40 `````` (* monoid *) `````` Robbert Krebbers committed Feb 11, 2016 41 42 `````` mixin_cmra_assoc : Assoc (≡) (⋅); mixin_cmra_comm : Comm (≡) (⋅); `````` Ralf Jung committed Mar 08, 2016 43 44 45 `````` mixin_cmra_core_l x : core x ⋅ x ≡ x; mixin_cmra_core_idemp x : core (core x) ≡ core x; mixin_cmra_core_preserving x y : x ≼ y → core x ≼ core y; `````` Robbert Krebbers committed Feb 01, 2016 46 `````` mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; `````` Robbert Krebbers committed Feb 24, 2016 47 48 49 `````` mixin_cmra_extend n x y1 y2 : ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 } `````` Robbert Krebbers committed Nov 11, 2015 50 ``````}. `````` Robbert Krebbers committed Nov 22, 2015 51 `````` `````` Robbert Krebbers committed Nov 11, 2015 52 53 54 55 56 57 ``````(** Bundeled version *) Structure cmraT := CMRAT { cmra_car :> Type; cmra_equiv : Equiv cmra_car; cmra_dist : Dist cmra_car; cmra_compl : Compl cmra_car; `````` Ralf Jung committed Mar 08, 2016 58 `````` cmra_core : Core cmra_car; `````` Robbert Krebbers committed Nov 11, 2015 59 `````` cmra_op : Op cmra_car; `````` Robbert Krebbers committed Feb 24, 2016 60 `````` cmra_valid : Valid cmra_car; `````` Robbert Krebbers committed Nov 11, 2015 61 `````` cmra_validN : ValidN cmra_car; `````` Robbert Krebbers committed Jan 14, 2016 62 `````` cmra_cofe_mixin : CofeMixin cmra_car; `````` Robbert Krebbers committed Feb 24, 2016 63 `````` cmra_mixin : CMRAMixin cmra_car `````` Robbert Krebbers committed Nov 11, 2015 64 ``````}. `````` Robbert Krebbers committed May 25, 2016 65 ``````Arguments CMRAT _ {_ _ _ _ _ _ _} _ _. `````` Robbert Krebbers committed Jan 14, 2016 66 67 68 69 ``````Arguments cmra_car : simpl never. Arguments cmra_equiv : simpl never. Arguments cmra_dist : simpl never. Arguments cmra_compl : simpl never. `````` Ralf Jung committed Mar 08, 2016 70 ``````Arguments cmra_core : simpl never. `````` Robbert Krebbers committed Jan 14, 2016 71 ``````Arguments cmra_op : simpl never. `````` Robbert Krebbers committed Feb 24, 2016 72 ``````Arguments cmra_valid : simpl never. `````` Robbert Krebbers committed Jan 14, 2016 73 74 75 ``````Arguments cmra_validN : simpl never. Arguments cmra_cofe_mixin : simpl never. Arguments cmra_mixin : simpl never. `````` Robbert Krebbers committed Nov 11, 2015 76 ``````Add Printing Constructor cmraT. `````` Robbert Krebbers committed Mar 11, 2016 77 ``````Existing Instances cmra_core cmra_op cmra_valid cmra_validN. `````` Robbert Krebbers committed May 25, 2016 78 ``````Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A). `````` Robbert Krebbers committed Nov 11, 2015 79 80 ``````Canonical Structure cmra_cofeC. `````` Robbert Krebbers committed Jan 14, 2016 81 82 83 84 85 86 ``````(** Lifting properties from the mixin *) Section cmra_mixin. Context {A : cmraT}. Implicit Types x y : A. Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x). Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed. `````` Ralf Jung committed Mar 08, 2016 87 88 `````` Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _). Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 01, 2016 89 90 `````` 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 91 92 `````` 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 93 94 `````` 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 95 96 97 98 `````` 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. `````` Ralf Jung committed Mar 08, 2016 99 100 101 102 103 104 `````` Lemma cmra_core_l x : core x ⋅ x ≡ x. Proof. apply (mixin_cmra_core_l _ (cmra_mixin A)). Qed. Lemma cmra_core_idemp x : core (core x) ≡ core x. Proof. apply (mixin_cmra_core_idemp _ (cmra_mixin A)). Qed. Lemma cmra_core_preserving x y : x ≼ y → core x ≼ core y. Proof. apply (mixin_cmra_core_preserving _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 01, 2016 105 106 `````` 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 107 `````` Lemma cmra_extend n x y1 y2 : `````` Ralf Jung committed Feb 10, 2016 108 109 `````` ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }. `````` Robbert Krebbers committed Feb 24, 2016 110 `````` Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Jan 14, 2016 111 112 ``````End cmra_mixin. `````` Ralf Jung committed Mar 08, 2016 113 ``````(** * CMRAs with a unit element *) `````` Robbert Krebbers committed Feb 01, 2016 114 ``````(** We use the notation ∅ because for most instances (maps, sets, etc) the `````` Ralf Jung committed Mar 08, 2016 115 ```````empty' element is the unit. *) `````` Robbert Krebbers committed May 27, 2016 116 117 118 119 ``````Record UCMRAMixin A `{Dist A, Equiv A, Op A, Valid A, Empty A} := { mixin_ucmra_unit_valid : ✓ ∅; mixin_ucmra_unit_left_id : LeftId (≡) ∅ (⋅); mixin_ucmra_unit_timeless : Timeless ∅ `````` Robbert Krebbers committed Feb 01, 2016 120 ``````}. `````` Robbert Krebbers committed May 27, 2016 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 `````` Structure ucmraT := UCMRAT { ucmra_car :> Type; ucmra_equiv : Equiv ucmra_car; ucmra_dist : Dist ucmra_car; ucmra_compl : Compl ucmra_car; ucmra_core : Core ucmra_car; ucmra_op : Op ucmra_car; ucmra_valid : Valid ucmra_car; ucmra_validN : ValidN ucmra_car; ucmra_empty : Empty ucmra_car; ucmra_cofe_mixin : CofeMixin ucmra_car; ucmra_cmra_mixin : CMRAMixin ucmra_car; ucmra_mixin : UCMRAMixin ucmra_car }. Arguments UCMRAT _ {_ _ _ _ _ _ _ _} _ _ _. Arguments ucmra_car : simpl never. Arguments ucmra_equiv : simpl never. Arguments ucmra_dist : simpl never. Arguments ucmra_compl : simpl never. Arguments ucmra_core : simpl never. Arguments ucmra_op : simpl never. Arguments ucmra_valid : simpl never. Arguments ucmra_validN : simpl never. Arguments ucmra_cofe_mixin : simpl never. Arguments ucmra_cmra_mixin : simpl never. Arguments ucmra_mixin : simpl never. Add Printing Constructor ucmraT. Existing Instances ucmra_empty. Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A). Canonical Structure ucmra_cofeC. Coercion ucmra_cmraR (A : ucmraT) : cmraT := CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A). 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. Global Instance ucmra_unit_timeless : Timeless (∅ : A). Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed. End ucmra_mixin. `````` Robbert Krebbers committed Jan 14, 2016 167 `````` `````` Robbert Krebbers committed Mar 15, 2016 168 169 170 171 ``````(** * Persistent elements *) Class Persistent {A : cmraT} (x : A) := persistent : core x ≡ x. Arguments persistent {_} _ {_}. `````` Robbert Krebbers committed Feb 24, 2016 172 ``````(** * Discrete CMRAs *) `````` Robbert Krebbers committed Feb 26, 2016 173 ``````Class CMRADiscrete (A : cmraT) := { `````` Robbert Krebbers committed Feb 24, 2016 174 175 176 177 `````` cmra_discrete :> Discrete A; cmra_discrete_valid (x : A) : ✓{0} x → ✓ x }. `````` Robbert Krebbers committed Jan 16, 2016 178 ``````(** * Morphisms *) `````` Robbert Krebbers committed Jan 14, 2016 179 ``````Class CMRAMonotone {A B : cmraT} (f : A → B) := { `````` Robbert Krebbers committed Feb 26, 2016 180 181 182 `````` cmra_monotone_ne n :> Proper (dist n ==> dist n) f; validN_preserving n x : ✓{n} x → ✓{n} f x; included_preserving x y : x ≼ y → f x ≼ f y `````` Robbert Krebbers committed Jan 14, 2016 183 ``````}. `````` Robbert Krebbers committed Feb 26, 2016 184 185 ``````Arguments validN_preserving {_ _} _ {_} _ _ _. Arguments included_preserving {_ _} _ {_} _ _ _. `````` Robbert Krebbers committed Jan 14, 2016 186 `````` `````` Robbert Krebbers committed Feb 11, 2016 187 ``````(** * Local updates *) `````` Ralf Jung committed Feb 13, 2016 188 189 ``````(** The idea is that lemams taking this class will usually have L explicit, and leave Lv implicit - it will be inferred by the typeclass machinery. *) `````` Ralf Jung committed Feb 11, 2016 190 191 192 ``````Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := { local_update_ne n :> Proper (dist n ==> dist n) L; local_updateN n x y : Lv x → ✓{n} (x ⋅ y) → L (x ⋅ y) ≡{n}≡ L x ⋅ y `````` Robbert Krebbers committed Feb 11, 2016 193 194 195 ``````}. Arguments local_updateN {_ _} _ {_} _ _ _ _ _. `````` Robbert Krebbers committed Feb 01, 2016 196 ``````(** * Frame preserving updates *) `````` Robbert Krebbers committed Feb 18, 2016 197 ``````Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n z, `````` Robbert Krebbers committed Feb 10, 2016 198 `````` ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). `````` Robbert Krebbers committed Feb 02, 2016 199 ``````Instance: Params (@cmra_updateP) 1. `````` Ralf Jung committed Feb 03, 2016 200 ``````Infix "~~>:" := cmra_updateP (at level 70). `````` Robbert Krebbers committed Feb 18, 2016 201 ``````Definition cmra_update {A : cmraT} (x y : A) := ∀ n z, `````` Robbert Krebbers committed Feb 10, 2016 202 `````` ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). `````` Ralf Jung committed Feb 03, 2016 203 ``````Infix "~~>" := cmra_update (at level 70). `````` Robbert Krebbers committed Feb 02, 2016 204 ``````Instance: Params (@cmra_update) 1. `````` Robbert Krebbers committed Nov 22, 2015 205 `````` `````` Robbert Krebbers committed Jan 16, 2016 206 ``````(** * Properties **) `````` Robbert Krebbers committed Nov 11, 2015 207 ``````Section cmra. `````` Robbert Krebbers committed Jan 14, 2016 208 ``````Context {A : cmraT}. `````` Robbert Krebbers committed Nov 11, 2015 209 ``````Implicit Types x y z : A. `````` Robbert Krebbers committed Feb 01, 2016 210 ``````Implicit Types xs ys zs : list A. `````` Robbert Krebbers committed Nov 11, 2015 211 `````` `````` Robbert Krebbers committed Feb 01, 2016 212 ``````(** ** Setoids *) `````` Ralf Jung committed Mar 08, 2016 213 ``````Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _). `````` Robbert Krebbers committed Feb 01, 2016 214 215 216 217 ``````Proof. apply (ne_proper _). Qed. Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _). Proof. intros x1 x2 Hx y1 y2 Hy. `````` Robbert Krebbers committed Feb 11, 2016 218 `````` by rewrite Hy (comm _ x1) Hx (comm _ y2). `````` Robbert Krebbers committed Feb 01, 2016 219 220 221 222 223 224 225 226 227 ``````Qed. Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _). 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 228 229 230 231 ``````Proof. intros x y Hxy; rewrite !cmra_valid_validN. by split=> ? n; [rewrite -Hxy|rewrite Hxy]. Qed. `````` Robbert Krebbers committed Feb 01, 2016 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 ``````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. `````` Robbert Krebbers committed Feb 02, 2016 250 251 252 ``````Global Instance cmra_update_proper : Proper ((≡) ==> (≡) ==> iff) (@cmra_update A). Proof. `````` Robbert Krebbers committed Feb 18, 2016 253 `````` intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto. `````` Robbert Krebbers committed Feb 02, 2016 254 255 256 257 ``````Qed. Global Instance cmra_updateP_proper : Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A). Proof. `````` Robbert Krebbers committed Feb 18, 2016 258 `````` intros x1 x2 Hx P1 P2 HP; split=>Hup n z; `````` Robbert Krebbers committed Feb 02, 2016 259 260 `````` [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 261 262 `````` (** ** Validity *) `````` Robbert Krebbers committed Feb 18, 2016 263 ``````Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x. `````` Robbert Krebbers committed Feb 01, 2016 264 265 266 ``````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 267 ``````Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y. `````` Robbert Krebbers committed Feb 11, 2016 268 ``````Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 269 270 271 ``````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 272 273 274 275 276 277 278 279 280 ``````(** ** Core *) Lemma cmra_core_r x : x ⋅ core x ≡ x. Proof. by rewrite (comm _ x) cmra_core_l. Qed. Lemma cmra_core_core x : core x ⋅ core x ≡ core x. Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed. 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 Mar 15, 2016 281 282 ``````Global Instance cmra_core_persistent x : Persistent (core x). Proof. apply cmra_core_idemp. Qed. `````` Robbert Krebbers committed Feb 01, 2016 283 284 `````` (** ** Order *) `````` Robbert Krebbers committed Mar 11, 2016 285 286 ``````Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y. Proof. intros [z ->]. by exists z. Qed. `````` Robbert Krebbers committed Feb 01, 2016 287 288 289 ``````Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n). Proof. split. `````` Ralf Jung committed Mar 08, 2016 290 `````` - by intros x; exists (core x); rewrite cmra_core_r. `````` Robbert Krebbers committed Feb 17, 2016 291 `````` - intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). `````` Robbert Krebbers committed Feb 11, 2016 292 `````` by rewrite assoc -Hy -Hz. `````` Robbert Krebbers committed Feb 01, 2016 293 294 295 ``````Qed. Global Instance cmra_included_preorder: PreOrder (@included A _ _). Proof. `````` Robbert Krebbers committed Mar 11, 2016 296 297 298 299 `````` split. - by intros x; exists (core x); rewrite cmra_core_r. - intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz. `````` Robbert Krebbers committed Feb 01, 2016 300 ``````Qed. `````` Robbert Krebbers committed Feb 18, 2016 301 ``````Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x. `````` Robbert Krebbers committed Feb 01, 2016 302 ``````Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 18, 2016 303 ``````Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x. `````` Robbert Krebbers committed Mar 11, 2016 304 ``````Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 305 `````` `````` Robbert Krebbers committed Feb 18, 2016 306 ``````Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y. `````` Robbert Krebbers committed Feb 01, 2016 307 ``````Proof. by intros [z Hz]; exists z; apply dist_S. Qed. `````` Robbert Krebbers committed Feb 18, 2016 308 ``````Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y. `````` Robbert Krebbers committed Feb 01, 2016 309 310 311 312 313 314 315 ``````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 316 ``````Proof. rewrite (comm op); apply cmra_includedN_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 317 ``````Lemma cmra_included_r x y : y ≼ x ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 318 ``````Proof. rewrite (comm op); apply cmra_included_l. Qed. `````` Robbert Krebbers committed Nov 20, 2015 319 `````` `````` Ralf Jung committed Mar 08, 2016 320 ``````Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y. `````` Robbert Krebbers committed Feb 26, 2016 321 322 ``````Proof. intros [z ->]. `````` Ralf Jung committed Mar 08, 2016 323 `````` apply cmra_included_includedN, cmra_core_preserving, cmra_included_l. `````` Robbert Krebbers committed Feb 26, 2016 324 ``````Qed. `````` Ralf Jung committed Mar 08, 2016 325 326 ``````Lemma cmra_included_core x : core x ≼ x. Proof. by exists x; rewrite cmra_core_l. Qed. `````` Robbert Krebbers committed Feb 11, 2016 327 ``````Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 328 ``````Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. `````` Robbert Krebbers committed Feb 01, 2016 329 ``````Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 330 ``````Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. `````` Robbert Krebbers committed Feb 11, 2016 331 ``````Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z. `````` Robbert Krebbers committed Feb 11, 2016 332 ``````Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 333 ``````Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z. `````` Robbert Krebbers committed Feb 11, 2016 334 ``````Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 335 `````` `````` Robbert Krebbers committed Feb 18, 2016 336 ``````Lemma cmra_included_dist_l n x1 x2 x1' : `````` Ralf Jung committed Feb 10, 2016 337 `````` x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. `````` Robbert Krebbers committed Nov 11, 2015 338 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 339 340 `````` intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l. by rewrite Hx1 Hx2. `````` Robbert Krebbers committed Nov 11, 2015 341 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 342 `````` `````` Robbert Krebbers committed Jan 16, 2016 343 ``````(** ** Timeless *) `````` Robbert Krebbers committed Feb 10, 2016 344 ``````Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y. `````` Robbert Krebbers committed Dec 11, 2015 345 346 ``````Proof. intros ?? [x' ?]. `````` Robbert Krebbers committed Feb 24, 2016 347 `````` destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. `````` Robbert Krebbers committed Jan 13, 2016 348 `````` by exists z'; rewrite Hy (timeless x z). `````` Robbert Krebbers committed Dec 11, 2015 349 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 350 ``````Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y. `````` Robbert Krebbers committed Dec 11, 2015 351 ``````Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed. `````` Robbert Krebbers committed Jan 14, 2016 352 ``````Lemma cmra_op_timeless x1 x2 : `````` Robbert Krebbers committed Dec 11, 2015 353 `````` ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). `````` Robbert Krebbers committed Nov 18, 2015 354 355 ``````Proof. intros ??? z Hz. `````` Robbert Krebbers committed Feb 24, 2016 356 `````` destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. `````` Robbert Krebbers committed Feb 24, 2016 357 `````` { rewrite -?Hz. by apply cmra_valid_validN. } `````` Robbert Krebbers committed Jan 13, 2016 358 `````` by rewrite Hz' (timeless x1 y1) // (timeless x2 y2). `````` Robbert Krebbers committed Nov 18, 2015 359 ``````Qed. `````` Robbert Krebbers committed Nov 20, 2015 360 `````` `````` Robbert Krebbers committed Feb 24, 2016 361 362 363 364 365 366 367 368 ``````(** ** 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 committed Mar 11, 2016 369 `````` split; first by apply cmra_included_includedN. `````` Robbert Krebbers committed Feb 24, 2016 370 371 372 373 374 375 376 377 378 `````` intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l. Qed. Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A → Prop) : (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P. Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed. Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed. `````` Robbert Krebbers committed Feb 11, 2016 379 ``````(** ** Local updates *) `````` Ralf Jung committed Feb 11, 2016 380 381 ``````Global Instance local_update_proper Lv (L : A → A) : LocalUpdate Lv L → Proper ((≡) ==> (≡)) L. `````` Robbert Krebbers committed Feb 11, 2016 382 383 ``````Proof. intros; apply (ne_proper _). Qed. `````` Ralf Jung committed Feb 11, 2016 384 385 ``````Lemma local_update L `{!LocalUpdate Lv L} x y : Lv x → ✓ (x ⋅ y) → L (x ⋅ y) ≡ L x ⋅ y. `````` Robbert Krebbers committed Feb 24, 2016 386 387 388 ``````Proof. by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L). Qed. `````` Robbert Krebbers committed Feb 11, 2016 389 390 `````` Global Instance local_update_op x : LocalUpdate (λ _, True) (op x). `````` Robbert Krebbers committed Feb 11, 2016 391 ``````Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed. `````` Robbert Krebbers committed Feb 11, 2016 392 `````` `````` Ralf Jung committed Feb 13, 2016 393 394 395 ``````Global Instance local_update_id : LocalUpdate (λ _, True) (@id A). Proof. split; auto with typeclass_instances. Qed. `````` Robbert Krebbers committed Feb 01, 2016 396 ``````(** ** Updates *) `````` Robbert Krebbers committed Jan 14, 2016 397 ``````Global Instance cmra_update_preorder : PreOrder (@cmra_update A). `````` Robbert Krebbers committed Nov 22, 2015 398 ``````Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed. `````` Ralf Jung committed Feb 03, 2016 399 ``````Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). `````` Robbert Krebbers committed Nov 22, 2015 400 401 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 402 `````` - by intros Hx z ?; exists y; split; [done|apply (Hx z)]. `````` Robbert Krebbers committed Feb 18, 2016 403 `````` - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?). `````` Robbert Krebbers committed Nov 22, 2015 404 ``````Qed. `````` Ralf Jung committed Feb 03, 2016 405 ``````Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. `````` Robbert Krebbers committed Feb 18, 2016 406 ``````Proof. by intros ? n z ?; exists x. Qed. `````` Robbert Krebbers committed Feb 02, 2016 407 ``````Lemma cmra_updateP_compose (P Q : A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 408 `````` x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 409 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 410 `````` intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y). `````` Robbert Krebbers committed Feb 02, 2016 411 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 412 413 414 415 416 ``````Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q. Proof. rewrite cmra_update_updateP. intros; apply cmra_updateP_compose with (y =); intros; subst; auto. Qed. `````` Ralf Jung committed Feb 03, 2016 417 ``````Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 418 ``````Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. `````` Robbert Krebbers committed Feb 02, 2016 419 `````` `````` Robbert Krebbers committed Feb 02, 2016 420 ``````Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 421 `````` x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 422 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 423 424 425 `````` intros Hx1 Hx2 Hy n z ?. destruct (Hx1 n (x2 ⋅ z)) as (y1&?&?); first by rewrite assoc. destruct (Hx2 n (y1 ⋅ z)) as (y2&?&?); `````` Robbert Krebbers committed Feb 11, 2016 426 427 `````` first by rewrite assoc (comm _ x2) -assoc. exists (y1 ⋅ y2); split; last rewrite (comm _ y1) -assoc; auto. `````` Robbert Krebbers committed Feb 02, 2016 428 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 429 ``````Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 430 `````` x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. `````` Robbert Krebbers committed Feb 02, 2016 431 ``````Proof. eauto 10 using cmra_updateP_op. Qed. `````` Ralf Jung committed Feb 03, 2016 432 ``````Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2. `````` Robbert Krebbers committed Feb 02, 2016 433 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 434 `````` rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. `````` Robbert Krebbers committed Feb 02, 2016 435 ``````Qed. `````` Ralf Jung committed Feb 13, 2016 436 437 ``````Lemma cmra_update_id x : x ~~> x. Proof. intro. auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 438 439 ``````End cmra. `````` Robbert Krebbers committed May 27, 2016 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 ``````(** * Properties about CMRAs with a unit element **) Section ucmra. Context {A : ucmraT}. Implicit Types x y z : A. Global Instance ucmra_unit_inhabited : Inhabited A := populate ∅. 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. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed. Lemma ucmra_core_unit : core (∅:A) ≡ ∅. Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed. Lemma ucmra_update_unit x : x ~~> ∅. Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed. Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y. Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed. End ucmra. `````` Robbert Krebbers committed Feb 01, 2016 466 ``````(** * Properties about monotone functions *) `````` Robbert Krebbers committed Jan 14, 2016 467 ``````Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A). `````` Robbert Krebbers committed Feb 26, 2016 468 ``````Proof. repeat split; by try apply _. Qed. `````` Robbert Krebbers committed Feb 01, 2016 469 470 ``````Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) : CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f). `````` Robbert Krebbers committed Nov 20, 2015 471 472 ``````Proof. split. `````` Robbert Krebbers committed Feb 26, 2016 473 `````` - apply _. `````` Robbert Krebbers committed Feb 17, 2016 474 `````` - move=> n x Hx /=. by apply validN_preserving, validN_preserving. `````` Robbert Krebbers committed Feb 26, 2016 475 `````` - move=> x y Hxy /=. by apply included_preserving, included_preserving. `````` Robbert Krebbers committed Nov 20, 2015 476 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 477 `````` `````` Robbert Krebbers committed Feb 01, 2016 478 479 ``````Section cmra_monotone. Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}. `````` Robbert Krebbers committed Feb 26, 2016 480 481 `````` Global Instance cmra_monotone_proper : Proper ((≡) ==> (≡)) f := ne_proper _. Lemma includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y. `````` Robbert Krebbers committed Feb 01, 2016 482 `````` Proof. `````` Robbert Krebbers committed Feb 26, 2016 483 `````` intros [z ->]. `````` Robbert Krebbers committed Feb 26, 2016 484 `````` apply cmra_included_includedN, (included_preserving f), cmra_included_l. `````` Robbert Krebbers committed Feb 01, 2016 485 `````` Qed. `````` Robbert Krebbers committed Feb 11, 2016 486 `````` Lemma valid_preserving x : ✓ x → ✓ f x. `````` Robbert Krebbers committed Feb 01, 2016 487 488 489 `````` Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed. End cmra_monotone. `````` Robbert Krebbers committed May 25, 2016 490 491 ``````(** Functors *) Structure rFunctor := RFunctor { `````` Robbert Krebbers committed May 27, 2016 492 `````` rFunctor_car : cofeT → cofeT → cmraT; `````` Robbert Krebbers committed May 25, 2016 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 `````` rFunctor_map {A1 A2 B1 B2} : ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2; rFunctor_ne A1 A2 B1 B2 n : Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2); rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x; rFunctor_compose {A1 A2 A3 B1 B2 B3} (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x : rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x); rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) : CMRAMonotone (rFunctor_map fg) }. Existing Instances rFunctor_ne rFunctor_mono. Instance: Params (@rFunctor_map) 5. Class rFunctorContractive (F : rFunctor) := rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2). Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A. Coercion rFunctor_diag : rFunctor >-> Funclass. Program Definition constRF (B : cmraT) : rFunctor := {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}. Solve Obligations with done. Instance constRF_contractive B : rFunctorContractive (constRF B). Proof. rewrite /rFunctorContractive; apply _. Qed. `````` Robbert Krebbers committed May 27, 2016 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 ``````Structure urFunctor := URFunctor { urFunctor_car : cofeT → cofeT → ucmraT; urFunctor_map {A1 A2 B1 B2} : ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2; urFunctor_ne A1 A2 B1 B2 n : Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2); urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x ≡ x; urFunctor_compose {A1 A2 A3 B1 B2 B3} (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x : urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x); urFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) : CMRAMonotone (urFunctor_map fg) }. Existing Instances urFunctor_ne urFunctor_mono. Instance: Params (@urFunctor_map) 5. Class urFunctorContractive (F : urFunctor) := urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2). Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A. Coercion urFunctor_diag : urFunctor >-> Funclass. Program Definition constURF (B : ucmraT) : urFunctor := {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}. Solve Obligations with done. Instance constURF_contractive B : urFunctorContractive (constURF B). Proof. rewrite /urFunctorContractive; apply _. Qed. `````` Robbert Krebbers committed Feb 08, 2016 549 550 551 552 553 554 555 556 557 558 559 560 561 ``````(** * Transporting a CMRA equality *) Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B := eq_rect A id x _ H. Section cmra_transport. Context {A B : cmraT} (H : A = B). Notation T := (cmra_transport H). Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T. Proof. by intros ???; destruct H. Qed. Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T. Proof. by intros ???; destruct H. Qed. Lemma cmra_transport_op x y : T (x ⋅ y) = T x ⋅ T y. Proof. by destruct H. Qed. `````` Ralf Jung committed Mar 08, 2016 562 `````` Lemma cmra_transport_core x : T (core x) = core (T x). `````` Robbert Krebbers committed Feb 08, 2016 563 `````` Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 11, 2016 564 `````` Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x. `````` Robbert Krebbers committed Feb 08, 2016 565 `````` Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 11, 2016 566 `````` Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x. `````` Robbert Krebbers committed Feb 08, 2016 567 568 569 `````` Proof. by destruct H. Qed. Global Instance cmra_transport_timeless x : Timeless x → Timeless (T x). Proof. by destruct H. Qed. `````` Robbert Krebbers committed Mar 15, 2016 570 571 `````` Global Instance cmra_transport_persistent x : Persistent x → Persistent (T x). Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 08, 2016 572 573 574 575 576 577 578 579 `````` Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x : x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q. Proof. destruct H; eauto using cmra_updateP_weaken. Qed. Lemma cmra_transport_updateP' (P : A → Prop) x : x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'. Proof. eauto using cmra_transport_updateP. Qed. End cmra_transport. `````` Robbert Krebbers committed Feb 01, 2016 580 581 ``````(** * Instances *) (** ** Discrete CMRA *) `````` Robbert Krebbers committed May 25, 2016 582 ``````Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := { `````` Robbert Krebbers committed Feb 01, 2016 583 584 `````` (* setoids *) ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x); `````` Robbert Krebbers committed May 25, 2016 585 586 `````` ra_core_ne : Proper ((≡) ==> (≡)) core; ra_validN_ne : Proper ((≡) ==> impl) valid; `````` Robbert Krebbers committed Feb 01, 2016 587 `````` (* monoid *) `````` Robbert Krebbers committed May 25, 2016 588 589 `````` ra_assoc : Assoc (≡) (⋅); ra_comm : Comm (≡) (⋅); `````` Ralf Jung committed Mar 08, 2016 590 591 592 `````` ra_core_l x : core x ⋅ x ≡ x; ra_core_idemp x : core (core x) ≡ core x; ra_core_preserving x y : x ≼ y → core x ≼ core y; `````` Robbert Krebbers committed Mar 11, 2016 593 `````` ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x `````` Robbert Krebbers committed Feb 01, 2016 594 595 ``````}. `````` Robbert Krebbers committed Nov 16, 2015 596 ``````Section discrete. `````` Robbert Krebbers committed May 25, 2016 597 598 599 `````` Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A (≡)}. Context (ra_mix : RAMixin A). Existing Instances discrete_dist discrete_compl. `````` Robbert Krebbers committed Feb 01, 2016 600 `````` `````` Robbert Krebbers committed Feb 10, 2016 601 `````` Instance discrete_validN : ValidN A := λ n x, ✓ x. `````` Robbert Krebbers committed Jan 14, 2016 602 `````` Definition discrete_cmra_mixin : CMRAMixin A. `````` Robbert Krebbers committed Nov 16, 2015 603 `````` Proof. `````` Robbert Krebbers committed May 25, 2016 604 `````` destruct ra_mix; split; try done. `````` Robbert Krebbers committed Feb 24, 2016 605 `````` - intros x; split; first done. by move=> /(_ 0). `````` Robbert Krebbers committed May 25, 2016 606 `````` - intros n x y1 y2 ??; by exists (y1,y2). `````` Robbert Krebbers committed Nov 16, 2015 607 608 609 `````` Qed. End discrete. `````` Robbert Krebbers committed May 25, 2016 610 611 612 613 614 615 616 617 618 ``````Notation discreteR A ra_mix := (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)). Notation discreteLeibnizR A ra_mix := (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)). Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A, @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix). Proof. split. apply _. done. Qed. `````` Robbert Krebbers committed Feb 01, 2016 619 620 621 ``````(** ** CMRA for the unit type *) Section unit. Instance unit_valid : Valid () := λ x, True. `````` Robbert Krebbers committed May 25, 2016 622 `````` Instance unit_validN : ValidN () := λ n x, True. `````` Ralf Jung committed Mar 08, 2016 623 `````` Instance unit_core : Core () := λ x, x. `````` Robbert Krebbers committed Feb 01, 2016 624 `````` Instance unit_op : Op () := λ x y, (). `````` Robbert Krebbers committed May 27, 2016 625 626 `````` Lemma unit_cmra_mixin : CMRAMixin (). `````` Robbert Krebbers committed May 25, 2016 627 628 `````` Proof. by split; last exists ((),()). Qed. Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 629 630 631 632 633 634 635 `````` Instance unit_empty : Empty () := (). Lemma unit_ucmra_mixin : UCMRAMixin (). Proof. done. Qed. Canonical Structure unitUR : ucmraT := UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin. `````` Robbert Krebbers committed Mar 01, 2016 636 `````` Global Instance unit_cmra_discrete : CMRADiscrete unitR. `````` Robbert Krebbers committed May 25, 2016 637 `````` Proof. done. Qed. `````` Robbert Krebbers committed Mar 15, 2016 638 639 `````` Global Instance unit_persistent (x : ()) : Persistent x. Proof. done. Qed. `````` Robbert Krebbers committed Feb 01, 2016 640 ``````End unit. `````` Ralf Jung committed Jan 19, 2016 641 `````` `````` Robbert Krebbers committed Feb 01, 2016 642 ``````(** ** Product *) `````` Robbert Krebbers committed Jan 14, 2016 643 644 645 ``````Section prod. Context {A B : cmraT}. Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2). `````` Ralf Jung committed Mar 08, 2016 646 `````` Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)). `````` Robbert Krebbers committed Feb 24, 2016 647 `````` Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2. `````` Robbert Krebbers committed Feb 11, 2016 648 `````` Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2. `````` Robbert Krebbers committed May 27, 2016 649 `````` `````` Robbert Krebbers committed Jan 14, 2016 650 651 652 653 654 655 656 657 658 659 `````` Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2. Proof. split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|]. intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto. Qed. Lemma prod_includedN (x y : A * B) n : x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2. Proof. split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|]. intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto. Qed. `````` Robbert Krebbers committed May 27, 2016 660 `````` `````` Robbert Krebbers committed Jan 14, 2016 661 662 663 `````` Definition prod_cmra_mixin : CMRAMixin (A * B). Proof. split; try apply _. `````` Robbert Krebbers committed Feb 17, 2016 664 665 666 `````` - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2. - by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2. - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2. `````` Robbert Krebbers committed Feb 24, 2016 667 668 669 `````` - intros x; split. + intros [??] n; split; by apply cmra_valid_validN. + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy. `````` Robbert Krebbers committed Feb 17, 2016 670 671 672 `````` - by intros n x [??]; split; apply cmra_validN_S. - by split; rewrite /= assoc. - by split; rewrite /= comm. `````` Ralf Jung committed Mar 08, 2016 673 674 `````` - by split; rewrite /= cmra_core_l. - by split; rewrite /= cmra_core_idemp. `````` Robbert Krebbers committed Feb 26, 2016 675 `````` - intros x y; rewrite !prod_included. `````` Ralf Jung committed Mar 08, 2016 676 `````` by intros [??]; split; apply cmra_core_preserving. `````` Robbert Krebbers committed Feb 17, 2016 677 `````` - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. `````` Robbert Krebbers committed Feb 24, 2016 678 679 680 681 `````` - intros n x y1 y2 [??] [??]; simpl in *. destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto. destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto. by exists ((z1.1,z2.1),(z1.2,z2.2)). `````` Robbert Krebbers committed Jan 14, 2016 682 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 683 `````` Canonical Structure prodR := `````` Robbert Krebbers committed May 25, 2016 684 `````` CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 685 `````` `````` Robbert Krebbers committed Feb 24, 2016 686 `````` Global Instance prod_cmra_discrete : `````` Robbert Krebbers committed Mar 01, 2016 687 `````` CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodR. `````` Robbert Krebbers committed Feb 24, 2016 688 689 `````` Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed. `````` Robbert Krebbers committed Mar 15, 2016 690 691 692 693 `````` Global Instance pair_persistent x y : Persistent x → Persistent y → Persistent (x,y). Proof. by split. Qed. `````` Ralf Jung committed Feb 03, 2016 694 `````` Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. `````` Robbert Krebbers committed Feb 18, 2016 695 `````` Proof. intros ?? n z [??]; split; simpl in *; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 696 `` Lemma prod_updateP ``