cmra.v 22.5 KB
Newer Older
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.cofe. `````` Robbert Krebbers committed Feb 01, 2016 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 `````` Class Unit (A : Type) := unit : A → A. Instance: Params (@unit) 2. 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. Hint Extern 0 (?x ≼ ?y) => reflexivity. Instance: Params (@included) 3. Class Minus (A : Type) := minus : A → A → A. Instance: Params (@minus) 2. Infix "⩪" := minus (at level 40) : 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 Nov 23, 2015 23 ``````Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }"). `````` Robbert Krebbers committed Nov 11, 2015 24 `````` `````` Robbert Krebbers committed Feb 01, 2016 25 26 27 28 29 ``````Class Valid (A : Type) := valid : A → Prop. Instance: Params (@valid) 2. Notation "✓" := valid (at level 1). Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x. `````` 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 32 33 ``````Notation "x ≼{ n } y" := (includedN n x y) (at level 70, format "x ≼{ n } y") : C_scope. Instance: Params (@includedN) 4. `````` Robbert Krebbers committed Jan 16, 2016 34 ``````Hint Extern 0 (?x ≼{_} ?y) => reflexivity. `````` Robbert Krebbers committed Nov 20, 2015 35 `````` `````` Robbert Krebbers committed Feb 01, 2016 36 ``````Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := { `````` Robbert Krebbers committed Nov 11, 2015 37 `````` (* setoids *) `````` Robbert Krebbers committed Jan 14, 2016 38 39 `````` mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x); mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit; `````` Robbert Krebbers committed Feb 01, 2016 40 `````` mixin_cmra_validN_ne n : Proper (dist n ==> impl) (✓{n}); `````` Robbert Krebbers committed Jan 14, 2016 41 `````` mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus; `````` Robbert Krebbers committed Nov 11, 2015 42 `````` (* valid *) `````` Robbert Krebbers committed Feb 01, 2016 43 `````` mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; `````` Robbert Krebbers committed Nov 11, 2015 44 `````` (* monoid *) `````` Robbert Krebbers committed Jan 14, 2016 45 46 47 48 `````` mixin_cmra_associative : Associative (≡) (⋅); mixin_cmra_commutative : Commutative (≡) (⋅); mixin_cmra_unit_l x : unit x ⋅ x ≡ x; mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit x; `````` Robbert Krebbers committed Feb 01, 2016 49 50 `````` mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y; mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; `````` Ralf Jung committed Feb 10, 2016 51 `````` mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y `````` Robbert Krebbers committed Nov 11, 2015 52 ``````}. `````` Robbert Krebbers committed Jan 14, 2016 53 ``````Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2, `````` Ralf Jung committed Feb 10, 2016 54 55 `````` ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }. `````` Robbert Krebbers committed Nov 22, 2015 56 `````` `````` Robbert Krebbers committed Nov 11, 2015 57 58 59 60 61 62 63 64 65 66 ``````(** Bundeled version *) Structure cmraT := CMRAT { cmra_car :> Type; cmra_equiv : Equiv cmra_car; cmra_dist : Dist cmra_car; cmra_compl : Compl cmra_car; cmra_unit : Unit cmra_car; cmra_op : Op cmra_car; cmra_validN : ValidN cmra_car; cmra_minus : Minus cmra_car; `````` Robbert Krebbers committed Jan 14, 2016 67 68 69 `````` cmra_cofe_mixin : CofeMixin cmra_car; cmra_mixin : CMRAMixin cmra_car; cmra_extend_mixin : CMRAExtendMixin cmra_car `````` Robbert Krebbers committed Nov 11, 2015 70 ``````}. `````` Robbert Krebbers committed Feb 01, 2016 71 ``````Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _. `````` Robbert Krebbers committed Jan 14, 2016 72 73 74 75 76 77 78 79 80 81 82 ``````Arguments cmra_car : simpl never. Arguments cmra_equiv : simpl never. Arguments cmra_dist : simpl never. Arguments cmra_compl : simpl never. Arguments cmra_unit : simpl never. Arguments cmra_op : simpl never. Arguments cmra_validN : simpl never. Arguments cmra_minus : simpl never. Arguments cmra_cofe_mixin : simpl never. Arguments cmra_mixin : simpl never. Arguments cmra_extend_mixin : simpl never. `````` Robbert Krebbers committed Nov 11, 2015 83 ``````Add Printing Constructor cmraT. `````` Robbert Krebbers committed Feb 01, 2016 84 ``````Existing Instances cmra_unit cmra_op cmra_validN cmra_minus. `````` Robbert Krebbers committed Jan 14, 2016 85 ``````Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A). `````` Robbert Krebbers committed Nov 11, 2015 86 87 ``````Canonical Structure cmra_cofeC. `````` Robbert Krebbers committed Jan 14, 2016 88 89 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. Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _). Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 01, 2016 96 97 `````` 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 Jan 14, 2016 98 99 100 `````` Global Instance cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) (@minus A _). Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed. `````` Robbert Krebbers committed Feb 01, 2016 101 102 103 104 105 106 107 108 109 110 111 112 113 114 `````` Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x. Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed. Global Instance cmra_associative : Associative (≡) (@op A _). Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed. Global Instance cmra_commutative : Commutative (≡) (@op A _). Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed. Lemma cmra_unit_l x : unit x ⋅ x ≡ x. Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed. Lemma cmra_unit_idempotent x : unit (unit x) ≡ unit x. Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed. Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y. Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed. 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 10, 2016 115 `````` Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 116 117 `````` Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed. Lemma cmra_extend_op n x y1 y2 : `````` Ralf Jung committed Feb 10, 2016 118 119 `````` ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }. `````` Robbert Krebbers committed Jan 14, 2016 120 121 122 `````` Proof. apply (cmra_extend_mixin A). Qed. End cmra_mixin. `````` Robbert Krebbers committed Feb 01, 2016 123 124 125 126 127 128 129 130 ``````(** * CMRAs with a global identity element *) (** We use the notation ∅ because for most instances (maps, sets, etc) the `empty' element is the global identity. *) Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := { cmra_empty_valid : ✓ ∅; cmra_empty_left_id :> LeftId (≡) ∅ (⋅); cmra_empty_timeless :> Timeless ∅ }. `````` Robbert Krebbers committed Jan 14, 2016 131 `````` `````` Robbert Krebbers committed Jan 16, 2016 132 ``````(** * Morphisms *) `````` Robbert Krebbers committed Jan 14, 2016 133 134 135 136 137 ``````Class CMRAMonotone {A B : cmraT} (f : A → B) := { includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y; validN_preserving n x : ✓{n} x → ✓{n} (f x) }. `````` Robbert Krebbers committed Feb 01, 2016 138 ``````(** * Frame preserving updates *) `````` Robbert Krebbers committed Jan 14, 2016 139 ``````Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n, `````` Robbert Krebbers committed Feb 10, 2016 140 `````` ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). `````` Robbert Krebbers committed Feb 02, 2016 141 ``````Instance: Params (@cmra_updateP) 1. `````` Ralf Jung committed Feb 03, 2016 142 ``````Infix "~~>:" := cmra_updateP (at level 70). `````` Robbert Krebbers committed Jan 14, 2016 143 ``````Definition cmra_update {A : cmraT} (x y : A) := ∀ z n, `````` Robbert Krebbers committed Feb 10, 2016 144 `````` ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). `````` Ralf Jung committed Feb 03, 2016 145 ``````Infix "~~>" := cmra_update (at level 70). `````` Robbert Krebbers committed Feb 02, 2016 146 ``````Instance: Params (@cmra_update) 1. `````` Robbert Krebbers committed Nov 22, 2015 147 `````` `````` Robbert Krebbers committed Jan 16, 2016 148 ``````(** * Properties **) `````` Robbert Krebbers committed Nov 11, 2015 149 ``````Section cmra. `````` Robbert Krebbers committed Jan 14, 2016 150 ``````Context {A : cmraT}. `````` Robbert Krebbers committed Nov 11, 2015 151 ``````Implicit Types x y z : A. `````` Robbert Krebbers committed Feb 01, 2016 152 ``````Implicit Types xs ys zs : list A. `````` Robbert Krebbers committed Nov 11, 2015 153 `````` `````` Robbert Krebbers committed Feb 01, 2016 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 ``````(** ** Setoids *) Global Instance cmra_unit_proper : Proper ((≡) ==> (≡)) (@unit A _). 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. by rewrite Hy (commutative _ x1) Hx (commutative _ y2). 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_minus_proper : Proper ((≡) ==> (≡) ==> (≡)) (@minus A _). Proof. apply (ne_proper_2 _). Qed. Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _). Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed. 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 191 192 193 194 195 196 197 198 199 200 201 ``````Global Instance cmra_update_proper : Proper ((≡) ==> (≡) ==> iff) (@cmra_update A). Proof. intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto. Qed. Global Instance cmra_updateP_proper : Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A). Proof. intros x1 x2 Hx P1 P2 HP; split=>Hup z n; [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 `````` (** ** Validity *) Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x. Proof. done. Qed. Lemma cmra_validN_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x. 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. Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y. Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed. Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y. Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed. (** ** Units *) Lemma cmra_unit_r x : x ⋅ unit x ≡ x. Proof. by rewrite (commutative _ x) cmra_unit_l. Qed. Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x. Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed. Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} (unit x). Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed. Lemma cmra_unit_valid x : ✓ x → ✓ (unit x). Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed. (** ** Order *) `````` Robbert Krebbers committed Nov 20, 2015 226 227 228 229 230 231 ``````Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y. Proof. split; [by intros [z Hz] n; exists z; rewrite Hz|]. intros Hxy; exists (y ⩪ x); apply equiv_dist; intros n. symmetry; apply cmra_op_minus, Hxy. Qed. `````` Robbert Krebbers committed Feb 01, 2016 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 ``````Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n). Proof. split. * by intros x; exists (unit x); rewrite cmra_unit_r. * intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite (associative _) -Hy -Hz. Qed. Global Instance cmra_included_preorder: PreOrder (@included A _ _). Proof. split; red; intros until 0; rewrite !cmra_included_includedN; first done. intros; etransitivity; eauto. Qed. Lemma cmra_validN_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x. Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed. Lemma cmra_validN_included x y n : ✓{n} y → x ≼ y → ✓{n} x. Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed. Lemma cmra_includedN_S x y n : x ≼{S n} y → x ≼{n} y. Proof. by intros [z Hz]; exists z; apply dist_S. Qed. Lemma cmra_includedN_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y. 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. Proof. rewrite (commutative op); apply cmra_includedN_l. Qed. Lemma cmra_included_r x y : y ≼ x ⋅ y. Proof. rewrite (commutative op); apply cmra_included_l. Qed. `````` Robbert Krebbers committed Nov 20, 2015 262 `````` `````` Robbert Krebbers committed Feb 01, 2016 263 264 265 266 267 268 269 270 271 272 ``````Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y. Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed. Lemma cmra_included_unit x : unit x ≼ x. Proof. by exists x; rewrite cmra_unit_l. Qed. Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y. Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed. Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z. Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed. Lemma cmra_included_dist_l x1 x2 x1' n : `````` Ralf Jung committed Feb 10, 2016 273 `````` x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. `````` Robbert Krebbers committed Nov 11, 2015 274 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 275 276 `````` intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l. by rewrite Hx1 Hx2. `````` Robbert Krebbers committed Nov 11, 2015 277 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 278 279 280 `````` (** ** Minus *) Lemma cmra_op_minus' x y : x ≼ y → x ⋅ y ⩪ x ≡ y. `````` Robbert Krebbers committed Nov 11, 2015 281 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 282 `````` rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus. `````` Robbert Krebbers committed Nov 11, 2015 283 ``````Qed. `````` Robbert Krebbers committed Dec 11, 2015 284 `````` `````` Robbert Krebbers committed Jan 16, 2016 285 ``````(** ** Timeless *) `````` Robbert Krebbers committed Feb 10, 2016 286 ``````Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y. `````` Robbert Krebbers committed Dec 11, 2015 287 288 ``````Proof. intros ?? [x' ?]. `````` Robbert Krebbers committed Feb 10, 2016 289 `````` destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. `````` Robbert Krebbers committed Jan 13, 2016 290 `````` by exists z'; rewrite Hy (timeless x z). `````` Robbert Krebbers committed Dec 11, 2015 291 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 292 ``````Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y. `````` Robbert Krebbers committed Dec 11, 2015 293 ``````Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed. `````` Robbert Krebbers committed Jan 14, 2016 294 ``````Lemma cmra_op_timeless x1 x2 : `````` Robbert Krebbers committed Dec 11, 2015 295 `````` ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). `````` Robbert Krebbers committed Nov 18, 2015 296 297 ``````Proof. intros ??? z Hz. `````` Robbert Krebbers committed Feb 10, 2016 298 `````` destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. `````` Robbert Krebbers committed Feb 01, 2016 299 `````` { by rewrite -?Hz. } `````` Robbert Krebbers committed Jan 13, 2016 300 `````` by rewrite Hz' (timeless x1 y1) // (timeless x2 y2). `````` Robbert Krebbers committed Nov 18, 2015 301 ``````Qed. `````` Robbert Krebbers committed Nov 20, 2015 302 `````` `````` Robbert Krebbers committed Feb 01, 2016 303 304 305 306 307 308 309 310 311 312 313 314 ``````(** ** RAs with an empty element *) Section identity. Context `{Empty A, !CMRAIdentity A}. Lemma cmra_empty_leastN n x : ∅ ≼{n} x. Proof. by exists x; rewrite left_id. Qed. Lemma cmra_empty_least x : ∅ ≼ x. Proof. by exists x; rewrite left_id. Qed. Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅). Proof. by intros x; rewrite (commutative op) left_id. Qed. Lemma cmra_unit_empty : unit ∅ ≡ ∅. Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed. End identity. `````` Robbert Krebbers committed Nov 20, 2015 315 `````` `````` Robbert Krebbers committed Feb 01, 2016 316 ``````(** ** Updates *) `````` Robbert Krebbers committed Jan 14, 2016 317 ``````Global Instance cmra_update_preorder : PreOrder (@cmra_update A). `````` Robbert Krebbers committed Nov 22, 2015 318 ``````Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed. `````` Ralf Jung committed Feb 03, 2016 319 ``````Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). `````` Robbert Krebbers committed Nov 22, 2015 320 321 322 323 324 ``````Proof. split. * by intros Hx z ?; exists y; split; [done|apply (Hx z)]. * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?). Qed. `````` Ralf Jung committed Feb 03, 2016 325 ``````Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. `````` Robbert Krebbers committed Feb 02, 2016 326 ``````Proof. by intros ? z n ?; exists x. Qed. `````` Robbert Krebbers committed Feb 02, 2016 327 ``````Lemma cmra_updateP_compose (P Q : A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 328 `````` x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 329 330 331 ``````Proof. intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y). Qed. `````` Robbert Krebbers committed Feb 08, 2016 332 333 334 335 336 ``````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 337 ``````Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 338 ``````Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. `````` Robbert Krebbers committed Feb 02, 2016 339 `````` `````` Robbert Krebbers committed Feb 02, 2016 340 ``````Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 341 `````` x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 342 343 344 345 346 347 348 ``````Proof. intros Hx1 Hx2 Hy z n ?. destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite associative. destruct (Hx2 (y1 ⋅ z) n) as (y2&?&?); first by rewrite associative (commutative _ x2) -associative. exists (y1 ⋅ y2); split; last rewrite (commutative _ y1) -associative; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 349 ``````Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 350 `````` x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. `````` Robbert Krebbers committed Feb 02, 2016 351 ``````Proof. eauto 10 using cmra_updateP_op. Qed. `````` Ralf Jung committed Feb 03, 2016 352 ``````Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2. `````` Robbert Krebbers committed Feb 02, 2016 353 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 354 `````` rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. `````` Robbert Krebbers committed Feb 02, 2016 355 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 356 357 358 359 360 361 362 363 `````` Section identity_updates. Context `{Empty A, !CMRAIdentity A}. Lemma cmra_update_empty x : x ~~> ∅. Proof. intros z n; rewrite left_id; apply cmra_validN_op_r. Qed. Lemma cmra_update_empty_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y. Proof. split; [intros; transitivity ∅|]; auto using cmra_update_empty. Qed. End identity_updates. `````` Robbert Krebbers committed Nov 11, 2015 364 365 ``````End cmra. `````` Robbert Krebbers committed Feb 01, 2016 366 ``````(** * Properties about monotone functions *) `````` Robbert Krebbers committed Jan 14, 2016 367 ``````Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A). `````` Robbert Krebbers committed Nov 16, 2015 368 ``````Proof. by split. Qed. `````` Robbert Krebbers committed Feb 01, 2016 369 370 ``````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 371 372 ``````Proof. split. `````` Robbert Krebbers committed Feb 01, 2016 373 374 `````` * move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving. * move=> n x Hx /=. by apply validN_preserving, validN_preserving. `````` Robbert Krebbers committed Nov 20, 2015 375 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 376 `````` `````` Robbert Krebbers committed Feb 01, 2016 377 378 379 380 381 382 383 384 385 386 ``````Section cmra_monotone. Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}. Lemma included_preserving x y : x ≼ y → f x ≼ f y. Proof. rewrite !cmra_included_includedN; eauto using includedN_preserving. Qed. Lemma valid_preserving x : ✓ x → ✓ (f x). Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed. End cmra_monotone. `````` 387 `````` `````` Robbert Krebbers committed Feb 08, 2016 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 ``````(** * 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. Lemma cmra_transport_unit x : T (unit x) = unit (T x). Proof. by destruct H. Qed. Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x. Proof. by destruct H. Qed. Lemma cmra_transport_valid x : ✓ (T x) ↔ ✓ x. 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 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 ``````(** * Instances *) (** ** Discrete CMRA *) Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := { (* setoids *) ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x); ra_unit_ne :> Proper ((≡) ==> (≡)) unit; ra_validN_ne :> Proper ((≡) ==> impl) ✓; ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus; (* monoid *) ra_associative :> Associative (≡) (⋅); ra_commutative :> Commutative (≡) (⋅); ra_unit_l x : unit x ⋅ x ≡ x; ra_unit_idempotent x : unit (unit x) ≡ unit x; ra_unit_preserving x y : x ≼ y → unit x ≼ unit y; ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x; ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y }. `````` Robbert Krebbers committed Nov 16, 2015 435 ``````Section discrete. `````` Robbert Krebbers committed Feb 01, 2016 436 437 438 `````` Context {A : cofeT} `{∀ x : A, Timeless x}. Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A). `````` Robbert Krebbers committed Feb 10, 2016 439 `````` Instance discrete_validN : ValidN A := λ n x, ✓ x. `````` Robbert Krebbers committed Jan 14, 2016 440 `````` Definition discrete_cmra_mixin : CMRAMixin A. `````` Robbert Krebbers committed Nov 16, 2015 441 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 442 443 `````` by destruct ra; split; unfold Proper, respectful, includedN; try setoid_rewrite <-(timeless_iff _ _ _ _). `````` Robbert Krebbers committed Nov 16, 2015 444 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 445 `````` Definition discrete_extend_mixin : CMRAExtendMixin A. `````` Robbert Krebbers committed Nov 16, 2015 446 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 447 448 `````` intros n x y1 y2 ??; exists (y1,y2); split_ands; auto. apply (timeless _), dist_le with n; auto with lia. `````` Robbert Krebbers committed Nov 16, 2015 449 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 450 `````` Definition discreteRA : cmraT := `````` Robbert Krebbers committed Feb 01, 2016 451 `````` CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin. `````` Robbert Krebbers committed Feb 02, 2016 452 `````` Lemma discrete_updateP (x : discreteRA) (P : A → Prop) : `````` Ralf Jung committed Feb 03, 2016 453 `````` (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P. `````` Robbert Krebbers committed Feb 02, 2016 454 `````` Proof. intros Hvalid z n; apply Hvalid. Qed. `````` Robbert Krebbers committed Feb 02, 2016 455 `````` Lemma discrete_update (x y : discreteRA) : `````` Ralf Jung committed Feb 03, 2016 456 `````` (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. `````` Robbert Krebbers committed Feb 02, 2016 457 `````` Proof. intros Hvalid z n; apply Hvalid. Qed. `````` Robbert Krebbers committed Nov 16, 2015 458 459 ``````End discrete. `````` Robbert Krebbers committed Feb 01, 2016 460 461 462 463 464 465 466 467 468 469 470 471 472 473 ``````(** ** CMRA for the unit type *) Section unit. Instance unit_valid : Valid () := λ x, True. Instance unit_unit : Unit () := λ x, x. Instance unit_op : Op () := λ x y, (). Instance unit_minus : Minus () := λ x y, (). Global Instance unit_empty : Empty () := (). Definition unit_ra : RA (). Proof. by split. Qed. Canonical Structure unitRA : cmraT := Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra. Global Instance unit_cmra_identity : CMRAIdentity unitRA. Proof. by split; intros []. Qed. End unit. `````` Ralf Jung committed Jan 19, 2016 474 `````` `````` Robbert Krebbers committed Feb 01, 2016 475 ``````(** ** Product *) `````` Robbert Krebbers committed Jan 14, 2016 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 ``````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) := (∅, ∅). Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)). Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} (x.1) ∧ ✓{n} (x.2). Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2). 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 _. * 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]; split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2. `````` Robbert Krebbers committed Feb 01, 2016 501 `````` * by intros n x [??]; split; apply cmra_validN_S. `````` Robbert Krebbers committed Jan 14, 2016 502 503 `````` * split; simpl; apply (associative _). * split; simpl; apply (commutative _). `````` Robbert Krebbers committed Feb 01, 2016 504 505 `````` * split; simpl; apply cmra_unit_l. * split; simpl; apply cmra_unit_idempotent. `````` Robbert Krebbers committed Jan 14, 2016 506 `````` * intros n x y; rewrite !prod_includedN. `````` Robbert Krebbers committed Feb 01, 2016 507 508 `````` by intros [??]; split; apply cmra_unit_preservingN. * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. `````` Robbert Krebbers committed Jan 14, 2016 509 510 511 512 513 514 515 516 517 518 519 520 `````` * intros x y n; rewrite prod_includedN; intros [??]. by split; apply cmra_op_minus. Qed. Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B). Proof. intros n x y1 y2 [??] [??]; simpl in *. destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto. destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto. by exists ((z1.1,z2.1),(z1.2,z2.2)). Qed. Canonical Structure prodRA : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin. `````` Robbert Krebbers committed Feb 01, 2016 521 522 523 524 525 526 527 528 `````` Global Instance prod_cmra_identity `{Empty A, Empty B} : CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodRA. Proof. split. * split; apply cmra_empty_valid. * by split; rewrite /=left_id. * by intros ? [??]; split; apply (timeless _). Qed. `````` Ralf Jung committed Feb 03, 2016 529 `````` Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. `````` Robbert Krebbers committed Feb 02, 2016 530 `````` Proof. intros ?? z n [??]; split; simpl in *; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 531 `````` Lemma prod_updateP P1 P2 (Q : A * B → Prop) x : `````` Ralf Jung committed Feb 03, 2016 532 `````` x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 533 534 535 536 537 `````` Proof. intros Hx1 Hx2 HP z n [??]; simpl in *. destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto. exists (a,b); repeat split; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 538 `````` Lemma prod_updateP' P1 P2 x : `````` Ralf Jung committed Feb 03, 2016 539 `````` x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2). `````` Robbert Krebbers committed Feb 02, 2016 540 `````` Proof. eauto using prod_updateP. Qed. `````` Robbert Krebbers committed Jan 14, 2016 541 542 543 544 545 ``````End prod. Arguments prodRA : clear implicits. 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 546 547 ``````Proof. split. `````` Robbert Krebbers committed Jan 14, 2016 548 `````` * intros n x y; rewrite !prod_includedN; intros [??]; simpl. `````` Robbert Krebbers committed Nov 20, 2015 549 `````` by split; apply includedN_preserving. `````` Robbert Krebbers committed Nov 16, 2015 550 551 `````` * by intros n x [??]; split; simpl; apply validN_preserving. Qed.``````