cmra.v 23.4 KB
 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 `````` 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 24 ``````Notation "✓{ n } x" := (validN n x) (at level 20, n at level 1, 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 33 34 ``````Notation "x ≼{ n } y" := (includedN n x y) (at level 70, format "x ≼{ n } y") : C_scope. 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; `````` 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 `````` 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 104 105 106 107 `````` 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 108 109 `````` 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 110 111 `````` 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 112 113 114 115 `````` 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 116 `````` Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 117 118 `````` Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed. Lemma cmra_extend_op n x y1 y2 : `````` Ralf Jung committed Feb 10, 2016 119 120 `````` ✓{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 121 122 123 `````` Proof. apply (cmra_extend_mixin A). Qed. End cmra_mixin. `````` Robbert Krebbers committed Feb 01, 2016 124 125 126 127 128 129 130 131 ``````(** * 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 132 ``````Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅. `````` Robbert Krebbers committed Jan 14, 2016 133 `````` `````` Robbert Krebbers committed Jan 16, 2016 134 ``````(** * Morphisms *) `````` Robbert Krebbers committed Jan 14, 2016 135 136 ``````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 137 `````` validN_preserving n x : ✓{n} x → ✓{n} f x `````` Robbert Krebbers committed Jan 14, 2016 138 139 ``````}. `````` Robbert Krebbers committed Feb 11, 2016 140 ``````(** * Local updates *) `````` 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 Jan 14, 2016 148 ``````Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n, `````` 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 Jan 14, 2016 152 ``````Definition cmra_update {A : cmraT} (x y : A) := ∀ z n, `````` 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 203 204 205 206 207 208 209 210 ``````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 211 212 213 214 215 216 217 218 219 `````` (** ** 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. `````` 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 11, 2016 229 ``````Lemma cmra_unit_validN x n : ✓{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 238 239 240 ``````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 241 242 243 244 245 ``````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). `````` Robbert Krebbers committed Feb 11, 2016 246 `````` by rewrite assoc -Hy -Hz. `````` Robbert Krebbers committed Feb 01, 2016 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 ``````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. `````` 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 285 `````` Lemma cmra_included_dist_l x1 x2 x1' n : `````` 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 10, 2016 302 `````` destruct (cmra_extend_op 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 10, 2016 311 `````` destruct (cmra_extend_op 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 319 320 321 322 323 ``````(** ** 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 (≡) ∅ (⋅). `````` 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 `````` `````` Robbert Krebbers committed Feb 01, 2016 341 ``````(** ** Updates *) `````` Robbert Krebbers committed Jan 14, 2016 342 ``````Global Instance cmra_update_preorder : PreOrder (@cmra_update A). `````` Robbert Krebbers committed Nov 22, 2015 343 ``````Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed. `````` Ralf Jung committed Feb 03, 2016 344 ``````Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). `````` Robbert Krebbers committed Nov 22, 2015 345 346 347 348 349 ``````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 350 ``````Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. `````` Robbert Krebbers committed Feb 02, 2016 351 ``````Proof. by intros ? z n ?; exists x. Qed. `````` Robbert Krebbers committed Feb 02, 2016 352 ``````Lemma cmra_updateP_compose (P Q : A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 353 `````` x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 354 355 356 ``````Proof. intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y). Qed. `````` Robbert Krebbers committed Feb 08, 2016 357 358 359 360 361 ``````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 362 ``````Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 363 ``````Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. `````` Robbert Krebbers committed Feb 02, 2016 364 `````` `````` Robbert Krebbers committed Feb 02, 2016 365 ``````Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 366 `````` x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 367 368 ``````Proof. intros Hx1 Hx2 Hy z n ?. `````` Robbert Krebbers committed Feb 11, 2016 369 `````` destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite assoc. `````` Robbert Krebbers committed Feb 02, 2016 370 `````` destruct (Hx2 (y1 ⋅ z) n) as (y2&?&?); `````` Robbert Krebbers committed Feb 11, 2016 371 372 `````` first by rewrite assoc (comm _ x2) -assoc. exists (y1 ⋅ y2); split; last rewrite (comm _ y1) -assoc; auto. `````` Robbert Krebbers committed Feb 02, 2016 373 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 374 ``````Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : `````` Ralf Jung committed Feb 03, 2016 375 `````` x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. `````` Robbert Krebbers committed Feb 02, 2016 376 ``````Proof. eauto 10 using cmra_updateP_op. Qed. `````` Ralf Jung committed Feb 03, 2016 377 ``````Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2. `````` Robbert Krebbers committed Feb 02, 2016 378 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 379 `````` rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. `````` Robbert Krebbers committed Feb 02, 2016 380 ``````Qed. `````` Ralf Jung committed Feb 13, 2016 381 382 ``````Lemma cmra_update_id x : x ~~> x. Proof. intro. auto. Qed. `````` Robbert Krebbers committed Feb 08, 2016 383 384 385 386 387 388 389 390 `````` 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 391 392 ``````End cmra. `````` Robbert Krebbers committed Feb 01, 2016 393 ``````(** * Properties about monotone functions *) `````` Robbert Krebbers committed Jan 14, 2016 394 ``````Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A). `````` Robbert Krebbers committed Nov 16, 2015 395 ``````Proof. by split. Qed. `````` Robbert Krebbers committed Feb 01, 2016 396 397 ``````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 398 399 ``````Proof. split. `````` Robbert Krebbers committed Feb 01, 2016 400 401 `````` * 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 402 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 403 `````` `````` Robbert Krebbers committed Feb 01, 2016 404 405 406 407 408 409 ``````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 410 `````` Lemma valid_preserving x : ✓ x → ✓ f x. `````` Robbert Krebbers committed Feb 01, 2016 411 412 413 `````` Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed. End cmra_monotone. `````` 414 `````` `````` Robbert Krebbers committed Feb 08, 2016 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 ``````(** * 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 430 `````` Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x. `````` Robbert Krebbers committed Feb 08, 2016 431 `````` Proof. by destruct H. Qed. `````` Robbert Krebbers committed Feb 11, 2016 432 `````` Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x. `````` Robbert Krebbers committed Feb 08, 2016 433 434 435 436 437 438 439 440 441 442 443 `````` 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 444 445 446 447 448 449 ``````(** * 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 450 `````` ra_validN_ne :> Proper ((≡) ==> impl) valid; `````` Robbert Krebbers committed Feb 01, 2016 451 452 `````` ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus; (* monoid *) `````` Robbert Krebbers committed Feb 11, 2016 453 454 `````` ra_assoc :> Assoc (≡) (⋅); ra_comm :> Comm (≡) (⋅); `````` Robbert Krebbers committed Feb 01, 2016 455 `````` ra_unit_l x : unit x ⋅ x ≡ x; `````` Robbert Krebbers committed Feb 11, 2016 456 `````` ra_unit_idemp x : unit (unit x) ≡ unit x; `````` Robbert Krebbers committed Feb 01, 2016 457 458 459 460 461 `````` 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 462 ``````Section discrete. `````` Robbert Krebbers committed Feb 01, 2016 463 464 465 `````` 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 466 `````` Instance discrete_validN : ValidN A := λ n x, ✓ x. `````` Robbert Krebbers committed Jan 14, 2016 467 `````` Definition discrete_cmra_mixin : CMRAMixin A. `````` Robbert Krebbers committed Nov 16, 2015 468 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 469 470 `````` by destruct ra; split; unfold Proper, respectful, includedN; try setoid_rewrite <-(timeless_iff _ _ _ _). `````` Robbert Krebbers committed Nov 16, 2015 471 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 472 `````` Definition discrete_extend_mixin : CMRAExtendMixin A. `````` Robbert Krebbers committed Nov 16, 2015 473 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 474 475 `````` 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 476 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 477 `````` Definition discreteRA : cmraT := `````` Robbert Krebbers committed Feb 01, 2016 478 `````` CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin. `````` Robbert Krebbers committed Feb 02, 2016 479 `````` Lemma discrete_updateP (x : discreteRA) (P : A → Prop) : `````` Ralf Jung committed Feb 03, 2016 480 `````` (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P. `````` Robbert Krebbers committed Feb 02, 2016 481 `````` Proof. intros Hvalid z n; apply Hvalid. Qed. `````` Robbert Krebbers committed Feb 02, 2016 482 `````` Lemma discrete_update (x y : discreteRA) : `````` Ralf Jung committed Feb 03, 2016 483 `````` (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. `````` Robbert Krebbers committed Feb 02, 2016 484 `````` Proof. intros Hvalid z n; apply Hvalid. Qed. `````` Robbert Krebbers committed Nov 16, 2015 485 486 ``````End discrete. `````` Robbert Krebbers committed Feb 01, 2016 487 488 489 490 491 492 493 494 495 496 497 498 499 500 ``````(** ** 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 501 `````` `````` Robbert Krebbers committed Feb 01, 2016 502 ``````(** ** Product *) `````` Robbert Krebbers committed Jan 14, 2016 503 504 505 506 507 ``````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 508 `````` Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2. `````` Robbert Krebbers committed Jan 14, 2016 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 `````` 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 528 `````` * by intros n x [??]; split; apply cmra_validN_S. `````` Robbert Krebbers committed Feb 11, 2016 529 530 531 532 `````` * by split; rewrite /= assoc. * by split; rewrite /= comm. * by split; rewrite /= cmra_unit_l. * by split; rewrite /= cmra_unit_idemp. `````` Robbert Krebbers committed Jan 14, 2016 533 `````` * intros n x y; rewrite !prod_includedN. `````` Robbert Krebbers committed Feb 01, 2016 534 535 `````` 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 536 537 538 539 540 541 542 543 544 545 546 547 `````` * 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 548 549 550 551 552 553 554 555 `````` 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 556 `````` Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. `````` Robbert Krebbers committed Feb 02, 2016 557 `````` Proof. intros ?? z n [??]; split; simpl in *; auto. Qed. `````` Robbert Krebbers committed Feb 02, 2016 558 `````` Lemma prod_updateP P1 P2 (Q : A * B → Prop) x : `````` Ralf Jung committed Feb 03, 2016 559 `````` x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 560 561 562 563 564 `````` 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 565 `````` Lemma prod_updateP' P1 P2 x : `````` Ralf Jung committed Feb 03, 2016 566 `````` x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2). `````` Robbert Krebbers committed Feb 02, 2016 567 `````` Proof. eauto using prod_updateP. Qed. `````` Robbert Krebbers committed Jan 14, 2016 568 569 570 571 572 ``````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 573 574 ``````Proof. split. `````` Robbert Krebbers committed Jan 14, 2016 575 `````` * intros n x y; rewrite !prod_includedN; intros [??]; simpl. `````` Robbert Krebbers committed Nov 20, 2015 576 `````` by split; apply includedN_preserving. `````` Robbert Krebbers committed Nov 16, 2015 577 578 `````` * by intros n x [??]; split; simpl; apply validN_preserving. Qed.``````