agree.v 12.3 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.algebra Require Export cmra. `````` Ralf Jung committed Nov 25, 2016 2 ``````From iris.algebra Require Import list. `````` Robbert Krebbers committed Oct 25, 2016 3 ``````From iris.base_logic Require Import base_logic. `````` Ralf Jung committed Nov 25, 2016 4 5 6 7 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. Local Arguments op _ _ _ !_ /. Local Arguments pcore _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 8 `````` `````` Ralf Jung committed Apr 12, 2017 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 ``````(** Define an agreement construction such that Agree A is discrete when A is discrete. Notice that this construction is NOT complete. The fullowing is due to Aleš: Proposition: Ag(T) is not necessarily complete. Proof. Let T be the set of binary streams (infinite sequences) with the usual ultrametric, measuring how far they agree. Let Aₙ be the set of all binary strings of length n. Thus for Aₙ to be a subset of T we have them continue as a stream of zeroes. Now Aₙ is a finite non-empty subset of T. Moreover {Aₙ} is a Cauchy sequence in the defined (Hausdorff) metric. However the limit (if it were to exist as an element of Ag(T)) would have to be the set of all binary streams, which is not exactly finite. Thus Ag(T) is not necessarily complete. *) `````` Robbert Krebbers committed Dec 10, 2018 29 30 31 ``````(** Note that the projection [agree_car] is not non-expansive, so it cannot be used in the logic. If you need to get a witness out, you should use the lemma [to_agree_uninjN] instead. *) `````` Robbert Krebbers committed Nov 27, 2017 32 ``````Record agree (A : Type) : Type := { `````` 33 34 `````` agree_car : list A; agree_not_nil : bool_decide (agree_car = []) = false `````` Robbert Krebbers committed Nov 11, 2015 35 ``````}. `````` Ralf Jung committed Nov 25, 2016 36 ``````Arguments agree_car {_} _. `````` 37 38 ``````Arguments agree_not_nil {_} _. Local Coercion agree_car : agree >-> list. `````` Ralf Jung committed Nov 25, 2016 39 `````` `````` Robbert Krebbers committed Nov 27, 2017 40 41 42 ``````Definition to_agree {A} (a : A) : agree A := {| agree_car := [a]; agree_not_nil := eq_refl |}. `````` 43 44 45 ``````Lemma elem_of_agree {A} (x : agree A) : ∃ a, a ∈ agree_car x. Proof. destruct x as [[|a ?] ?]; set_solver+. Qed. Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y → x = y. `````` Ralf Jung committed Nov 25, 2016 46 ``````Proof. `````` 47 48 `````` destruct x as [a ?], y as [b ?]; simpl. intros ->; f_equal. apply (proof_irrel _). `````` Ralf Jung committed Nov 25, 2016 49 50 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 51 ``````Section agree. `````` Ralf Jung committed Jan 25, 2017 52 ``````Local Set Default Proof Using "Type". `````` Ralf Jung committed Nov 22, 2016 53 ``````Context {A : ofeT}. `````` 54 55 ``````Implicit Types a b : A. Implicit Types x y : agree A. `````` Robbert Krebbers committed Nov 11, 2015 56 `````` `````` 57 ``````(* OFE *) `````` Robbert Krebbers committed Jan 14, 2016 58 ``````Instance agree_dist : Dist (agree A) := λ n x y, `````` 59 60 61 `````` (∀ a, a ∈ agree_car x → ∃ b, b ∈ agree_car y ∧ a ≡{n}≡ b) ∧ (∀ b, b ∈ agree_car y → ∃ a, a ∈ agree_car x ∧ a ≡{n}≡ b). Instance agree_equiv : Equiv (agree A) := λ x y, ∀ n, x ≡{n}≡ y. `````` Ralf Jung committed Nov 25, 2016 62 `````` `````` Ralf Jung committed Nov 22, 2016 63 ``````Definition agree_ofe_mixin : OfeMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 64 65 ``````Proof. split. `````` 66 67 68 69 70 71 72 73 74 75 `````` - done. - intros n; split; rewrite /dist /agree_dist. + intros x; split; eauto. + intros x y [??]. naive_solver eauto. + intros x y z [H1 H1'] [H2 H2']; split. * intros a ?. destruct (H1 a) as (b&?&?); auto. destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans. * intros a ?. destruct (H2' a) as (b&?&?); auto. destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans. - intros n x y [??]; split; naive_solver eauto using dist_S. `````` Robbert Krebbers committed Nov 11, 2015 76 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 77 78 ``````Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin. `````` 79 80 81 82 83 84 85 86 87 88 ``````(* CMRA *) (* agree_validN is carefully written such that, when applied to a singleton, it is convertible to True. This makes working with agreement much more pleasant. *) Instance agree_validN : ValidN (agree A) := λ n x, match agree_car x with | [a] => True | _ => ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b end. Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x. `````` Robbert Krebbers committed Jan 14, 2016 89 ``````Program Instance agree_op : Op (agree A) := λ x y, `````` Robbert Krebbers committed Nov 27, 2017 90 `````` {| agree_car := agree_car x ++ agree_car y |}. `````` 91 ``````Next Obligation. by intros [[|??]] y. Qed. `````` Robbert Krebbers committed May 28, 2016 92 ``````Instance agree_pcore : PCore (agree A) := Some. `````` Robbert Krebbers committed Feb 24, 2016 93 `````` `````` 94 95 96 97 98 99 ``````Lemma agree_validN_def n x : ✓{n} x ↔ ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b. Proof. rewrite /validN /agree_validN. destruct (agree_car _) as [|? [|??]]; auto. setoid_rewrite elem_of_list_singleton; naive_solver. Qed. `````` Ralf Jung committed Nov 25, 2016 100 `````` `````` 101 102 103 ``````Instance agree_comm : Comm (≡) (@op (agree A) _). Proof. intros x y n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed. Instance agree_assoc : Assoc (≡) (@op (agree A) _). `````` Robbert Krebbers committed Jan 16, 2016 104 ``````Proof. `````` 105 `````` intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver. `````` Robbert Krebbers committed Jan 16, 2016 106 ``````Qed. `````` 107 108 109 110 ``````Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x. Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed. Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n). `````` Ralf Jung committed Nov 25, 2016 111 ``````Proof. `````` 112 113 `````` intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb. destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto. `````` Ralf Jung committed Nov 25, 2016 114 ``````Qed. `````` 115 116 ``````Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n). Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed. `````` Ralf Jung committed Nov 25, 2016 117 `````` `````` 118 ``````Instance agree_op_ne' x : NonExpansive (op x). `````` Robbert Krebbers committed Nov 11, 2015 119 ``````Proof. `````` 120 `````` intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver. `````` Robbert Krebbers committed Nov 11, 2015 121 ``````Qed. `````` 122 ``````Instance agree_op_ne : NonExpansive2 (@op (agree A) _). `````` Robbert Krebbers committed Feb 11, 2016 123 ``````Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed. `````` 124 ``````Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _. `````` Robbert Krebbers committed Feb 24, 2016 125 `````` `````` Robbert Krebbers committed Feb 26, 2016 126 127 128 129 130 ``````Lemma agree_included (x y : agree A) : x ≼ y ↔ y ≡ x ⋅ y. Proof. split; [|by intros ?; exists y]. by intros [z Hz]; rewrite Hz assoc agree_idemp. Qed. `````` Robbert Krebbers committed Mar 21, 2017 131 `````` `````` Ralf Jung committed Nov 25, 2016 132 133 ``````Lemma agree_op_invN n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2. Proof. `````` 134 135 136 `````` rewrite agree_validN_def /=. setoid_rewrite elem_of_app=> Hv; split=> a Ha. - destruct (elem_of_agree x2); naive_solver. - destruct (elem_of_agree x1); naive_solver. `````` Robbert Krebbers committed Feb 24, 2016 137 138 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 139 ``````Definition agree_cmra_mixin : CmraMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 140 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 141 `````` apply cmra_total_mixin; try apply _ || by eauto. `````` 142 `````` - intros n x; rewrite !agree_validN_def; eauto using dist_S. `````` Robbert Krebbers committed May 28, 2016 143 `````` - intros x. apply agree_idemp. `````` 144 145 `````` - intros n x y; rewrite !agree_validN_def /=. setoid_rewrite elem_of_app; naive_solver. `````` Robbert Krebbers committed Aug 14, 2016 146 `````` - intros n x y1 y2 Hval Hx; exists x, x; simpl; split. `````` Robbert Krebbers committed Feb 24, 2016 147 `````` + by rewrite agree_idemp. `````` Ralf Jung committed Nov 25, 2016 148 `````` + by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp. `````` Robbert Krebbers committed Nov 11, 2015 149 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 150 ``````Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin. `````` Robbert Krebbers committed Jan 14, 2016 151 `````` `````` Robbert Krebbers committed Oct 25, 2017 152 153 ``````Global Instance agree_cmra_total : CmraTotal agreeR. Proof. rewrite /CmraTotal; eauto. Qed. `````` Robbert Krebbers committed Oct 25, 2017 154 ``````Global Instance agree_core_id (x : agree A) : CoreId x. `````` Robbert Krebbers committed May 28, 2016 155 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Mar 15, 2016 156 `````` `````` Robbert Krebbers committed Oct 25, 2017 157 ``````Global Instance agree_cmra_discrete : OfeDiscrete A → CmraDiscrete agreeR. `````` Ralf Jung committed Nov 25, 2016 158 159 ``````Proof. intros HD. split. `````` Robbert Krebbers committed Oct 25, 2017 160 `````` - intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _); auto. `````` 161 `````` - intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??. `````` Robbert Krebbers committed Oct 25, 2017 162 `````` apply discrete_iff_0; auto. `````` Ralf Jung committed Nov 25, 2016 163 164 ``````Qed. `````` Ralf Jung committed Jan 27, 2017 165 ``````Global Instance to_agree_ne : NonExpansive to_agree. `````` Ralf Jung committed Nov 25, 2016 166 ``````Proof. `````` 167 168 `````` intros n a1 a2 Hx; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver. `````` Ralf Jung committed Nov 25, 2016 169 ``````Qed. `````` Robbert Krebbers committed Jan 16, 2016 170 ``````Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _. `````` Robbert Krebbers committed Jul 21, 2016 171 `````` `````` Robbert Krebbers committed Nov 27, 2017 172 173 174 175 176 177 178 179 180 ``````Global Instance to_agree_discrete a : Discrete a → Discrete (to_agree a). Proof. intros ? y [H H'] n; split. - intros a' ->%elem_of_list_singleton. destruct (H a) as [b ?]; first by left. exists b. by rewrite -discrete_iff_0. - intros b Hb. destruct (H' b) as (b'&->%elem_of_list_singleton&?); auto. exists a. by rewrite elem_of_list_singleton -discrete_iff_0. Qed. `````` Ralf Jung committed Nov 25, 2016 181 ``````Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree). `````` 182 183 184 ``````Proof. move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver. Qed. `````` Ralf Jung committed Nov 25, 2016 185 ``````Global Instance to_agree_inj : Inj (≡) (≡) (to_agree). `````` Robbert Krebbers committed Mar 21, 2017 186 ``````Proof. intros a b ?. apply equiv_dist=>n. by apply to_agree_injN, equiv_dist. Qed. `````` Robbert Krebbers committed Jul 21, 2016 187 `````` `````` Robbert Krebbers committed Dec 10, 2018 188 ``````Lemma to_agree_uninjN n x : ✓{n} x → ∃ a, to_agree a ≡{n}≡ x. `````` Robbert Krebbers committed Jul 21, 2016 189 ``````Proof. `````` 190 191 192 `````` rewrite agree_validN_def=> Hv. destruct (elem_of_agree x) as [a ?]. exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver. `````` Ralf Jung committed Nov 25, 2016 193 194 ``````Qed. `````` Robbert Krebbers committed Dec 10, 2018 195 ``````Lemma to_agree_uninj x : ✓ x → ∃ a, to_agree a ≡ x. `````` Ralf Jung committed Dec 13, 2016 196 ``````Proof. `````` 197 198 199 `````` rewrite /valid /agree_valid; setoid_rewrite agree_validN_def. destruct (elem_of_agree x) as [a ?]. exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver. `````` Ralf Jung committed Dec 13, 2016 200 201 ``````Qed. `````` 202 ``````Lemma agree_valid_includedN n x y : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. `````` Ralf Jung committed Nov 25, 2016 203 ``````Proof. `````` 204 205 206 207 208 209 210 211 212 `````` move=> Hval [z Hy]; move: Hval; rewrite Hy. by move=> /agree_op_invN->; rewrite agree_idemp. Qed. Lemma to_agree_included a b : to_agree a ≼ to_agree b ↔ a ≡ b. Proof. split; last by intros ->. intros (x & Heq). apply equiv_dist=>n. destruct (Heq n) as [_ Hincl]. by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+. `````` Jacques-Henri Jourdan committed Feb 01, 2017 213 214 ``````Qed. `````` 215 ``````Global Instance agree_cancelable x : Cancelable x. `````` Jacques-Henri Jourdan committed Feb 01, 2017 216 217 218 219 220 221 222 ``````Proof. intros n y z Hv Heq. destruct (to_agree_uninjN n x) as [x' EQx]; first by eapply cmra_validN_op_l. destruct (to_agree_uninjN n y) as [y' EQy]; first by eapply cmra_validN_op_r. destruct (to_agree_uninjN n z) as [z' EQz]. { eapply (cmra_validN_op_r n x z). by rewrite -Heq. } assert (Hx'y' : x' ≡{n}≡ y'). `````` Robbert Krebbers committed Mar 21, 2017 223 `````` { apply (inj to_agree), agree_op_invN. by rewrite EQx EQy. } `````` Jacques-Henri Jourdan committed Feb 01, 2017 224 `````` assert (Hx'z' : x' ≡{n}≡ z'). `````` Robbert Krebbers committed Mar 21, 2017 225 `````` { apply (inj to_agree), agree_op_invN. by rewrite EQx EQz -Heq. } `````` Jacques-Henri Jourdan committed Feb 01, 2017 226 227 228 `````` by rewrite -EQy -EQz -Hx'y' -Hx'z'. Qed. `````` 229 ``````Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y. `````` Robbert Krebbers committed Mar 21, 2017 230 231 232 ``````Proof. intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN. Qed. `````` 233 ``````Lemma agree_op_inv' a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b. `````` Robbert Krebbers committed Mar 21, 2017 234 ``````Proof. by intros ?%agree_op_inv%(inj _). Qed. `````` 235 ``````Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b. `````` Robbert Krebbers committed Mar 21, 2017 236 237 ``````Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed. `````` Robbert Krebbers committed Feb 13, 2016 238 ``````(** Internalized properties *) `````` Robbert Krebbers committed Dec 10, 2018 239 ``````Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b). `````` Robbert Krebbers committed Feb 25, 2016 240 ``````Proof. `````` Ralf Jung committed Nov 25, 2016 241 242 243 `````` uPred.unseal. do 2 split. - intros Hx. exact: to_agree_injN. - intros Hx. exact: to_agree_ne. `````` Robbert Krebbers committed Feb 25, 2016 244 ``````Qed. `````` Robbert Krebbers committed Dec 10, 2018 245 ``````Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y. `````` Ralf Jung committed Nov 25, 2016 246 ``````Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed. `````` Robbert Krebbers committed Dec 10, 2018 247 248 249 `````` Lemma to_agree_uninjI {M} x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x. Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed. `````` Robbert Krebbers committed Nov 11, 2015 250 251 ``````End agree. `````` Maxime Dénès committed Jan 24, 2019 252 ``````Instance: Params (@to_agree) 1 := {}. `````` Robbert Krebbers committed Jan 14, 2016 253 ``````Arguments agreeC : clear implicits. `````` Robbert Krebbers committed Mar 01, 2016 254 ``````Arguments agreeR : clear implicits. `````` Robbert Krebbers committed Jan 14, 2016 255 `````` `````` Robbert Krebbers committed Dec 21, 2015 256 ``````Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B := `````` 257 258 `````` {| agree_car := f <\$> agree_car x |}. Next Obligation. by intros A B f [[|??] ?]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 259 ``````Lemma agree_map_id {A} (x : agree A) : agree_map id x = x. `````` 260 ``````Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed. `````` Robbert Krebbers committed Jan 16, 2016 261 262 ``````Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) : agree_map (g ∘ f) x = agree_map g (agree_map f x). `````` 263 ``````Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed. `````` Robbert Krebbers committed Dec 03, 2018 264 265 266 ``````Lemma agree_map_to_agree {A B} (f : A → B) (x : A) : agree_map f (to_agree x) = to_agree (f x). Proof. by apply agree_eq. Qed. `````` Robbert Krebbers committed Dec 15, 2015 267 `````` `````` Robbert Krebbers committed Nov 11, 2015 268 ``````Section agree_map. `````` Ralf Jung committed Mar 05, 2019 269 `````` Context {A B : ofeT} (f : A → B) {Hf: NonExpansive f}. `````` 270 `````` `````` Ralf Jung committed Jan 27, 2017 271 `````` Instance agree_map_ne : NonExpansive (agree_map f). `````` 272 273 274 275 `````` Proof. intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap. - intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver. - intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver. `````` Ralf Jung committed Nov 25, 2016 276 `````` Qed. `````` Robbert Krebbers committed Feb 26, 2016 277 `````` Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _. `````` Ralf Jung committed Nov 25, 2016 278 `````` `````` Robbert Krebbers committed Dec 15, 2015 279 `````` Lemma agree_map_ext (g : A → B) x : `````` 280 281 282 283 284 `````` (∀ a, f a ≡ g a) → agree_map f x ≡ agree_map g x. Proof using Hf. intros Hfg n; split=> b /=; setoid_rewrite elem_of_list_fmap. - intros (a&->&?). exists (g a). rewrite Hfg; eauto. - intros (a&->&?). exists (f a). rewrite -Hfg; eauto. `````` Ralf Jung committed Nov 25, 2016 285 286 `````` Qed. `````` Robbert Krebbers committed Oct 25, 2017 287 `````` Global Instance agree_map_morphism : CmraMorphism (agree_map f). `````` 288 `````` Proof using Hf. `````` Robbert Krebbers committed Feb 26, 2016 289 `````` split; first apply _. `````` 290 291 292 `````` - intros n x. rewrite !agree_validN_def=> Hv b b' /=. intros (a&->&?)%elem_of_list_fmap (a'&->&?)%elem_of_list_fmap. apply Hf; eauto. `````` 293 `````` - done. `````` 294 295 `````` - intros x y n; split=> b /=; rewrite !fmap_app; setoid_rewrite elem_of_app; eauto. `````` Robbert Krebbers committed Nov 11, 2015 296 297 `````` Qed. End agree_map. `````` Robbert Krebbers committed Nov 16, 2015 298 `````` `````` Robbert Krebbers committed Feb 04, 2016 299 300 ``````Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B := CofeMor (agree_map f : agreeC A → agreeC B). `````` Ralf Jung committed Jan 27, 2017 301 ``````Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B). `````` Robbert Krebbers committed Nov 16, 2015 302 ``````Proof. `````` 303 304 `````` intros n f g Hfg x; split=> b /=; setoid_rewrite elem_of_list_fmap; naive_solver. `````` Robbert Krebbers committed Nov 16, 2015 305 ``````Qed. `````` Ralf Jung committed Feb 05, 2016 306 `````` `````` Robbert Krebbers committed Mar 02, 2016 307 308 309 310 ``````Program Definition agreeRF (F : cFunctor) : rFunctor := {| rFunctor_car A B := agreeR (cFunctor_car F A B); rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg) |}. `````` Robbert Krebbers committed Mar 07, 2016 311 312 313 ``````Next Obligation. intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 314 315 ``````Next Obligation. intros F A B x; simpl. rewrite -{2}(agree_map_id x). `````` 316 `````` apply (agree_map_ext _)=>y. by rewrite cFunctor_id. `````` Robbert Krebbers committed Mar 02, 2016 317 318 319 ``````Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose. `````` 320 `````` apply (agree_map_ext _)=>y; apply cFunctor_compose. `````` Robbert Krebbers committed Mar 02, 2016 321 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 322 323 324 325 326 327 328 `````` Instance agreeRF_contractive F : cFunctorContractive F → rFunctorContractive (agreeRF F). Proof. intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_contractive. Qed.``````