csum.v 15.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 {_ _}. `````` Maxime Dénès committed Jan 24, 2019 20 21 22 ``````Instance: Params (@Cinl) 2 := {}. Instance: Params (@Cinr) 2 := {}. Instance: Params (@CsumBot) 2 := {}. `````` Robbert Krebbers committed Jan 30, 2017 23 `````` `````` 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. `````` Robbert Krebbers committed Oct 25, 2017 99 100 ``````Global Instance csum_ofe_discrete : OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumC. `````` Robbert Krebbers committed Oct 25, 2017 101 ``````Proof. by inversion_clear 3; constructor; apply (discrete _). Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 102 ``````Global Instance csum_leibniz : `````` Robbert Krebbers committed Jun 04, 2019 103 `````` LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumC. `````` Jacques-Henri Jourdan committed May 30, 2016 104 105 ``````Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed. `````` Robbert Krebbers committed Oct 25, 2017 106 107 108 109 ``````Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a). Proof. by inversion_clear 2; constructor; apply (discrete _). Qed. Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b). Proof. by inversion_clear 2; constructor; apply (discrete _). Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 110 111 112 113 114 115 116 117 118 119 120 121 ``````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. `````` Maxime Dénès committed Jan 24, 2019 122 ``````Instance: Params (@csum_map) 4 := {}. `````` Jacques-Henri Jourdan committed May 30, 2016 123 124 125 126 127 128 129 `````` 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 130 ``````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 131 132 `````` (∀ 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 133 ``````Instance csum_map_cmra_ne {A A' B B' : ofeT} n : `````` Jacques-Henri Jourdan committed May 30, 2016 134 135 136 137 138 139 `````` 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 140 141 142 ``````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 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 `````` 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. `````` Jacques-Henri Jourdan committed Feb 01, 2017 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 `````` - unfold included. intros [[a'|b'|] Hy]; destruct x as [a|b|]; inversion_clear Hy; eauto 10. - 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_includedN n x y : x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a') ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼{n} b'). Proof. split. - unfold includedN. intros [[a'|b'|] Hy]; destruct x as [a|b|]; inversion_clear Hy; eauto 10. `````` Jacques-Henri Jourdan committed May 30, 2016 200 201 202 203 204 205 `````` - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]]. + destruct x; exists CsumBot; constructor. + exists (Cinl c); by constructor. + exists (Cinr c); by constructor. Qed. `````` Robbert Krebbers committed Oct 25, 2017 206 ``````Lemma csum_cmra_mixin : CmraMixin (csum A B). `````` Jacques-Henri Jourdan committed May 30, 2016 207 208 ``````Proof. split. `````` Robbert Krebbers committed Feb 09, 2017 209 `````` - intros [] n; destruct 1; constructor; by ofe_subst. `````` Jacques-Henri Jourdan committed May 30, 2016 210 211 212 213 214 215 216 `````` - 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. `````` Robbert Krebbers committed Feb 09, 2017 217 `````` - intros ? [a|b|] [a'|b'|] H; inversion_clear H; ofe_subst; done. `````` Jacques-Henri Jourdan committed May 30, 2016 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 `````` - 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 235 `````` destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto. `````` Jacques-Henri Jourdan committed May 30, 2016 236 237 `````` exists (Cinl ca'). rewrite csum_included; eauto 10. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. `````` Ralf Jung committed Jul 25, 2016 238 `````` destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto. `````` Jacques-Henri Jourdan committed May 30, 2016 239 240 241 `````` 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'. `````` 242 243 `````` + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'. destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); [done|apply (inj Cinl), Hx'|]. `````` Robbert Krebbers committed Aug 14, 2016 244 `````` exists (Cinl z1), (Cinl z2). by repeat constructor. `````` 245 246 `````` + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'. destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); [done|apply (inj Cinr), Hx'|]. `````` Robbert Krebbers committed Aug 14, 2016 247 248 `````` 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 249 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 250 ``````Canonical Structure csumR := CmraT (csum A B) csum_cmra_mixin. `````` Jacques-Henri Jourdan committed May 30, 2016 251 252 `````` Global Instance csum_cmra_discrete : `````` Robbert Krebbers committed Oct 25, 2017 253 `````` CmraDiscrete A → CmraDiscrete B → CmraDiscrete csumR. `````` Jacques-Henri Jourdan committed May 30, 2016 254 255 256 257 258 ``````Proof. split; first apply _. by move=>[a|b|] HH /=; try apply cmra_discrete_valid. Qed. `````` Robbert Krebbers committed Oct 25, 2017 259 260 261 262 ``````Global Instance Cinl_core_id a : CoreId a → CoreId (Cinl a). Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed. Global Instance Cinr_core_id b : CoreId b → CoreId (Cinr b). Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 263 `````` `````` Jacques-Henri Jourdan committed May 31, 2016 264 ``````Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a). `````` Jacques-Henri Jourdan committed May 31, 2016 265 ``````Proof. by move=> H[]? =>[/H||]. Qed. `````` Jacques-Henri Jourdan committed May 31, 2016 266 ``````Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b). `````` Jacques-Henri Jourdan committed May 31, 2016 267 ``````Proof. by move=> H[]? =>[|/H|]. Qed. `````` Jacques-Henri Jourdan committed May 31, 2016 268 `````` `````` Jacques-Henri Jourdan committed Feb 01, 2017 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 ``````Global Instance Cinl_cancelable a : Cancelable a → Cancelable (Cinl a). Proof. move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ. constructor. by eapply (cancelableN a). Qed. Global Instance Cinr_cancelable b : Cancelable b → Cancelable (Cinr b). Proof. move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ. constructor. by eapply (cancelableN b). Qed. Global Instance Cinl_id_free a : IdFree a → IdFree (Cinl a). Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed. Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b). Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 285 286 ``````(** Internalized properties *) Lemma csum_equivI {M} (x y : csum A B) : `````` Robbert Krebbers committed Dec 10, 2018 287 288 289 290 291 292 `````` x ≡ y ⊣⊢@{uPredI M} match x, y with | Cinl a, Cinl a' => a ≡ a' | Cinr b, Cinr b' => b ≡ b' | CsumBot, CsumBot => True | _, _ => False end. `````` Jacques-Henri Jourdan committed May 30, 2016 293 294 295 296 297 ``````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 Dec 10, 2018 298 299 300 301 302 `````` ✓ x ⊣⊢@{uPredI M} match x with | Cinl a => ✓ a | Cinr b => ✓ b | CsumBot => False end. `````` Jacques-Henri Jourdan committed May 30, 2016 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 ``````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 338 339 340 `````` 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 341 ``````Proof. `````` Robbert Krebbers committed Oct 06, 2016 342 343 344 345 `````` 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 346 ``````Qed. `````` Robbert Krebbers committed Oct 06, 2016 347 348 ``````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 349 ``````Proof. `````` Robbert Krebbers committed Oct 06, 2016 350 351 352 353 `````` 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 354 ``````Qed. `````` Jacques-Henri Jourdan committed May 30, 2016 355 356 357 358 359 ``````End cmra. Arguments csumR : clear implicits. (* Functor *) `````` 360 ``````Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') : `````` Robbert Krebbers committed Oct 25, 2017 361 `````` CmraMorphism f → CmraMorphism g → CmraMorphism (csum_map f g). `````` Jacques-Henri Jourdan committed May 30, 2016 362 363 ``````Proof. split; try apply _. `````` 364 365 366 `````` - intros n [a|b|]; simpl; auto using cmra_morphism_validN. - move=> [a|b|]=>//=; rewrite cmra_morphism_pcore; by destruct pcore. - intros [xa|ya|] [xb|yb|]=>//=; by rewrite -cmra_morphism_op. `````` Jacques-Henri Jourdan committed May 30, 2016 367 368 369 ``````Qed. Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {| `````` Robbert Krebbers committed Jun 04, 2019 370 371 `````` 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) `````` Jacques-Henri Jourdan committed May 30, 2016 372 373 ``````|}. Next Obligation. `````` Robbert Krebbers committed Jun 04, 2019 374 `````` by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne. `````` Jacques-Henri Jourdan committed May 30, 2016 375 376 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Jun 04, 2019 377 `````` intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x). `````` Jacques-Henri Jourdan committed May 30, 2016 378 379 380 `````` apply csum_map_ext=>y; apply rFunctor_id. Qed. Next Obligation. `````` Robbert Krebbers committed Jun 04, 2019 381 `````` intros Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -csum_map_compose. `````` Jacques-Henri Jourdan committed May 30, 2016 382 383 384 385 386 387 388 `````` apply csum_map_ext=>y; apply rFunctor_compose. Qed. Instance csumRF_contractive Fa Fb : rFunctorContractive Fa → rFunctorContractive Fb → rFunctorContractive (csumRF Fa Fb). Proof. `````` Robbert Krebbers committed Jun 04, 2019 389 390 `````` intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg. by apply csumC_map_ne; try apply rFunctor_contractive. `````` Jacques-Henri Jourdan committed May 30, 2016 391 ``Qed.``