cmra.v 23 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 44 mixin_cmra_validN_0 x : ✓{0} x; mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; Robbert Krebbers committed Nov 11, 2015 45 (* monoid *) Robbert Krebbers committed Jan 14, 2016 46 47 48 49 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 50 51 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 52 mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y Robbert Krebbers committed Nov 11, 2015 53 }. Robbert Krebbers committed Jan 14, 2016 54 Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2, Ralf Jung committed Feb 10, 2016 55 56 ✓{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 57 Robbert Krebbers committed Nov 11, 2015 58 59 60 61 62 63 64 65 66 67 (** 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 68 69 70 cmra_cofe_mixin : CofeMixin cmra_car; cmra_mixin : CMRAMixin cmra_car; cmra_extend_mixin : CMRAExtendMixin cmra_car Robbert Krebbers committed Nov 11, 2015 71 }. Robbert Krebbers committed Feb 01, 2016 72 Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _. Robbert Krebbers committed Jan 14, 2016 73 74 75 76 77 78 79 80 81 82 83 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 84 Add Printing Constructor cmraT. Robbert Krebbers committed Feb 01, 2016 85 Existing Instances cmra_unit cmra_op cmra_validN cmra_minus. Robbert Krebbers committed Jan 14, 2016 86 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A). Robbert Krebbers committed Nov 11, 2015 87 88 Canonical Structure cmra_cofeC. Robbert Krebbers committed Jan 14, 2016 89 90 91 92 93 94 95 96 (** 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 97 98 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 99 100 101 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 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 Lemma cmra_validN_0 x : ✓{0} x. Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed. 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 118 Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y. Robbert Krebbers committed Jan 14, 2016 119 120 Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed. Lemma cmra_extend_op n x y1 y2 : Ralf Jung committed Feb 10, 2016 121 122 ✓{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 123 124 125 Proof. apply (cmra_extend_mixin A). Qed. End cmra_mixin. Robbert Krebbers committed Feb 01, 2016 126 127 128 129 130 131 132 133 134 135 Hint Extern 0 (✓{0} _) => apply cmra_validN_0. (** * 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 136 Robbert Krebbers committed Jan 16, 2016 137 (** * Morphisms *) Robbert Krebbers committed Jan 14, 2016 138 139 140 141 142 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 143 (** * Frame preserving updates *) Robbert Krebbers committed Jan 14, 2016 144 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n, Robbert Krebbers committed Feb 02, 2016 145 ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z). Robbert Krebbers committed Feb 02, 2016 146 Instance: Params (@cmra_updateP) 1. Ralf Jung committed Feb 03, 2016 147 Infix "~~>:" := cmra_updateP (at level 70). Robbert Krebbers committed Jan 14, 2016 148 Definition cmra_update {A : cmraT} (x y : A) := ∀ z n, Robbert Krebbers committed Feb 02, 2016 149 ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z). Ralf Jung committed Feb 03, 2016 150 Infix "~~>" := cmra_update (at level 70). Robbert Krebbers committed Feb 02, 2016 151 Instance: Params (@cmra_update) 1. Robbert Krebbers committed Nov 22, 2015 152 Robbert Krebbers committed Jan 16, 2016 153 (** * Properties **) Robbert Krebbers committed Nov 11, 2015 154 Section cmra. Robbert Krebbers committed Jan 14, 2016 155 Context {A : cmraT}. Robbert Krebbers committed Nov 11, 2015 156 Implicit Types x y z : A. Robbert Krebbers committed Feb 01, 2016 157 Implicit Types xs ys zs : list A. Robbert Krebbers committed Nov 11, 2015 158 Robbert Krebbers committed Feb 01, 2016 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 191 192 193 194 195 (** ** 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 196 197 198 199 200 201 202 203 204 205 206 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 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 (** ** 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 231 232 233 234 235 236 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 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 262 263 264 265 266 267 268 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_0 x y : x ≼{0} y. Proof. by exists (unit x). 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 269 Robbert Krebbers committed Feb 01, 2016 270 271 272 273 274 275 276 277 278 279 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 280 x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. Robbert Krebbers committed Nov 11, 2015 281 Proof. Robbert Krebbers committed Feb 01, 2016 282 283 intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l. by rewrite Hx1 Hx2. Robbert Krebbers committed Nov 11, 2015 284 Qed. Robbert Krebbers committed Feb 01, 2016 285 286 287 (** ** Minus *) Lemma cmra_op_minus' x y : x ≼ y → x ⋅ y ⩪ x ≡ y. Robbert Krebbers committed Nov 11, 2015 288 Proof. Robbert Krebbers committed Feb 01, 2016 289 rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus. Robbert Krebbers committed Nov 11, 2015 290 Qed. Robbert Krebbers committed Dec 11, 2015 291 Robbert Krebbers committed Jan 16, 2016 292 (** ** Timeless *) Robbert Krebbers committed Jan 14, 2016 293 Lemma cmra_timeless_included_l x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y. Robbert Krebbers committed Dec 11, 2015 294 295 296 Proof. intros ?? [x' ?]. destruct (cmra_extend_op 1 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 299 300 Qed. Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{1} y → x ≼{n} y. 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 Nov 20, 2015 305 destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. Robbert Krebbers committed Feb 01, 2016 306 { by rewrite -?Hz. } 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 01, 2016 310 311 312 313 314 315 316 317 318 319 320 321 (** ** 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 322 Robbert Krebbers committed Feb 01, 2016 323 (** ** Updates *) Robbert Krebbers committed Jan 14, 2016 324 Global Instance cmra_update_preorder : PreOrder (@cmra_update A). Robbert Krebbers committed Nov 22, 2015 325 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed. Ralf Jung committed Feb 03, 2016 326 Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). Robbert Krebbers committed Nov 22, 2015 327 328 329 330 331 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 332 Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. Robbert Krebbers committed Feb 02, 2016 333 Proof. by intros ? z n ?; exists x. Qed. Robbert Krebbers committed Feb 02, 2016 334 Lemma cmra_updateP_compose (P Q : A → Prop) x : Ralf Jung committed Feb 03, 2016 335 x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. Robbert Krebbers committed Feb 02, 2016 336 337 338 Proof. intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y). Qed. Robbert Krebbers committed Feb 08, 2016 339 340 341 342 343 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 344 Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q. Robbert Krebbers committed Feb 02, 2016 345 Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. Robbert Krebbers committed Feb 02, 2016 346 Robbert Krebbers committed Feb 02, 2016 347 Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : Ralf Jung committed Feb 03, 2016 348 x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. Robbert Krebbers committed Feb 02, 2016 349 350 351 352 353 354 355 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 356 Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : Ralf Jung committed Feb 03, 2016 357 x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. Robbert Krebbers committed Feb 02, 2016 358 Proof. eauto 10 using cmra_updateP_op. Qed. Ralf Jung committed Feb 03, 2016 359 Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2. Robbert Krebbers committed Feb 02, 2016 360 Proof. Robbert Krebbers committed Feb 02, 2016 361 rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. Robbert Krebbers committed Feb 02, 2016 362 Qed. Robbert Krebbers committed Feb 08, 2016 363 364 365 366 367 368 369 370 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 371 372 End cmra. Robbert Krebbers committed Feb 01, 2016 373 Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0. Robbert Krebbers committed Jan 16, 2016 374 Robbert Krebbers committed Feb 01, 2016 375 (** * Properties about monotone functions *) Robbert Krebbers committed Jan 14, 2016 376 Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A). Robbert Krebbers committed Nov 16, 2015 377 Proof. by split. Qed. Robbert Krebbers committed Feb 01, 2016 378 379 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 380 381 Proof. split. Robbert Krebbers committed Feb 01, 2016 382 383 * 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 384 Qed. Robbert Krebbers committed Nov 16, 2015 385 Robbert Krebbers committed Feb 01, 2016 386 387 388 389 390 391 392 393 394 395 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. Robbert Krebbers committed Feb 08, 2016 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 (** * 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 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 (** * 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 443 Section discrete. Robbert Krebbers committed Feb 01, 2016 444 445 446 Context {A : cofeT} `{∀ x : A, Timeless x}. Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A). Robbert Krebbers committed Nov 16, 2015 447 Instance discrete_validN : ValidN A := λ n x, Robbert Krebbers committed Nov 23, 2015 448 match n with 0 => True | S n => ✓ x end. Robbert Krebbers committed Jan 14, 2016 449 Definition discrete_cmra_mixin : CMRAMixin A. Robbert Krebbers committed Nov 16, 2015 450 Proof. Robbert Krebbers committed Feb 01, 2016 451 452 453 454 455 destruct ra; split; unfold Proper, respectful, includedN; repeat match goal with | |- ∀ n : nat, _ => intros [|?] end; try setoid_rewrite <-(timeless_S _ _ _ _); try done. by intros x y ?; exists x. Robbert Krebbers committed Nov 16, 2015 456 Qed. Robbert Krebbers committed Jan 14, 2016 457 Definition discrete_extend_mixin : CMRAExtendMixin A. Robbert Krebbers committed Nov 16, 2015 458 Proof. Robbert Krebbers committed Feb 01, 2016 459 460 461 462 intros [|n] x y1 y2 ??. * by exists (unit x, x); rewrite /= ra_unit_l. * exists (y1,y2); split_ands; auto. apply (timeless _), dist_le with (S n); auto with lia. Robbert Krebbers committed Nov 16, 2015 463 Qed. Robbert Krebbers committed Jan 14, 2016 464 Definition discreteRA : cmraT := Robbert Krebbers committed Feb 01, 2016 465 CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin. Robbert Krebbers committed Feb 02, 2016 466 Lemma discrete_updateP (x : discreteRA) (P : A → Prop) : Ralf Jung committed Feb 03, 2016 467 (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P. Robbert Krebbers committed Feb 02, 2016 468 Proof. intros Hvalid z n; apply Hvalid. Qed. Robbert Krebbers committed Feb 02, 2016 469 Lemma discrete_update (x y : discreteRA) : Ralf Jung committed Feb 03, 2016 470 (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. Robbert Krebbers committed Feb 02, 2016 471 Proof. intros Hvalid z n; apply Hvalid. Qed. Robbert Krebbers committed Nov 16, 2015 472 473 End discrete. Robbert Krebbers committed Feb 01, 2016 474 475 476 477 478 479 480 481 482 483 484 485 486 487 (** ** 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 488 Robbert Krebbers committed Feb 01, 2016 489 (** ** Product *) Robbert Krebbers committed Jan 14, 2016 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 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 515 516 * by split. * by intros n x [??]; split; apply cmra_validN_S. Robbert Krebbers committed Jan 14, 2016 517 518 * split; simpl; apply (associative _). * split; simpl; apply (commutative _). Robbert Krebbers committed Feb 01, 2016 519 520 * split; simpl; apply cmra_unit_l. * split; simpl; apply cmra_unit_idempotent. Robbert Krebbers committed Jan 14, 2016 521 * intros n x y; rewrite !prod_includedN. Robbert Krebbers committed Feb 01, 2016 522 523 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 524 525 526 527 528 529 530 531 532 533 534 535 * 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 536 537 538 539 540 541 542 543 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 544 Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. Robbert Krebbers committed Feb 02, 2016 545 Proof. intros ?? z n [??]; split; simpl in *; auto. Qed. Robbert Krebbers committed Feb 02, 2016 546 Lemma prod_updateP P1 P2 (Q : A * B → Prop) x : Ralf Jung committed Feb 03, 2016 547 x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q. Robbert Krebbers committed Feb 02, 2016 548 549 550 551 552 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 553 Lemma prod_updateP' P1 P2 x : Ralf Jung committed Feb 03, 2016 554 x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2). Robbert Krebbers committed Feb 02, 2016 555 Proof. eauto using prod_updateP. Qed. Robbert Krebbers committed Jan 14, 2016 556 557 558 559 560 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 561 562 Proof. split. Robbert Krebbers committed Jan 14, 2016 563 * intros n x y; rewrite !prod_includedN; intros [??]; simpl. Robbert Krebbers committed Nov 20, 2015 564 by split; apply includedN_preserving. Robbert Krebbers committed Nov 16, 2015 565 566 * by intros n x [??]; split; simpl; apply validN_preserving. Qed.