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