cmra.v 13 KB
 Robbert Krebbers committed Dec 15, 2015 1 ``````Require Export modures.ra modures.cofe. `````` Robbert Krebbers committed Nov 11, 2015 2 3 4 `````` Class ValidN (A : Type) := validN : nat → A → Prop. Instance: Params (@validN) 3. `````` Robbert Krebbers committed Nov 23, 2015 5 ``````Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }"). `````` Robbert Krebbers committed Nov 11, 2015 6 `````` `````` Robbert Krebbers committed Nov 20, 2015 7 8 9 10 ``````Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ z. Notation "x ≼{ n } y" := (includedN n x y) (at level 70, format "x ≼{ n } y") : C_scope. Instance: Params (@includedN) 4. `````` Robbert Krebbers committed Nov 22, 2015 11 ``````Hint Extern 0 (?x ≼{_} ?x) => reflexivity. `````` Robbert Krebbers committed Nov 20, 2015 12 13 `````` Class CMRA A `{Equiv A, Compl A, Unit A, Op A, Valid A, ValidN A, Minus A} := { `````` Robbert Krebbers committed Nov 11, 2015 14 15 16 17 `````` (* setoids *) cmra_cofe :> Cofe A; cmra_op_ne n x :> Proper (dist n ==> dist n) (op x); cmra_unit_ne n :> Proper (dist n ==> dist n) unit; `````` Robbert Krebbers committed Nov 23, 2015 18 `````` cmra_valid_ne n :> Proper (dist n ==> impl) (✓{n}); `````` Robbert Krebbers committed Nov 11, 2015 19 20 `````` cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus; (* valid *) `````` Robbert Krebbers committed Nov 23, 2015 21 22 23 `````` cmra_valid_0 x : ✓{0} x; cmra_valid_S n x : ✓{S n} x → ✓{n} x; cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; `````` Robbert Krebbers committed Nov 11, 2015 24 25 26 27 28 `````` (* monoid *) cmra_associative : Associative (≡) (⋅); cmra_commutative : Commutative (≡) (⋅); cmra_unit_l x : unit x ⋅ x ≡ x; cmra_unit_idempotent x : unit (unit x) ≡ unit x; `````` Robbert Krebbers committed Nov 20, 2015 29 `````` cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y; `````` Robbert Krebbers committed Nov 23, 2015 30 `````` cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; `````` Robbert Krebbers committed Nov 20, 2015 31 `````` cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y `````` Robbert Krebbers committed Nov 11, 2015 32 33 ``````}. Class CMRAExtend A `{Equiv A, Dist A, Op A, ValidN A} := `````` Robbert Krebbers committed Nov 20, 2015 34 `````` cmra_extend_op n x y1 y2 : `````` Robbert Krebbers committed Nov 23, 2015 35 `````` ✓{n} x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }. `````` Robbert Krebbers committed Nov 11, 2015 36 `````` `````` Robbert Krebbers committed Nov 20, 2015 37 38 39 ``````Class CMRAMonotone `{Dist A, Op A, ValidN A, Dist B, Op B, ValidN B} (f : A → B) := { includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y; `````` Robbert Krebbers committed Nov 23, 2015 40 `````` validN_preserving n x : ✓{n} x → ✓{n} (f x) `````` Robbert Krebbers committed Nov 11, 2015 41 42 ``````}. `````` Robbert Krebbers committed Nov 23, 2015 43 ``````Hint Extern 0 (✓{0} _) => apply cmra_valid_0. `````` Robbert Krebbers committed Nov 22, 2015 44 `````` `````` Robbert Krebbers committed Nov 11, 2015 45 46 47 48 49 50 51 52 53 54 55 56 57 58 ``````(** 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_valid : Valid cmra_car; cmra_validN : ValidN cmra_car; cmra_minus : Minus cmra_car; cmra_cmra : CMRA cmra_car; cmra_extend : CMRAExtend cmra_car }. `````` Robbert Krebbers committed Nov 20, 2015 59 ``````Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _}. `````` Robbert Krebbers committed Nov 19, 2015 60 61 62 63 64 65 66 67 68 69 ``````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_valid _ _ : simpl never. Arguments cmra_validN _ _ _ : simpl never. Arguments cmra_minus _ _ _ : simpl never. Arguments cmra_cmra _ : simpl never. `````` Robbert Krebbers committed Nov 11, 2015 70 71 ``````Add Printing Constructor cmraT. Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op `````` Robbert Krebbers committed Nov 20, 2015 72 `````` cmra_valid cmra_validN cmra_minus cmra_cmra cmra_extend. `````` Robbert Krebbers committed Nov 11, 2015 73 74 75 ``````Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A. Canonical Structure cmra_cofeC. `````` Robbert Krebbers committed Nov 22, 2015 76 ``````(** Updates *) `````` Robbert Krebbers committed Nov 23, 2015 77 78 ``````Definition cmra_updateP `{Op A, ValidN A} (x : A) (P : A → Prop) := ∀ z n, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). `````` Robbert Krebbers committed Nov 22, 2015 79 80 81 ``````Instance: Params (@cmra_updateP) 3. Infix "⇝:" := cmra_updateP (at level 70). Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n, `````` Robbert Krebbers committed Nov 23, 2015 82 `````` ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). `````` Robbert Krebbers committed Nov 22, 2015 83 84 85 ``````Infix "⇝" := cmra_update (at level 70). Instance: Params (@cmra_update) 3. `````` Robbert Krebbers committed Dec 11, 2015 86 87 88 89 90 ``````(** Timeless elements *) Class ValidTimeless `{Valid A, ValidN A} (x : A) := valid_timeless : validN 1 x → valid x. Arguments valid_timeless {_ _ _} _ {_} _. `````` Robbert Krebbers committed Nov 22, 2015 91 ``````(** Properties **) `````` Robbert Krebbers committed Nov 11, 2015 92 93 94 95 ``````Section cmra. Context `{cmra : CMRA A}. Implicit Types x y z : A. `````` Robbert Krebbers committed Nov 20, 2015 96 97 98 99 100 101 102 ``````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 Nov 23, 2015 103 ``````Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (✓{n}) | 1. `````` Robbert Krebbers committed Nov 11, 2015 104 ``````Proof. by split; apply cmra_valid_ne. Qed. `````` Robbert Krebbers committed Nov 23, 2015 105 ``````Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (✓{n}) | 1. `````` Robbert Krebbers committed Nov 11, 2015 106 107 108 ``````Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed. Global Instance cmra_ra : RA A. Proof. `````` Robbert Krebbers committed Nov 12, 2015 109 110 `````` split; try by (destruct cmra; eauto using ne_proper, ne_proper_2 with typeclass_instances). `````` Robbert Krebbers committed Nov 11, 2015 111 `````` * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite <-Hx. `````` Robbert Krebbers committed Nov 20, 2015 112 113 `````` * intros x y; rewrite !cmra_included_includedN. eauto using cmra_unit_preserving. `````` Robbert Krebbers committed Nov 11, 2015 114 115 `````` * intros x y; rewrite !cmra_valid_validN; intros ? n. by apply cmra_valid_op_l with y. `````` Robbert Krebbers committed Nov 20, 2015 116 117 `````` * intros x y [z Hz]; apply equiv_dist; intros n. by apply cmra_op_minus; exists z; rewrite Hz. `````` Robbert Krebbers committed Nov 11, 2015 118 ``````Qed. `````` Robbert Krebbers committed Nov 23, 2015 119 ``````Lemma cmra_valid_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y. `````` Robbert Krebbers committed Nov 11, 2015 120 ``````Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed. `````` Robbert Krebbers committed Nov 23, 2015 121 ``````Lemma cmra_valid_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x. `````` Robbert Krebbers committed Nov 11, 2015 122 123 124 125 126 127 ``````Proof. induction 2; eauto using cmra_valid_S. Qed. Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (⋅). Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2). Qed. `````` Robbert Krebbers committed Nov 23, 2015 128 ``````Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x). `````` Robbert Krebbers committed Nov 12, 2015 129 ``````Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed. `````` Robbert Krebbers committed Dec 11, 2015 130 131 132 133 134 135 136 137 138 139 140 `````` (* Timeless *) Lemma cmra_timeless_included_l `{!CMRAExtend A} x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y. Proof. intros ?? [x' ?]. destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. by exists z'; rewrite Hy, (timeless x z) by done. 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 Nov 18, 2015 141 ``````Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 : `````` Robbert Krebbers committed Dec 11, 2015 142 `````` ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). `````` Robbert Krebbers committed Nov 18, 2015 143 144 ``````Proof. intros ??? z Hz. `````` Robbert Krebbers committed Nov 20, 2015 145 `````` destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. `````` Robbert Krebbers committed Dec 11, 2015 146 `````` { by rewrite <-?Hz; apply cmra_valid_validN. } `````` Robbert Krebbers committed Nov 18, 2015 147 148 `````` by rewrite Hz', (timeless x1 y1), (timeless x2 y2). Qed. `````` Robbert Krebbers committed Nov 20, 2015 149 150 151 `````` (** * Included *) Global Instance cmra_included_ne n : `````` Robbert Krebbers committed Nov 22, 2015 152 `````` Proper (dist n ==> dist n ==> iff) (includedN n) | 1. `````` Robbert Krebbers committed Nov 20, 2015 153 154 155 156 ``````Proof. intros x x' Hx y y' Hy; unfold includedN. by setoid_rewrite Hx; setoid_rewrite Hy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 157 158 ``````Global Instance cmra_included_proper : Proper ((≡) ==> (≡) ==> iff) (includedN n) | 1. `````` Robbert Krebbers committed Nov 20, 2015 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 ``````Proof. intros n x x' Hx y y' Hy; unfold includedN. by setoid_rewrite Hx; setoid_rewrite Hy. Qed. Lemma cmra_included_0 x y : x ≼{0} y. Proof. by exists (unit x). Qed. Lemma cmra_included_S x y n : x ≼{S n} y → x ≼{n} y. Proof. by intros [z Hz]; exists z; apply dist_S. Qed. Lemma cmra_included_l n x y : x ≼{n} x ⋅ y. Proof. by exists y. Qed. Lemma cmra_included_r n x y : y ≼{n} x ⋅ y. Proof. rewrite (commutative op); apply cmra_included_l. Qed. Global Instance cmra_included_ord n : PreOrder (includedN n). Proof. split. * by intros x; exists (unit x); rewrite ra_unit_r. * intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite (associative _), <-Hy, <-Hz. Qed. `````` Robbert Krebbers committed Nov 23, 2015 179 ``````Lemma cmra_valid_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x. `````` Robbert Krebbers committed Nov 20, 2015 180 ``````Proof. intros Hyv [z Hy]; rewrite Hy in Hyv; eauto using cmra_valid_op_l. Qed. `````` Robbert Krebbers committed Nov 23, 2015 181 ``````Lemma cmra_valid_included x y n : ✓{n} y → x ≼ y → ✓{n} x. `````` Robbert Krebbers committed Nov 20, 2015 182 183 184 185 186 187 188 ``````Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed. Lemma cmra_included_dist_l x1 x2 x1' n : x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2. Proof. intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using ra_included_l. by rewrite Hx1, Hx2. Qed. `````` Robbert Krebbers committed Nov 22, 2015 189 190 191 192 193 194 195 196 197 198 `````` (** * Properties of [(⇝)] relation *) Global Instance cmra_update_preorder : PreOrder cmra_update. Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed. Lemma cmra_update_updateP x y : x ⇝ y ↔ x ⇝: (y =). Proof. split. * by intros Hx z ?; exists y; split; [done|apply (Hx z)]. * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?). Qed. `````` Robbert Krebbers committed Nov 11, 2015 199 200 ``````End cmra. `````` Robbert Krebbers committed Nov 20, 2015 201 ``````Instance cmra_monotone_id `{CMRA A} : CMRAMonotone (@id A). `````` Robbert Krebbers committed Nov 16, 2015 202 ``````Proof. by split. Qed. `````` Robbert Krebbers committed Nov 20, 2015 203 204 205 206 207 208 209 210 211 ``````Instance cmra_monotone_ra_monotone `{CMRA A, CMRA B} (f : A → B) : CMRAMonotone f → RAMonotone f. Proof. split. * intros x y; rewrite !cmra_included_includedN. by intros ? n; apply includedN_preserving. * intros x; rewrite !cmra_valid_validN. by intros ? n; apply validN_preserving. Qed. `````` Robbert Krebbers committed Nov 16, 2015 212 `````` `````` Robbert Krebbers committed Nov 22, 2015 213 ``````Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0. `````` Robbert Krebbers committed Nov 11, 2015 214 215 ``````(* Also via [cmra_cofe; cofe_equivalence] *) Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances. `````` Robbert Krebbers committed Nov 16, 2015 216 217 218 219 220 221 222 `````` (** Discrete *) Section discrete. Context `{ra : RA A}. Existing Instances discrete_dist discrete_compl. Let discrete_cofe' : Cofe A := discrete_cofe. Instance discrete_validN : ValidN A := λ n x, `````` Robbert Krebbers committed Nov 23, 2015 223 `````` match n with 0 => True | S n => ✓ x end. `````` Robbert Krebbers committed Nov 16, 2015 224 225 226 227 228 229 230 231 232 `````` Instance discrete_cmra : CMRA A. Proof. split; try by (destruct ra; auto). * by intros [|n]; try apply ra_op_proper. * by intros [|n]; try apply ra_unit_proper. * by intros [|n]; try apply ra_valid_proper. * by intros [|n]; try apply ra_minus_proper. * by intros [|n]. * intros x; split; intros Hvalid. by intros [|n]. apply (Hvalid 1). `````` Robbert Krebbers committed Nov 20, 2015 233 `````` * by intros [|n]; try apply ra_unit_preserving. `````` Robbert Krebbers committed Nov 16, 2015 234 `````` * by intros [|n]; try apply ra_valid_op_l. `````` Robbert Krebbers committed Nov 20, 2015 235 `````` * by intros [|n] x y; try apply ra_op_minus. `````` Robbert Krebbers committed Nov 16, 2015 236 237 238 `````` Qed. Instance discrete_extend : CMRAExtend A. Proof. `````` Robbert Krebbers committed Nov 20, 2015 239 `````` intros [|n] x y1 y2 ??; [|by exists (y1,y2)]. `````` Robbert Krebbers committed Nov 16, 2015 240 241 `````` by exists (x,unit x); simpl; rewrite ra_unit_r. Qed. `````` Robbert Krebbers committed Dec 11, 2015 242 243 `````` Global Instance discrete_timeless (x : A) : ValidTimeless x. Proof. by intros ?. Qed. `````` Robbert Krebbers committed Nov 20, 2015 244 `````` Definition discreteRA : cmraT := CMRAT A. `````` Robbert Krebbers committed Nov 22, 2015 245 `````` Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} : `````` Robbert Krebbers committed Nov 23, 2015 246 `````` (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ⇝: P. `````` Robbert Krebbers committed Nov 22, 2015 247 248 249 250 `````` Proof. intros Hvalid z [|n]; [|apply Hvalid]. by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y. Qed. `````` Robbert Krebbers committed Nov 23, 2015 251 `````` Lemma discrete_update (x y : A) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ⇝ y. `````` Robbert Krebbers committed Nov 22, 2015 252 `````` Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed. `````` Robbert Krebbers committed Nov 16, 2015 253 ``````End discrete. `````` Robbert Krebbers committed Nov 20, 2015 254 ``````Arguments discreteRA _ {_ _ _ _ _ _}. `````` Robbert Krebbers committed Nov 16, 2015 255 256 257 258 259 260 261 `````` (** Product *) Instance prod_op `{Op A, Op B} : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2). Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅). Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := λ x, (unit (x.1), unit (x.2)). Instance prod_valid `{Valid A, Valid B} : Valid (A * B) := λ x, `````` Robbert Krebbers committed Nov 23, 2015 262 `````` ✓ (x.1) ∧ ✓ (x.2). `````` Robbert Krebbers committed Nov 16, 2015 263 ``````Instance prod_validN `{ValidN A, ValidN B} : ValidN (A * B) := λ n x, `````` Robbert Krebbers committed Nov 23, 2015 264 `````` ✓{n} (x.1) ∧ ✓{n} (x.2). `````` Robbert Krebbers committed Nov 16, 2015 265 266 ``````Instance prod_minus `{Minus A, Minus B} : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2). `````` Robbert Krebbers committed Nov 20, 2015 267 268 269 270 271 272 273 274 275 276 277 278 ``````Lemma prod_included `{Equiv A, Equiv B, Op A, Op B} (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 `{Dist A, Dist B, Op A, Op B} (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. `````` Robbert Krebbers committed Nov 16, 2015 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 ``````Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B). Proof. split; try apply _. * by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1, ?Hy2. * by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1, ?Hy2. * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite <-?Hy1, <-?Hy2. * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hx1, ?Hx2, ?Hy1, ?Hy2. * split; apply cmra_valid_0. * by intros n x [??]; split; apply cmra_valid_S. * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|]. intros Hvalid; split; apply cmra_valid_validN; intros n; apply Hvalid. * split; simpl; apply (associative _). * split; simpl; apply (commutative _). * split; simpl; apply ra_unit_l. * split; simpl; apply ra_unit_idempotent. `````` Robbert Krebbers committed Nov 20, 2015 295 296 `````` * intros n x y; rewrite !prod_includedN. by intros [??]; split; apply cmra_unit_preserving. `````` Robbert Krebbers committed Nov 16, 2015 297 `````` * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto. `````` Robbert Krebbers committed Nov 20, 2015 298 299 `````` * intros x y n; rewrite prod_includedN; intros [??]. by split; apply cmra_op_minus. `````` Robbert Krebbers committed Nov 16, 2015 300 301 302 303 304 305 306 ``````Qed. Instance prod_ra_empty `{RAEmpty A, RAEmpty B} : RAEmpty (A * B). Proof. repeat split; simpl; repeat apply ra_empty_valid; repeat apply (left_id _ _). Qed. Instance prod_cmra_extend `{CMRAExtend A, CMRAExtend B} : CMRAExtend (A * B). Proof. `````` Robbert Krebbers committed Nov 20, 2015 307 308 309 `````` 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. `````` Robbert Krebbers committed Nov 16, 2015 310 311 `````` by exists ((z1.1,z2.1),(z1.2,z2.2)). Qed. `````` Robbert Krebbers committed Dec 11, 2015 312 313 314 ``````Instance pair_timeless `{Valid A, ValidN A, Valid B, ValidN B} (x : A) (y : B) : ValidTimeless x → ValidTimeless y → ValidTimeless (x,y). Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed. `````` Robbert Krebbers committed Nov 16, 2015 315 ``````Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B). `````` Robbert Krebbers committed Nov 20, 2015 316 317 318 ``````Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'} (f : A → A') (g : B → B') `{!CMRAMonotone f, !CMRAMonotone g} : CMRAMonotone (prod_map f g). `````` Robbert Krebbers committed Nov 16, 2015 319 320 ``````Proof. split. `````` Robbert Krebbers committed Nov 20, 2015 321 322 `````` * intros n x1 x2; rewrite !prod_includedN; intros [??]; simpl. by split; apply includedN_preserving. `````` Robbert Krebbers committed Nov 16, 2015 323 324 325 326 327 `````` * by intros n x [??]; split; simpl; apply validN_preserving. Qed. Definition prodRA_map {A A' B B' : cmraT} (f : A -n> A') (g : B -n> B') : prodRA A B -n> prodRA A' B' := CofeMor (prod_map f g : prodRA A B → prodRA A' B'). `````` Robbert Krebbers committed Nov 16, 2015 328 329 ``````Instance prodRA_map_ne {A A' B B'} n : Proper (dist n==> dist n==> dist n) (@prodRA_map A A' B B') := prodC_map_ne n.``````