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