cmra.v 27 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 116 117 118 119 ```````empty' element is the unit. *) Class CMRAUnit (A : cmraT) `{Empty A} := { cmra_unit_valid : ✓ ∅; cmra_unit_left_id :> LeftId (≡) ∅ (⋅); cmra_unit_timeless :> Timeless ∅ `````` Robbert Krebbers committed Feb 01, 2016 120 ``````}. `````` Ralf Jung committed Mar 08, 2016 121 ``````Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate ∅. `````` Robbert Krebbers committed Jan 14, 2016 122 `````` `````` Robbert Krebbers committed Mar 15, 2016 123 124 125 126 ``````(** * Persistent elements *) Class Persistent {A : cmraT} (x : A) := persistent : core x ≡ x. Arguments persistent {_} _ {_}. `````` Robbert Krebbers committed Feb 24, 2016 127 ``````(** * Discrete CMRAs *) `````` Robbert Krebbers committed Feb 26, 2016 128 ``````Class CMRADiscrete (A : cmraT) := { `````` Robbert Krebbers committed Feb 24, 2016 129 130 131 132 `````` cmra_discrete :> Discrete A; cmra_discrete_valid (x : A) : ✓{0} x → ✓ x }. `````` Robbert Krebbers committed Jan 16, 2016 133 ``````(** * Morphisms *) `````` Robbert Krebbers committed Jan 14, 2016 134 ``````Class CMRAMonotone {A B : cmraT} (f : A → B) := { `````` Robbert Krebbers committed Feb 26, 2016 135 136 137 `````` 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 138 ``````}. `````` Robbert Krebbers committed Feb 26, 2016 139 140 ``````Arguments validN_preserving {_ _} _ {_} _ _ _. Arguments included_preserving {_ _} _ {_} _ _ _. `````` Robbert Krebbers committed Jan 14, 2016 141 `````` `````` Robbert Krebbers committed Feb 11, 2016 142 ``````(** * Local updates *) `````` Ralf Jung committed Feb 13, 2016 143 144 ``````(** 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 145 146 147 ``````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 148 149 150 ``````}. Arguments local_updateN {_ _} _ {_} _ _ _ _ _. `````` Robbert Krebbers committed Feb 01, 2016 151 ``````(** * Frame preserving updates *) `````` Robbert Krebbers committed Feb 18, 2016 152 ``````Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n z, `````` Robbert Krebbers committed Feb 10, 2016 153 `````` ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). `````` Robbert Krebbers committed Feb 02, 2016 154 ``````Instance: Params (@cmra_updateP) 1. `````` Ralf Jung committed Feb 03, 2016 155 ``````Infix "~~>:" := cmra_updateP (at level 70). `````` Robbert Krebbers committed Feb 18, 2016 156 ``````Definition cmra_update {A : cmraT} (x y : A) := ∀ n z, `````` Robbert Krebbers committed Feb 10, 2016 157 `````` ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). `````` Ralf Jung committed Feb 03, 2016 158 ``````Infix "~~>" := cmra_update (at level 70). `````` Robbert Krebbers committed Feb 02, 2016 159 ``````Instance: Params (@cmra_update) 1. `````` Robbert Krebbers committed Nov 22, 2015 160 `````` `````` Robbert Krebbers committed Jan 16, 2016 161 ``````(** * Properties **) `````` Robbert Krebbers committed Nov 11, 2015 162 ``````Section cmra. `````` Robbert Krebbers committed Jan 14, 2016 163 ``````Context {A : cmraT}. `````` Robbert Krebbers committed Nov 11, 2015 164 ``````Implicit Types x y z : A. `````` Robbert Krebbers committed Feb 01, 2016 165 ``````Implicit Types xs ys zs : list A. `````` Robbert Krebbers committed Nov 11, 2015 166 `````` `````` Robbert Krebbers committed Feb 01, 2016 167 ``````(** ** Setoids *) `````` Ralf Jung committed Mar 08, 2016 168 ``````Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _). `````` Robbert Krebbers committed Feb 01, 2016 169 170 171 172 ``````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 173 `````` by rewrite Hy (comm _ x1) Hx (comm _ y2). `````` Robbert Krebbers committed Feb 01, 2016 174 175 176 177 178 179 180 181 182 ``````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 183 184 185 186 ``````Proof. intros x y Hxy; rewrite !cmra_valid_validN. by split=> ? n; [rewrite -Hxy|rewrite Hxy]. Qed. `````` Robbert Krebbers committed Feb 01, 2016 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 ``````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 205 206 207 ``````Global Instance cmra_update_proper : Proper ((≡) ==> (≡) ==> iff) (@cmra_update A). Proof. `````` Robbert Krebbers committed Feb 18, 2016 208 `````` intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto. `````` Robbert Krebbers committed Feb 02, 2016 209 210 211 212 ``````Qed. Global Instance cmra_updateP_proper : Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A). Proof. `````` Robbert Krebbers committed Feb 18, 2016 213 `````` intros x1 x2 Hx P1 P2 HP; split=>Hup n z; `````` Robbert Krebbers committed Feb 02, 2016 214 215 `````` [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 216 217 `````` (** ** Validity *) `````` Robbert Krebbers committed Feb 18, 2016 218 ``````Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x. `````` Robbert Krebbers committed Feb 01, 2016 219 220 221 ``````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 222 ``````Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y. `````` Robbert Krebbers committed Feb 11, 2016 223 ``````Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 224 225 226 ``````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 227 228 229 230 231 232 233 234 235 ``````(** ** 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 236 237 ``````Global Instance cmra_core_persistent x : Persistent (core x). Proof. apply cmra_core_idemp. Qed. `````` Robbert Krebbers committed Feb 01, 2016 238 239 `````` (** ** Order *) `````` Robbert Krebbers committed Mar 11, 2016 240 241 ``````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 242 243 244 ``````Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n). Proof. split. `````` Ralf Jung committed Mar 08, 2016 245 `````` - by intros x; exists (core x); rewrite cmra_core_r. `````` Robbert Krebbers committed Feb 17, 2016 246 `````` - intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). `````` Robbert Krebbers committed Feb 11, 2016 247 `````` by rewrite assoc -Hy -Hz. `````` Robbert Krebbers committed Feb 01, 2016 248 249 250 ``````Qed. Global Instance cmra_included_preorder: PreOrder (@included A _ _). Proof. `````` Robbert Krebbers committed Mar 11, 2016 251 252 253 254 `````` 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 255 ``````Qed. `````` Robbert Krebbers committed Feb 18, 2016 256 ``````Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x. `````` Robbert Krebbers committed Feb 01, 2016 257 ``````Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 18, 2016 258 ``````Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x. `````` Robbert Krebbers committed Mar 11, 2016 259 ``````Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 260 `````` `````` Robbert Krebbers committed Feb 18, 2016 261 ``````Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y. `````` Robbert Krebbers committed Feb 01, 2016 262 ``````Proof. by intros [z Hz]; exists z; apply dist_S. Qed. `````` Robbert Krebbers committed Feb 18, 2016 263 ``````Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y. `````` Robbert Krebbers committed Feb 01, 2016 264 265 266 267 268 269 270 ``````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 271 ``````Proof. rewrite (comm op); apply cmra_includedN_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 272 ``````Lemma cmra_included_r x y : y ≼ x ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 273 ``````Proof. rewrite (comm op); apply cmra_included_l. Qed. `````` Robbert Krebbers committed Nov 20, 2015 274 `````` `````` Ralf Jung committed Mar 08, 2016 275 ``````Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y. `````` Robbert Krebbers committed Feb 26, 2016 276 277 ``````Proof. intros [z ->]. `````` Ralf Jung committed Mar 08, 2016 278 `````` apply cmra_included_includedN, cmra_core_preserving, cmra_included_l. `````` Robbert Krebbers committed Feb 26, 2016 279 ``````Qed. `````` Ralf Jung committed Mar 08, 2016 280 281 ``````Lemma cmra_included_core x : core x ≼ x. Proof. by exists x; rewrite cmra_core_l. Qed. `````` Robbert Krebbers committed Feb 11, 2016 282 ``````Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 283 ``````Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. `````` Robbert Krebbers committed Feb 01, 2016 284 ``````Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y. `````` Robbert Krebbers committed Feb 11, 2016 285 ``````Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. `````` Robbert Krebbers committed Feb 11, 2016 286 ``````Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z. `````` Robbert Krebbers committed Feb 11, 2016 287 ``````Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 288 ``````Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z. `````` Robbert Krebbers committed Feb 11, 2016 289 ``````Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed. `````` Robbert Krebbers committed Feb 01, 2016 290 `````` `````` Robbert Krebbers committed Feb 18, 2016 291 ``````Lemma cmra_included_dist_l n x1 x2 x1' : `````` Ralf Jung committed Feb 10, 2016 292 `````` x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. `````` Robbert Krebbers committed Nov 11, 2015 293 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 294 295 `````` intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l. by rewrite Hx1 Hx2. `````` Robbert Krebbers committed Nov 11, 2015 296 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 297 `````` `````` Robbert Krebbers committed Jan 16, 2016 298 ``````(** ** Timeless *) `````` Robbert Krebbers committed Feb 10, 2016 299 ``````Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y. `````` Robbert Krebbers committed Dec 11, 2015 300 301 ``````Proof. intros ?? [x' ?]. `````` Robbert Krebbers committed Feb 24, 2016 302 `````` destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. `````` Robbert Krebbers committed Jan 13, 2016 303 `````` by exists z'; rewrite Hy (timeless x z). `````` Robbert Krebbers committed Dec 11, 2015 304 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 305 ``````Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y. `````` Robbert Krebbers committed Dec 11, 2015 306 ``````Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed. `````` Robbert Krebbers committed Jan 14, 2016 307 ``````Lemma cmra_op_timeless x1 x2 : `````` Robbert Krebbers committed Dec 11, 2015 308 `````` ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). `````` Robbert Krebbers committed Nov 18, 2015 309 310 ``````Proof. intros ??? z Hz. `````` Robbert Krebbers committed Feb 24, 2016 311 `````` destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. `````` Robbert Krebbers committed Feb 24, 2016 312 `````` { rewrite -?Hz. by apply cmra_valid_validN. } `````` Robbert Krebbers committed Jan 13, 2016 313 `````` by rewrite Hz' (timeless x1 y1) // (timeless x2 y2). `````` Robbert Krebbers committed Nov 18, 2015 314 ``````Qed. `````` Robbert Krebbers committed Nov 20, 2015 315 `````` `````` Robbert Krebbers committed Feb 24, 2016 316 317 318 319 320 321 322 323 ``````(** ** 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 324 `````` split; first by apply cmra_included_includedN. `````` Robbert Krebbers committed Feb 24, 2016 325 326 327 328 329 330 331 332 333 `````` 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. `````` Ralf Jung committed Mar 08, 2016 334 335 336 337 338 339 ``````(** ** RAs with a unit element *) Section unit. Context `{Empty A, !CMRAUnit A}. Lemma cmra_unit_validN n : ✓{n} ∅. Proof. apply cmra_valid_validN, cmra_unit_valid. Qed. Lemma cmra_unit_leastN n x : ∅ ≼{n} x. `````` Robbert Krebbers committed Feb 01, 2016 340 `````` Proof. by exists x; rewrite left_id. Qed. `````` Ralf Jung committed Mar 08, 2016 341 `````` Lemma cmra_unit_least x : ∅ ≼ x. `````` Robbert Krebbers committed Feb 01, 2016 342 `````` Proof. by exists x; rewrite left_id. Qed. `````` Ralf Jung committed Mar 08, 2016 343 `````` Global Instance cmra_unit_right_id : RightId (≡) ∅ (⋅). `````` Robbert Krebbers committed Feb 11, 2016 344 `````` Proof. by intros x; rewrite (comm op) left_id. Qed. `````` Robbert Krebbers committed Mar 15, 2016 345 346 `````` Global Instance cmra_unit_persistent : Persistent ∅. Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed. `````` Robbert Krebbers committed May 22, 2016 347 348 `````` Lemma cmra_core_unit : core (∅:A) ≡ ∅. Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed. `````` Ralf Jung committed Mar 08, 2016 349 ``````End unit. `````` Robbert Krebbers committed Nov 20, 2015 350 `````` `````` Robbert Krebbers committed Feb 11, 2016 351 ``````(** ** Local updates *) `````` Ralf Jung committed Feb 11, 2016 352 353 ``````Global Instance local_update_proper Lv (L : A → A) : LocalUpdate Lv L → Proper ((≡) ==> (≡)) L. `````` Robbert Krebbers committed Feb 11, 2016 354 355 ``````Proof. intros; apply (ne_proper _). Qed. `````` Ralf Jung committed Feb 11, 2016 356 357 ``````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 358 359 360 ``````Proof. by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L). Qed. `````` Robbert Krebbers committed Feb 11, 2016 361 362 `````` Global Instance local_update_op x : LocalUpdate (λ _, True) (op x). `````` Robbert Krebbers committed Feb 11, 2016 363 ``````Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed. `````` Robbert Krebbers committed Feb 11, 2016 364 `````` `````` Ralf Jung committed Feb 13, 2016 365 366 367 ``````Global Instance local_update_id : LocalUpdate (λ _, True) (@id A). Proof. split; auto with typeclass_instances. Qed. `````` Robbert Krebbers committed Feb 01, 2016 368 ``````(** ** Updates *) `````` Robbert Krebbers committed Jan 14, 2016 369 ``````Global Instance cmra_update_preorder : PreOrder (@cmra_update A). `````` Robbert Krebbers committed Nov 22, 2015 370 ``````Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed. `````` Ralf Jung committed Feb 03, 2016 371 ``````Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). `````` Robbert Krebbers committed Nov 22, 2015 372 373 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 374 `````` - by intros Hx z ?; exists y; split; [done|apply (Hx z)]. `````` Robbert Krebbers committed Feb 18, 2016 375 `````` - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?). `````` Robbert Krebbers committed Nov 22, 2015 376 ``````Qed. `````` Ralf Jung committed Feb 03, 2016 377 ``````Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. `````` Robbert Krebbers committed Feb 18, 2016 378 ``````Proof. by intros ? n z ?; exists x. Qed. `````` Robbert Krebbers committed Feb 02, 2016 379 ``````Lemma cmra_updateP_compose (P Q : A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 380 `````` x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 381 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 382 `````` intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y). `````` Robbert Krebbers committed Feb 02, 2016 383 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 384 385 386 387 388 ``````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 389 ``````Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 390 ``````Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. `````` Robbert Krebbers committed Feb 02, 2016 391 `````` `````` Robbert Krebbers committed Feb 02, 2016 392 ``````Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 393 `````` x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 394 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 395 396 397 `````` 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 398 399 `````` first by rewrite assoc (comm _ x2) -assoc. exists (y1 ⋅ y2); split; last rewrite (comm _ y1) -assoc; auto. `````` Robbert Krebbers committed Feb 02, 2016 400 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 401 ``````Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 402 `````` x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. `````` Robbert Krebbers committed Feb 02, 2016 403 ``````Proof. eauto 10 using cmra_updateP_op. Qed. `````` Ralf Jung committed Feb 03, 2016 404 ``````Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2. `````` Robbert Krebbers committed Feb 02, 2016 405 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 406 `````` rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. `````` Robbert Krebbers committed Feb 02, 2016 407 ``````Qed. `````` Ralf Jung committed Feb 13, 2016 408 409 ``````Lemma cmra_update_id x : x ~~> x. Proof. intro. auto. Qed. `````` Robbert Krebbers committed Feb 08, 2016 410 `````` `````` Ralf Jung committed Mar 08, 2016 411 412 413 ``````Section unit_updates. Context `{Empty A, !CMRAUnit A}. Lemma cmra_update_unit x : x ~~> ∅. `````` Robbert Krebbers committed Feb 18, 2016 414 `````` Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed. `````` Ralf Jung committed Mar 08, 2016 415 416 417 `````` Lemma cmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y. Proof. split; [intros; trans ∅|]; auto using cmra_update_unit. Qed. End unit_updates. `````` Robbert Krebbers committed Nov 11, 2015 418 419 ``````End cmra. `````` Robbert Krebbers committed Feb 01, 2016 420 ``````(** * Properties about monotone functions *) `````` Robbert Krebbers committed Jan 14, 2016 421 ``````Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A). `````` Robbert Krebbers committed Feb 26, 2016 422 ``````Proof. repeat split; by try apply _. Qed. `````` Robbert Krebbers committed Feb 01, 2016 423 424 ``````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 425 426 ``````Proof. split. `````` Robbert Krebbers committed Feb 26, 2016 427 `````` - apply _. `````` Robbert Krebbers committed Feb 17, 2016 428 `````` - move=> n x Hx /=. by apply validN_preserving, validN_preserving. `````` Robbert Krebbers committed Feb 26, 2016 429 `````` - move=> x y Hxy /=. by apply included_preserving, included_preserving. `````` Robbert Krebbers committed Nov 20, 2015 430 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 431 `````` `````` Robbert Krebbers committed Feb 01, 2016 432 433 ``````Section cmra_monotone. Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}. `````` Robbert Krebbers committed Feb 26, 2016 434 435 `````` 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 436 `````` Proof. `````` Robbert Krebbers committed Feb 26, 2016 437 `````` intros [z ->]. `````` Robbert Krebbers committed Feb 26, 2016 438 `````` apply cmra_included_includedN, (included_preserving f), cmra_included_l. `````` Robbert Krebbers committed Feb 01, 2016 439 `````` Qed. `````` Robbert Krebbers committed Feb 11, 2016 440 `````` Lemma valid_preserving x : ✓ x → ✓ f x. `````` Robbert Krebbers committed Feb 01, 2016 441 442 443 `````` Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed. End cmra_monotone. `````` Robbert Krebbers committed Feb 08, 2016 444 445 446 447 448 449 450 451 452 453 454 455 456 ``````(** * 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 457 `````` Lemma cmra_transport_core x : T (core x) = core (T x). `````` Robbert Krebbers committed Feb 08, 2016 458 `````` Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 11, 2016 459 `````` Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x. `````` Robbert Krebbers committed Feb 08, 2016 460 `````` Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 11, 2016 461 `````` Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x. `````` Robbert Krebbers committed Feb 08, 2016 462 463 464 `````` 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 465 466 `````` Global Instance cmra_transport_persistent x : Persistent x → Persistent (T x). Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 08, 2016 467 468 469 470 471 472 473 474 `````` 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 475 476 ``````(** * Instances *) (** ** Discrete CMRA *) `````` Robbert Krebbers committed May 25, 2016 477 ``````Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := { `````` Robbert Krebbers committed Feb 01, 2016 478 479 `````` (* setoids *) ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x); `````` Robbert Krebbers committed May 25, 2016 480 481 `````` ra_core_ne : Proper ((≡) ==> (≡)) core; ra_validN_ne : Proper ((≡) ==> impl) valid; `````` Robbert Krebbers committed Feb 01, 2016 482 `````` (* monoid *) `````` Robbert Krebbers committed May 25, 2016 483 484 `````` ra_assoc : Assoc (≡) (⋅); ra_comm : Comm (≡) (⋅); `````` Ralf Jung committed Mar 08, 2016 485 486 487 `````` 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 488 `````` ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x `````` Robbert Krebbers committed Feb 01, 2016 489 490 ``````}. `````` Robbert Krebbers committed Nov 16, 2015 491 ``````Section discrete. `````` Robbert Krebbers committed May 25, 2016 492 493 494 `````` 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 495 `````` `````` Robbert Krebbers committed Feb 10, 2016 496 `````` Instance discrete_validN : ValidN A := λ n x, ✓ x. `````` Robbert Krebbers committed Jan 14, 2016 497 `````` Definition discrete_cmra_mixin : CMRAMixin A. `````` Robbert Krebbers committed Nov 16, 2015 498 `````` Proof. `````` Robbert Krebbers committed May 25, 2016 499 `````` destruct ra_mix; split; try done. `````` Robbert Krebbers committed Feb 24, 2016 500 `````` - intros x; split; first done. by move=> /(_ 0). `````` Robbert Krebbers committed May 25, 2016 501 `````` - intros n x y1 y2 ??; by exists (y1,y2). `````` Robbert Krebbers committed Nov 16, 2015 502 503 504 `````` Qed. End discrete. `````` Robbert Krebbers committed May 25, 2016 505 506 507 508 509 510 511 512 513 ``````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 514 515 516 ``````(** ** CMRA for the unit type *) Section unit. Instance unit_valid : Valid () := λ x, True. `````` Robbert Krebbers committed May 25, 2016 517 `````` Instance unit_validN : ValidN () := λ n x, True. `````` Ralf Jung committed Mar 08, 2016 518 `````` Instance unit_core : Core () := λ x, x. `````` Robbert Krebbers committed Feb 01, 2016 519 520 `````` Instance unit_op : Op () := λ x y, (). Global Instance unit_empty : Empty () := (). `````` Robbert Krebbers committed May 25, 2016 521 522 523 `````` Definition unit_cmra_mixin : CMRAMixin (). Proof. by split; last exists ((),()). Qed. Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin. `````` Ralf Jung committed Mar 08, 2016 524 `````` Global Instance unit_cmra_unit : CMRAUnit unitR. `````` Robbert Krebbers committed Mar 01, 2016 525 `````` Global Instance unit_cmra_discrete : CMRADiscrete unitR. `````` Robbert Krebbers committed May 25, 2016 526 `````` Proof. done. Qed. `````` Robbert Krebbers committed Mar 15, 2016 527 528 `````` Global Instance unit_persistent (x : ()) : Persistent x. Proof. done. Qed. `````` Robbert Krebbers committed Feb 01, 2016 529 ``````End unit. `````` Ralf Jung committed Jan 19, 2016 530 `````` `````` Robbert Krebbers committed Feb 01, 2016 531 ``````(** ** Product *) `````` Robbert Krebbers committed Jan 14, 2016 532 533 534 535 ``````Section prod. Context {A B : cmraT}. Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2). Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅). `````` Ralf Jung committed Mar 08, 2016 536 `````` Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)). `````` Robbert Krebbers committed Feb 24, 2016 537 `````` Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2. `````` Robbert Krebbers committed Feb 11, 2016 538 `````` Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2. `````` Robbert Krebbers committed Jan 14, 2016 539 540 541 542 543 544 545 546 547 548 549 550 551 `````` 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. Definition prod_cmra_mixin : CMRAMixin (A * B). Proof. split; try apply _. `````` Robbert Krebbers committed Feb 17, 2016 552 553 554 `````` - 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 555 556 557 `````` - 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 558 559 560 `````` - by intros n x [??]; split; apply cmra_validN_S. - by split; rewrite /= assoc. - by split; rewrite /= comm. `````` Ralf Jung committed Mar 08, 2016 561 562 `````` - by split; rewrite /= cmra_core_l. - by split; rewrite /= cmra_core_idemp. `````` Robbert Krebbers committed Feb 26, 2016 563 `````` - intros x y; rewrite !prod_included. `````` Ralf Jung committed Mar 08, 2016 564 `````` by intros [??]; split; apply cmra_core_preserving. `````` Robbert Krebbers committed Feb 17, 2016 565 `````` - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. `````` Robbert Krebbers committed Feb 24, 2016 566 567 568 569 `````` - 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 570 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 571 572 `````` Canonical Structure prodR : cmraT := CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin. `````` Ralf Jung committed Mar 08, 2016 573 574 `````` Global Instance prod_cmra_unit `{Empty A, Empty B} : CMRAUnit A → CMRAUnit B → CMRAUnit prodR. `````` Robbert Krebbers committed Feb 01, 2016 575 576 `````` Proof. split. `````` Ralf Jung committed Mar 08, 2016 577 `````` - split; apply cmra_unit_valid. `````` Robbert Krebbers committed Feb 17, 2016 578 579 `````` - by split; rewrite /=left_id. - by intros ? [??]; split; apply (timeless _). `````` Robbert Krebbers committed Feb 01, 2016 580 `````` Qed. `````` Robbert Krebbers committed Feb 24, 2016 581 `````` Global Instance prod_cmra_discrete : `````` Robbert Krebbers committed Mar 01, 2016 582 `````` CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodR. `````` Robbert Krebbers committed Feb 24, 2016 583 584 `````` Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed. `````` Robbert Krebbers committed Mar 15, 2016 585 586 587 588 `````` Global Instance pair_persistent x y : Persistent x → Persistent y → Persistent (x,y). Proof. by split. Qed. `````` Robbert Krebbers committed May 23, 2016 589 590 591 592 `````` Lemma pair_split `{CMRAUnit A, CMRAUnit B} (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y). Proof. constructor; by rewrite /= ?left_id ?right_id. Qed. `````` Ralf Jung committed Feb 03, 2016 593 `````` Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. `````` Robbert Krebbers committed Feb 18, 2016 594 `````` Proof. intros ?? n z [??]; split; simpl in *; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 595 `````` Lemma prod_updateP P1 P2 (Q : A * B → Prop) x : `````` Ralf Jung committed Feb 03, 2016 596 `````` x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 597 `````` Proof. `````` Robbert Krebbers committed Feb 18, 2016 598 599 `````` intros Hx1 Hx2 HP n z [??]; simpl in *. destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto. `````` Robbert Krebbers committed Feb 02, 2016 600 601 `````` exists (a,b); repeat split; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 602 `````` Lemma prod_updateP' P1 P2 x : `````` Ralf Jung committed Feb 03, 2016 603 `````` x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2). `````` Robbert Krebbers committed Feb 02, 2016 604 `````` Proof. eauto using prod_updateP. Qed. `````` Robbert Krebbers committed May 22, 2016 605 606 607 608 609 610 611 612 613 614 `````` Global Instance prod_local_update (LA : A → A) `{!LocalUpdate LvA LA} (LB : B → B) `{!LocalUpdate LvB LB} : LocalUpdate (λ x, LvA (x.1) ∧ LvB (x.2)) (prod_map LA LB). Proof. constructor. - intros n x y [??]; constructor; simpl; by apply local_update_ne. - intros n ?? [??] [??]; constructor; simpl in *; eapply local_updateN; eauto. Qed. `````` Robbert Krebbers committed Jan 14, 2016 615 ``````End prod. `````` Robbert Krebbers committed May 22, 2016 616 `````` `````` Robbert Krebbers committed Mar 01, 2016 617 ``````Arguments prodR : clear implicits. `````` Robbert Krebbers committed Jan 14, 2016 618 619 620 `````` Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') : CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g). `````` Robbert Krebbers committed Nov 16, 2015 621 ``````Proof. `````` Robbert Krebbers committed Feb 26, 2016 622 `````` split; first apply _. `````` Robbert Krebbers committed Feb 17, 2016 623 `````` - by intros n x [??]; split; simpl; apply validN_preserving. `````` Robbert Krebbers committed Feb 26, 2016 624 625 `````` - intros x y; rewrite !prod_included=> -[??] /=. by split; apply included_preserving. `````` Robbert Krebbers committed Nov 16, 2015 626 ``````Qed. `````` Robbert Krebbers committed Mar 02, 2016 627 628 629 630 631 632 `````` (** Functors *) Structure rFunctor := RFunctor { rFunctor_car : cofeT → cofeT -> cmraT; rFunctor_map {A1 A2 B1 B2} : ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2; `````` Robbert Krebbers committed Mar 07, 2016 633 634 `````` rFunctor_ne A1 A2 B1 B2 n : Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2); `````` Robbert Krebbers committed Mar 02, 2016 635 636 637 638 639 640 641 `````` 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) }. `````` Robbert Krebbers committed Mar 07, 2016 642 ``````Existing Instances rFunctor_ne rFunctor_mono. `````` Robbert Krebbers committed Mar 02, 2016 643 644 ``````Instance: Params (@rFunctor_map) 5. `````` Ralf Jung committed Mar 07, 2016 645 646 647 ``````Class rFunctorContractive (F : rFunctor) := rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2). `````` Robbert Krebbers committed Mar 02, 2016 648 649 650 651 652 653 654 ``````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. `````` Ralf Jung committed Mar 07, 2016 655 ``````Instance constRF_contractive B : rFunctorContractive (constRF B). `````` Robbert Krebbers committed Mar 07, 2016 656 ``````Proof. rewrite /rFunctorContractive; apply _. Qed. `````` Ralf Jung committed Mar 07, 2016 657 `````` `````` Robbert Krebbers committed Mar 02, 2016 658 659 660 661 662 ``````Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {| rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B); rFunctor_map A1 A2 B1 B2 fg := prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg) |}. `````` Robbert Krebbers committed Mar 07, 2016 663 664 665 ``````Next Obligation. intros F1 F2 A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 666 667 668 669 670 ``````Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed. Next Obligation. intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl. by rewrite !rFunctor_compose. Qed. `````` Ralf Jung committed Mar 07, 2016 671 672 673 674 675 676 677 678 `````` Instance prodRF_contractive F1 F2 : rFunctorContractive F1 → rFunctorContractive F2 → rFunctorContractive (prodRF F1 F2). Proof. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_contractive. Qed.``````