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