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