csum.v 14.2 KB
 Robbert Krebbers committed Jul 25, 2016 1 ``````From iris.algebra Require Export cmra. `````` Robbert Krebbers committed Oct 25, 2016 2 3 ``````From iris.base_logic Require Import base_logic. From iris.algebra Require Import local_updates. `````` Ralf Jung committed Jan 05, 2017 4 ``````Set Default Proof Using "Type". `````` Jacques-Henri Jourdan committed May 30, 2016 5 6 7 8 9 10 11 12 ``````Local Arguments pcore _ _ !_ /. Local Arguments cmra_pcore _ !_ /. Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. Local Arguments cmra_validN _ _ !_ /. Local Arguments cmra_valid _ !_ /. Inductive csum (A B : Type) := `````` Robbert Krebbers committed Jan 30, 2017 13 14 15 `````` | Cinl : A → csum A B | Cinr : B → csum A B | CsumBot : csum A B. `````` Jacques-Henri Jourdan committed May 30, 2016 16 17 18 19 ``````Arguments Cinl {_ _} _. Arguments Cinr {_ _} _. Arguments CsumBot {_ _}. `````` Robbert Krebbers committed Jan 30, 2017 20 21 22 23 ``````Instance: Params (@Cinl) 2. Instance: Params (@Cinr) 2. Instance: Params (@CsumBot) 2. `````` Robbert Krebbers committed Sep 21, 2016 24 25 26 27 28 ``````Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x, match x with Cinl a => Some a | _ => None end. Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x, match x with Cinr b => Some b | _ => None end. `````` Jacques-Henri Jourdan committed May 30, 2016 29 ``````Section cofe. `````` Ralf Jung committed Nov 22, 2016 30 ``````Context {A B : ofeT}. `````` Jacques-Henri Jourdan committed May 30, 2016 31 32 33 34 35 ``````Implicit Types a : A. Implicit Types b : B. (* Cofe *) Inductive csum_equiv : Equiv (csum A B) := `````` Robbert Krebbers committed Jun 23, 2016 36 `````` | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a' `````` Jacques-Henri Jourdan committed Jan 26, 2017 37 `````` | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b' `````` Jacques-Henri Jourdan committed May 30, 2016 38 39 40 `````` | CsumBot_equiv : CsumBot ≡ CsumBot. Existing Instance csum_equiv. Inductive csum_dist : Dist (csum A B) := `````` Robbert Krebbers committed Jun 23, 2016 41 `````` | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a' `````` Jacques-Henri Jourdan committed Jan 26, 2017 42 `````` | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b' `````` Jacques-Henri Jourdan committed May 30, 2016 43 44 45 `````` | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot. Existing Instance csum_dist. `````` Ralf Jung committed Jan 27, 2017 46 ``````Global Instance Cinl_ne : NonExpansive (@Cinl A B). `````` Jacques-Henri Jourdan committed May 30, 2016 47 48 49 50 51 52 53 ``````Proof. by constructor. Qed. Global Instance Cinl_proper : Proper ((≡) ==> (≡)) (@Cinl A B). Proof. by constructor. Qed. Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B). Proof. by inversion_clear 1. Qed. Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B). Proof. by inversion_clear 1. Qed. `````` Ralf Jung committed Jan 27, 2017 54 ``````Global Instance Cinr_ne : NonExpansive (@Cinr A B). `````` Jacques-Henri Jourdan committed May 30, 2016 55 56 57 58 59 60 61 62 ``````Proof. by constructor. Qed. Global Instance Cinr_proper : Proper ((≡) ==> (≡)) (@Cinr A B). Proof. by constructor. Qed. Global Instance Cinr_inj : Inj (≡) (≡) (@Cinr A B). Proof. by inversion_clear 1. Qed. Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B). Proof. by inversion_clear 1. Qed. `````` Ralf Jung committed Nov 22, 2016 63 ``````Definition csum_ofe_mixin : OfeMixin (csum A B). `````` Jacques-Henri Jourdan committed May 30, 2016 64 65 66 67 68 69 70 71 72 73 74 75 ``````Proof. split. - intros mx my; split. + by destruct 1; constructor; try apply equiv_dist. + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done; apply equiv_dist=> n; by feed inversion (Hxy n). - intros n; split. + by intros [|a|]; constructor. + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; apply dist_S. Qed. `````` Ralf Jung committed Nov 22, 2016 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 ``````Canonical Structure csumC : ofeT := OfeT (csum A B) csum_ofe_mixin. Program Definition csum_chain_l (c : chain csumC) (a : A) : chain A := {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}. Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Program Definition csum_chain_r (c : chain csumC) (b : B) : chain B := {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}. Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Definition csum_compl `{Cofe A, Cofe B} : Compl csumC := λ c, match c 0 with | Cinl a => Cinl (compl (csum_chain_l c a)) | Cinr b => Cinr (compl (csum_chain_r c b)) | CsumBot => CsumBot end. Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumC := {| compl := csum_compl |}. Next Obligation. intros ?? n c; rewrite /compl /csum_compl. feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver. + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver. Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 ``````Global Instance csum_discrete : Discrete A → Discrete B → Discrete csumC. Proof. by inversion_clear 3; constructor; apply (timeless _). Qed. Global Instance csum_leibniz : LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv (csumC A B). Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed. Global Instance Cinl_timeless a : Timeless a → Timeless (Cinl a). Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Global Instance Cinr_timeless b : Timeless b → Timeless (Cinr b). Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. End cofe. Arguments csumC : clear implicits. (* Functor on COFEs *) Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B') (x : csum A B) : csum A' B' := match x with | Cinl a => Cinl (fA a) | Cinr b => Cinr (fB b) | CsumBot => CsumBot end. Instance: Params (@csum_map) 4. Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x. Proof. by destruct x. Qed. Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'') (g : B → B') (g' : B' → B'') (x : csum A B) : csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x). Proof. by destruct x. Qed. `````` Ralf Jung committed Nov 22, 2016 129 ``````Lemma csum_map_ext {A A' B B' : ofeT} (f f' : A → A') (g g' : B → B') x : `````` Jacques-Henri Jourdan committed May 30, 2016 130 131 `````` (∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x. Proof. by destruct x; constructor. Qed. `````` Ralf Jung committed Nov 22, 2016 132 ``````Instance csum_map_cmra_ne {A A' B B' : ofeT} n : `````` Jacques-Henri Jourdan committed May 30, 2016 133 134 135 136 137 138 `````` Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n) (@csum_map A A' B B'). Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed. Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') : csumC A B -n> csumC A' B' := CofeMor (csum_map f g). `````` Ralf Jung committed Jan 27, 2017 139 140 141 ``````Instance csumC_map_ne A A' B B' : NonExpansive2 (@csumC_map A A' B B'). Proof. by intros n f f' Hf g g' Hg []; constructor. Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 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 `````` Section cmra. Context {A B : cmraT}. Implicit Types a : A. Implicit Types b : B. (* CMRA *) Instance csum_valid : Valid (csum A B) := λ x, match x with | Cinl a => ✓ a | Cinr b => ✓ b | CsumBot => False end. Instance csum_validN : ValidN (csum A B) := λ n x, match x with | Cinl a => ✓{n} a | Cinr b => ✓{n} b | CsumBot => False end. Instance csum_pcore : PCore (csum A B) := λ x, match x with | Cinl a => Cinl <\$> pcore a | Cinr b => Cinr <\$> pcore b | CsumBot => Some CsumBot end. Instance csum_op : Op (csum A B) := λ x y, match x, y with | Cinl a, Cinl a' => Cinl (a ⋅ a') | Cinr b, Cinr b' => Cinr (b ⋅ b') | _, _ => CsumBot end. Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a'). Proof. done. Qed. Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b'). Proof. done. Qed. Lemma csum_included x y : x ≼ y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a') ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b'). Proof. split. - intros [z Hy]; destruct x as [a|b|], z as [a'|b'|]; inversion_clear Hy; auto. + right; left; eexists _, _; split_and!; eauto. eexists; eauto. + right; right; eexists _, _; split_and!; eauto. eexists; eauto. - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]]. + destruct x; exists CsumBot; constructor. + exists (Cinl c); by constructor. + exists (Cinr c); by constructor. Qed. Lemma csum_cmra_mixin : CMRAMixin (csum A B). Proof. split. `````` Ralf Jung committed Jan 27, 2017 196 `````` - intros [] n; destruct 1; constructor; by cofe_subst. `````` Jacques-Henri Jourdan committed May 30, 2016 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 `````` - intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto. exists (Cinl ca'); by repeat constructor. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto. exists (Cinr cb'); by repeat constructor. - intros ? [a|b|] [a'|b'|] H; inversion_clear H; cofe_subst; done. - intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O. - intros n [a|b|]; simpl; auto using cmra_validN_S. - intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc. - intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm. - intros [a|b|] ? [=]; subst; auto. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. constructor; eauto using cmra_pcore_l. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. constructor; eauto using cmra_pcore_l. - intros [a|b|] ? [=]; subst; auto. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. feed inversion (cmra_pcore_idemp b cb); repeat constructor; auto. - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=]. + exists CsumBot. rewrite csum_included; eauto. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. `````` Ralf Jung committed Jul 25, 2016 222 `````` destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto. `````` Jacques-Henri Jourdan committed May 30, 2016 223 224 `````` exists (Cinl ca'). rewrite csum_included; eauto 10. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. `````` Ralf Jung committed Jul 25, 2016 225 `````` destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto. `````` Jacques-Henri Jourdan committed May 30, 2016 226 227 228 `````` exists (Cinr cb'). rewrite csum_included; eauto 10. - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done. - intros n [a|b|] y1 y2 Hx Hx'. `````` Robbert Krebbers committed Aug 14, 2016 229 230 231 232 233 234 235 `````` + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'. destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); auto. exists (Cinl z1), (Cinl z2). by repeat constructor. + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'. destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); auto. exists (Cinr z1), (Cinr z2). by repeat constructor. + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'. `````` Jacques-Henri Jourdan committed May 30, 2016 236 237 ``````Qed. Canonical Structure csumR := `````` Ralf Jung committed Nov 22, 2016 238 `````` CMRAT (csum A B) csum_ofe_mixin csum_cmra_mixin. `````` Jacques-Henri Jourdan committed May 30, 2016 239 240 241 242 243 244 245 246 247 248 249 250 251 `````` Global Instance csum_cmra_discrete : CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR. Proof. split; first apply _. by move=>[a|b|] HH /=; try apply cmra_discrete_valid. Qed. Global Instance Cinl_persistent a : Persistent a → Persistent (Cinl a). Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. Global Instance Cinr_persistent b : Persistent b → Persistent (Cinr b). Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. `````` Jacques-Henri Jourdan committed May 31, 2016 252 ``````Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a). `````` Jacques-Henri Jourdan committed May 31, 2016 253 ``````Proof. by move=> H[]? =>[/H||]. Qed. `````` Jacques-Henri Jourdan committed May 31, 2016 254 ``````Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b). `````` Jacques-Henri Jourdan committed May 31, 2016 255 ``````Proof. by move=> H[]? =>[|/H|]. Qed. `````` Jacques-Henri Jourdan committed May 31, 2016 256 `````` `````` Robbert Krebbers committed Sep 28, 2016 257 258 259 260 261 ``````Global Instance Cinl_cmra_homomorphism : CMRAHomomorphism Cinl. Proof. split. apply _. done. Qed. Global Instance Cinr_cmra_homomorphism : CMRAHomomorphism Cinr. Proof. split. apply _. done. Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 262 263 ``````(** Internalized properties *) Lemma csum_equivI {M} (x y : csum A B) : `````` Robbert Krebbers committed May 31, 2016 264 265 266 267 268 269 `````` x ≡ y ⊣⊢ (match x, y with | Cinl a, Cinl a' => a ≡ a' | Cinr b, Cinr b' => b ≡ b' | CsumBot, CsumBot => True | _, _ => False end : uPred M). `````` Jacques-Henri Jourdan committed May 30, 2016 270 271 272 273 274 ``````Proof. uPred.unseal; do 2 split; first by destruct 1. by destruct x, y; try destruct 1; try constructor. Qed. Lemma csum_validI {M} (x : csum A B) : `````` Robbert Krebbers committed May 31, 2016 275 276 277 278 279 `````` ✓ x ⊣⊢ (match x with | Cinl a => ✓ a | Cinr b => ✓ b | CsumBot => False end : uPred M). `````` Jacques-Henri Jourdan committed May 30, 2016 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 ``````Proof. uPred.unseal. by destruct x. Qed. (** Updates *) Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 → Cinl a1 ~~> Cinl a2. Proof. intros Ha n [[a|b|]|] ?; simpl in *; auto. - by apply (Ha n (Some a)). - by apply (Ha n None). Qed. Lemma csum_update_r (b1 b2 : B) : b1 ~~> b2 → Cinr b1 ~~> Cinr b2. Proof. intros Hb n [[a|b|]|] ?; simpl in *; auto. - by apply (Hb n (Some b)). - by apply (Hb n None). Qed. Lemma csum_updateP_l (P : A → Prop) (Q : csum A B → Prop) a : a ~~>: P → (∀ a', P a' → Q (Cinl a')) → Cinl a ~~>: Q. Proof. intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm. - destruct (Hx n (Some a')) as (c&?&?); naive_solver. - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l. Qed. Lemma csum_updateP_r (P : B → Prop) (Q : csum A B → Prop) b : b ~~>: P → (∀ b', P b' → Q (Cinr b')) → Cinr b ~~>: Q. Proof. intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm. - destruct (Hx n (Some b')) as (c&?&?); naive_solver. - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l. Qed. Lemma csum_updateP'_l (P : A → Prop) a : a ~~>: P → Cinl a ~~>: λ m', ∃ a', m' = Cinl a' ∧ P a'. Proof. eauto using csum_updateP_l. Qed. Lemma csum_updateP'_r (P : B → Prop) b : b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'. Proof. eauto using csum_updateP_r. Qed. `````` Robbert Krebbers committed Oct 06, 2016 315 316 317 `````` Lemma csum_local_update_l (a1 a2 a1' a2' : A) : (a1,a2) ~l~> (a1',a2') → (Cinl a1,Cinl a2) ~l~> (Cinl a1',Cinl a2'). `````` Jacques-Henri Jourdan committed Jul 01, 2016 318 ``````Proof. `````` Robbert Krebbers committed Oct 06, 2016 319 320 321 322 `````` intros Hup n mf ? Ha1; simpl in *. destruct (Hup n (mf ≫= maybe Cinl)); auto. { by destruct mf as [[]|]; inversion_clear Ha1. } split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor. `````` Jacques-Henri Jourdan committed Jul 01, 2016 323 ``````Qed. `````` Robbert Krebbers committed Oct 06, 2016 324 325 ``````Lemma csum_local_update_r (b1 b2 b1' b2' : B) : (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2'). `````` Jacques-Henri Jourdan committed Jul 01, 2016 326 ``````Proof. `````` Robbert Krebbers committed Oct 06, 2016 327 328 329 330 `````` intros Hup n mf ? Ha1; simpl in *. destruct (Hup n (mf ≫= maybe Cinr)); auto. { by destruct mf as [[]|]; inversion_clear Ha1. } split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor. `````` Jacques-Henri Jourdan committed Jul 01, 2016 331 ``````Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 332 333 334 335 336 337 338 339 340 ``````End cmra. Arguments csumR : clear implicits. (* Functor *) Instance csum_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') : CMRAMonotone f → CMRAMonotone g → CMRAMonotone (csum_map f g). Proof. split; try apply _. `````` Robbert Krebbers committed Sep 28, 2016 341 `````` - intros n [a|b|]; simpl; auto using cmra_monotone_validN. `````` Jacques-Henri Jourdan committed May 30, 2016 342 343 `````` - intros x y; rewrite !csum_included. intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl; `````` Ralf Jung committed Jul 25, 2016 344 `````` eauto 10 using cmra_monotone. `````` Jacques-Henri Jourdan committed May 30, 2016 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 ``````Qed. Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {| rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B); rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg) |}. Next Obligation. by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne. Qed. Next Obligation. intros Fa Fb A B x. rewrite /= -{2}(csum_map_id x). apply csum_map_ext=>y; apply rFunctor_id. Qed. Next Obligation. intros Fa Fb A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -csum_map_compose. apply csum_map_ext=>y; apply rFunctor_compose. Qed. Instance csumRF_contractive Fa Fb : rFunctorContractive Fa → rFunctorContractive Fb → rFunctorContractive (csumRF Fa Fb). Proof. by intros ?? A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive. Qed.``````