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