agree.v 12 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 Nov 27, 2017 29 ``````Record agree (A : Type) : Type := { `````` 30 31 `````` agree_car : list A; agree_not_nil : bool_decide (agree_car = []) = false `````` Robbert Krebbers committed Nov 11, 2015 32 ``````}. `````` Ralf Jung committed Nov 25, 2016 33 ``````Arguments agree_car {_} _. `````` 34 35 ``````Arguments agree_not_nil {_} _. Local Coercion agree_car : agree >-> list. `````` Ralf Jung committed Nov 25, 2016 36 `````` `````` Robbert Krebbers committed Nov 27, 2017 37 38 39 ``````Definition to_agree {A} (a : A) : agree A := {| agree_car := [a]; agree_not_nil := eq_refl |}. `````` 40 41 42 ``````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 43 ``````Proof. `````` 44 45 `````` destruct x as [a ?], y as [b ?]; simpl. intros ->; f_equal. apply (proof_irrel _). `````` Ralf Jung committed Nov 25, 2016 46 47 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 48 ``````Section agree. `````` Ralf Jung committed Jan 25, 2017 49 ``````Local Set Default Proof Using "Type". `````` Ralf Jung committed Nov 22, 2016 50 ``````Context {A : ofeT}. `````` 51 52 ``````Implicit Types a b : A. Implicit Types x y : agree A. `````` Robbert Krebbers committed Nov 11, 2015 53 `````` `````` 54 ``````(* OFE *) `````` Robbert Krebbers committed Jan 14, 2016 55 ``````Instance agree_dist : Dist (agree A) := λ n x y, `````` 56 57 58 `````` (∀ 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 59 `````` `````` Ralf Jung committed Nov 22, 2016 60 ``````Definition agree_ofe_mixin : OfeMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 61 62 ``````Proof. split. `````` 63 64 65 66 67 68 69 70 71 72 `````` - 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 73 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 74 75 ``````Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin. `````` 76 77 78 79 80 81 82 83 84 85 ``````(* 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 86 ``````Program Instance agree_op : Op (agree A) := λ x y, `````` Robbert Krebbers committed Nov 27, 2017 87 `````` {| agree_car := agree_car x ++ agree_car y |}. `````` 88 ``````Next Obligation. by intros [[|??]] y. Qed. `````` Robbert Krebbers committed May 28, 2016 89 ``````Instance agree_pcore : PCore (agree A) := Some. `````` Robbert Krebbers committed Feb 24, 2016 90 `````` `````` 91 92 93 94 95 96 ``````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 97 `````` `````` 98 99 100 ``````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 101 ``````Proof. `````` 102 `````` intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver. `````` Robbert Krebbers committed Jan 16, 2016 103 ``````Qed. `````` 104 105 106 107 ``````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 108 ``````Proof. `````` 109 110 `````` 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 111 ``````Qed. `````` 112 113 ``````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 114 `````` `````` 115 ``````Instance agree_op_ne' x : NonExpansive (op x). `````` Robbert Krebbers committed Nov 11, 2015 116 ``````Proof. `````` 117 `````` intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver. `````` Robbert Krebbers committed Nov 11, 2015 118 ``````Qed. `````` 119 ``````Instance agree_op_ne : NonExpansive2 (@op (agree A) _). `````` Robbert Krebbers committed Feb 11, 2016 120 ``````Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed. `````` 121 ``````Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _. `````` Robbert Krebbers committed Feb 24, 2016 122 `````` `````` Robbert Krebbers committed Feb 26, 2016 123 124 125 126 127 ``````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 128 `````` `````` Ralf Jung committed Nov 25, 2016 129 130 ``````Lemma agree_op_invN n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2. Proof. `````` 131 132 133 `````` 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 134 135 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 136 ``````Definition agree_cmra_mixin : CmraMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 137 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 138 `````` apply cmra_total_mixin; try apply _ || by eauto. `````` 139 `````` - intros n x; rewrite !agree_validN_def; eauto using dist_S. `````` Robbert Krebbers committed May 28, 2016 140 `````` - intros x. apply agree_idemp. `````` 141 142 `````` - intros n x y; rewrite !agree_validN_def /=. setoid_rewrite elem_of_app; naive_solver. `````` Robbert Krebbers committed Aug 14, 2016 143 `````` - intros n x y1 y2 Hval Hx; exists x, x; simpl; split. `````` Robbert Krebbers committed Feb 24, 2016 144 `````` + by rewrite agree_idemp. `````` Ralf Jung committed Nov 25, 2016 145 `````` + by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp. `````` Robbert Krebbers committed Nov 11, 2015 146 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 147 ``````Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin. `````` Robbert Krebbers committed Jan 14, 2016 148 `````` `````` Robbert Krebbers committed Oct 25, 2017 149 150 ``````Global Instance agree_cmra_total : CmraTotal agreeR. Proof. rewrite /CmraTotal; eauto. Qed. `````` Robbert Krebbers committed Oct 25, 2017 151 ``````Global Instance agree_core_id (x : agree A) : CoreId x. `````` Robbert Krebbers committed May 28, 2016 152 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Mar 15, 2016 153 `````` `````` Robbert Krebbers committed Oct 25, 2017 154 ``````Global Instance agree_cmra_discrete : OfeDiscrete A → CmraDiscrete agreeR. `````` Ralf Jung committed Nov 25, 2016 155 156 ``````Proof. intros HD. split. `````` Robbert Krebbers committed Oct 25, 2017 157 `````` - intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _); auto. `````` 158 `````` - intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??. `````` Robbert Krebbers committed Oct 25, 2017 159 `````` apply discrete_iff_0; auto. `````` Ralf Jung committed Nov 25, 2016 160 161 ``````Qed. `````` Ralf Jung committed Jan 27, 2017 162 ``````Global Instance to_agree_ne : NonExpansive to_agree. `````` Ralf Jung committed Nov 25, 2016 163 ``````Proof. `````` 164 165 `````` intros n a1 a2 Hx; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver. `````` Ralf Jung committed Nov 25, 2016 166 ``````Qed. `````` Robbert Krebbers committed Jan 16, 2016 167 ``````Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _. `````` Robbert Krebbers committed Jul 21, 2016 168 `````` `````` Robbert Krebbers committed Nov 27, 2017 169 170 171 172 173 174 175 176 177 ``````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 178 ``````Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree). `````` 179 180 181 ``````Proof. move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver. Qed. `````` Ralf Jung committed Nov 25, 2016 182 ``````Global Instance to_agree_inj : Inj (≡) (≡) (to_agree). `````` Robbert Krebbers committed Mar 21, 2017 183 ``````Proof. intros a b ?. apply equiv_dist=>n. by apply to_agree_injN, equiv_dist. Qed. `````` Robbert Krebbers committed Jul 21, 2016 184 `````` `````` Robbert Krebbers committed Dec 10, 2018 185 ``````Lemma to_agree_uninjN n x : ✓{n} x → ∃ a, to_agree a ≡{n}≡ x. `````` Robbert Krebbers committed Jul 21, 2016 186 ``````Proof. `````` 187 188 189 `````` 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 190 191 ``````Qed. `````` Robbert Krebbers committed Dec 10, 2018 192 ``````Lemma to_agree_uninj x : ✓ x → ∃ a, to_agree a ≡ x. `````` Ralf Jung committed Dec 13, 2016 193 ``````Proof. `````` 194 195 196 `````` 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 197 198 ``````Qed. `````` 199 ``````Lemma agree_valid_includedN n x y : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. `````` Ralf Jung committed Nov 25, 2016 200 ``````Proof. `````` 201 202 203 204 205 206 207 208 209 `````` 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 210 211 ``````Qed. `````` 212 ``````Global Instance agree_cancelable x : Cancelable x. `````` Jacques-Henri Jourdan committed Feb 01, 2017 213 214 215 216 217 218 219 ``````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 220 `````` { apply (inj to_agree), agree_op_invN. by rewrite EQx EQy. } `````` Jacques-Henri Jourdan committed Feb 01, 2017 221 `````` assert (Hx'z' : x' ≡{n}≡ z'). `````` Robbert Krebbers committed Mar 21, 2017 222 `````` { apply (inj to_agree), agree_op_invN. by rewrite EQx EQz -Heq. } `````` Jacques-Henri Jourdan committed Feb 01, 2017 223 224 225 `````` by rewrite -EQy -EQz -Hx'y' -Hx'z'. Qed. `````` 226 ``````Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y. `````` Robbert Krebbers committed Mar 21, 2017 227 228 229 ``````Proof. intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN. Qed. `````` 230 ``````Lemma agree_op_inv' a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b. `````` Robbert Krebbers committed Mar 21, 2017 231 ``````Proof. by intros ?%agree_op_inv%(inj _). Qed. `````` 232 ``````Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b. `````` Robbert Krebbers committed Mar 21, 2017 233 234 ``````Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed. `````` Robbert Krebbers committed Feb 13, 2016 235 ``````(** Internalized properties *) `````` Robbert Krebbers committed Dec 10, 2018 236 ``````Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b). `````` Robbert Krebbers committed Feb 25, 2016 237 ``````Proof. `````` Ralf Jung committed Nov 25, 2016 238 239 240 `````` uPred.unseal. do 2 split. - intros Hx. exact: to_agree_injN. - intros Hx. exact: to_agree_ne. `````` Robbert Krebbers committed Feb 25, 2016 241 ``````Qed. `````` Robbert Krebbers committed Dec 10, 2018 242 ``````Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y. `````` Ralf Jung committed Nov 25, 2016 243 ``````Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed. `````` Robbert Krebbers committed Nov 11, 2015 244 245 ``````End agree. `````` Robbert Krebbers committed Jan 30, 2017 246 ``````Instance: Params (@to_agree) 1. `````` Robbert Krebbers committed Jan 14, 2016 247 ``````Arguments agreeC : clear implicits. `````` Robbert Krebbers committed Mar 01, 2016 248 ``````Arguments agreeR : clear implicits. `````` Robbert Krebbers committed Jan 14, 2016 249 `````` `````` Robbert Krebbers committed Dec 21, 2015 250 ``````Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B := `````` 251 252 `````` {| agree_car := f <\$> agree_car x |}. Next Obligation. by intros A B f [[|??] ?]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 253 ``````Lemma agree_map_id {A} (x : agree A) : agree_map id x = x. `````` 254 ``````Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed. `````` Robbert Krebbers committed Jan 16, 2016 255 256 ``````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). `````` 257 ``````Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed. `````` Robbert Krebbers committed Dec 03, 2018 258 259 260 ``````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 261 `````` `````` Robbert Krebbers committed Nov 11, 2015 262 ``````Section agree_map. `````` Ralf Jung committed Jan 27, 2017 263 `````` Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}. `````` 264 `````` `````` Ralf Jung committed Jan 27, 2017 265 `````` Instance agree_map_ne : NonExpansive (agree_map f). `````` 266 267 268 269 `````` 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 270 `````` Qed. `````` Robbert Krebbers committed Feb 26, 2016 271 `````` Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _. `````` Ralf Jung committed Nov 25, 2016 272 `````` `````` Robbert Krebbers committed Dec 15, 2015 273 `````` Lemma agree_map_ext (g : A → B) x : `````` 274 275 276 277 278 `````` (∀ 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 279 280 `````` Qed. `````` Robbert Krebbers committed Oct 25, 2017 281 `````` Global Instance agree_map_morphism : CmraMorphism (agree_map f). `````` 282 `````` Proof using Hf. `````` Robbert Krebbers committed Feb 26, 2016 283 `````` split; first apply _. `````` 284 285 286 `````` - intros n x. rewrite !agree_validN_def=> Hv b b' /=. intros (a&->&?)%elem_of_list_fmap (a'&->&?)%elem_of_list_fmap. apply Hf; eauto. `````` 287 `````` - done. `````` 288 289 `````` - intros x y n; split=> b /=; rewrite !fmap_app; setoid_rewrite elem_of_app; eauto. `````` Robbert Krebbers committed Nov 11, 2015 290 291 `````` Qed. End agree_map. `````` Robbert Krebbers committed Nov 16, 2015 292 `````` `````` Robbert Krebbers committed Feb 04, 2016 293 294 ``````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 295 ``````Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B). `````` Robbert Krebbers committed Nov 16, 2015 296 ``````Proof. `````` 297 298 `````` intros n f g Hfg x; split=> b /=; setoid_rewrite elem_of_list_fmap; naive_solver. `````` Robbert Krebbers committed Nov 16, 2015 299 ``````Qed. `````` Ralf Jung committed Feb 05, 2016 300 `````` `````` Robbert Krebbers committed Mar 02, 2016 301 302 303 304 ``````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 305 306 307 ``````Next Obligation. intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 308 309 ``````Next Obligation. intros F A B x; simpl. rewrite -{2}(agree_map_id x). `````` 310 `````` apply (agree_map_ext _)=>y. by rewrite cFunctor_id. `````` Robbert Krebbers committed Mar 02, 2016 311 312 313 ``````Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose. `````` 314 `````` apply (agree_map_ext _)=>y; apply cFunctor_compose. `````` Robbert Krebbers committed Mar 02, 2016 315 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 316 317 318 319 320 321 322 `````` 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.``````