iprod.v 13.7 KB
Newer Older
 Robbert Krebbers committed Feb 13, 2016 1 From algebra Require Export cmra. Robbert Krebbers committed Mar 02, 2016 2 From algebra Require Import upred. Ralf Jung committed Feb 08, 2016 3 Robbert Krebbers committed Feb 08, 2016 4 (** * Indexed product *) Ralf Jung committed Feb 08, 2016 5 6 (** Need to put this in a definition to make canonical structures to work. *) Definition iprod {A} (B : A → cofeT) := ∀ x, B x. Robbert Krebbers committed Feb 08, 2016 7 Definition iprod_insert {A} {B : A → cofeT} `{∀ x x' : A, Decision (x = x')} Ralf Jung committed Feb 08, 2016 8 9 (x : A) (y : B x) (f : iprod B) : iprod B := λ x', match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end. Robbert Krebbers committed Feb 08, 2016 10 11 12 13 Global Instance iprod_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅. Definition iprod_singleton {A} {B : A → cofeT} `{∀ x x' : A, Decision (x = x'), ∀ x : A, Empty (B x)} Ralf Jung committed Feb 08, 2016 14 (x : A) (y : B x) : iprod B := iprod_insert x y ∅. Robbert Krebbers committed Feb 08, 2016 15 16 Instance: Params (@iprod_insert) 4. Instance: Params (@iprod_singleton) 5. Ralf Jung committed Feb 08, 2016 17 18 19 20 21 Section iprod_cofe. Context {A} {B : A → cofeT}. Implicit Types x : A. Implicit Types f g : iprod B. Robbert Krebbers committed Feb 08, 2016 22 Ralf Jung committed Feb 08, 2016 23 Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x. Ralf Jung committed Feb 10, 2016 24 Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x. Ralf Jung committed Feb 08, 2016 25 26 27 28 29 30 31 32 Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) := {| chain_car n := c n x |}. Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed. Program Instance iprod_compl : Compl (iprod B) := λ c x, compl (iprod_chain c x). Definition iprod_cofe_mixin : CofeMixin (iprod B). Proof. split. Robbert Krebbers committed Feb 17, 2016 33 - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. Ralf Jung committed Feb 08, 2016 34 intros Hfg k; apply equiv_dist; intros n; apply Hfg. Robbert Krebbers committed Feb 17, 2016 35 - intros n; split. Ralf Jung committed Feb 08, 2016 36 37 + by intros f x. + by intros f g ? x. Ralf Jung committed Feb 20, 2016 38 + by intros f g h ?? x; trans (g x). Robbert Krebbers committed Feb 17, 2016 39 - intros n f g Hfg x; apply dist_S, Hfg. Robbert Krebbers committed Feb 18, 2016 40 41 - intros n c x. rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)). Ralf Jung committed Feb 08, 2016 42 43 44 45 apply (chain_cauchy c); lia. Qed. Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin. Robbert Krebbers committed Feb 08, 2016 46 47 48 49 (** Properties of empty *) Section empty. Context `{∀ x, Empty (B x)}. Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl. Ralf Jung committed Feb 09, 2016 50 Global Instance iprod_empty_timeless : Robbert Krebbers committed Feb 08, 2016 51 (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B). Ralf Jung committed Feb 18, 2016 52 Proof. intros ? f Hf x. by apply: timeless. Qed. Robbert Krebbers committed Feb 08, 2016 53 54 End empty. Ralf Jung committed Feb 08, 2016 55 (** Properties of iprod_insert. *) Ralf Jung committed Feb 08, 2016 56 Context `{∀ x x' : A, Decision (x = x')}. Ralf Jung committed Feb 08, 2016 57 Robbert Krebbers committed Feb 18, 2016 58 Global Instance iprod_insert_ne n x : Ralf Jung committed Feb 08, 2016 59 60 61 62 63 64 65 Proper (dist n ==> dist n ==> dist n) (iprod_insert x). Proof. intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert. by destruct (decide _) as [[]|]. Qed. Global Instance iprod_insert_proper x : Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _. Ralf Jung committed Feb 08, 2016 66 Ralf Jung committed Feb 08, 2016 67 68 69 70 71 72 73 74 75 Lemma iprod_lookup_insert f x y : (iprod_insert x y f) x = y. Proof. rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done. by rewrite (proof_irrel Hx eq_refl). Qed. Lemma iprod_lookup_insert_ne f x x' y : x ≠ x' → (iprod_insert x y f) x' = f x'. Proof. by rewrite /iprod_insert; destruct (decide _). Qed. Robbert Krebbers committed Feb 08, 2016 76 Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x). Ralf Jung committed Feb 08, 2016 77 Proof. Robbert Krebbers committed Feb 08, 2016 78 intros ? y ?. Ralf Jung committed Feb 08, 2016 79 cut (f ≡ iprod_insert x y f). Robbert Krebbers committed Feb 08, 2016 80 { by move=> /(_ x)->; rewrite iprod_lookup_insert. } Ralf Jung committed Feb 18, 2016 81 by apply: timeless=>x'; destruct (decide (x = x')) as [->|]; Robbert Krebbers committed Feb 08, 2016 82 rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne. Ralf Jung committed Feb 08, 2016 83 84 85 86 Qed. Global Instance iprod_insert_timeless f x y : Timeless f → Timeless y → Timeless (iprod_insert x y f). Proof. Robbert Krebbers committed Feb 08, 2016 87 intros ?? g Heq x'; destruct (decide (x = x')) as [->|]. Robbert Krebbers committed Feb 17, 2016 88 - rewrite iprod_lookup_insert. Ralf Jung committed Feb 18, 2016 89 apply: timeless. by rewrite -(Heq x') iprod_lookup_insert. Robbert Krebbers committed Feb 17, 2016 90 - rewrite iprod_lookup_insert_ne //. Ralf Jung committed Feb 18, 2016 91 apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne. Ralf Jung committed Feb 08, 2016 92 93 94 Qed. (** Properties of iprod_singletom. *) Ralf Jung committed Feb 08, 2016 95 Context `{∀ x : A, Empty (B x)}. Robbert Krebbers committed Feb 08, 2016 96 Robbert Krebbers committed Feb 18, 2016 97 Global Instance iprod_singleton_ne n x : Ralf Jung committed Feb 08, 2016 98 99 100 101 Proper (dist n ==> dist n) (iprod_singleton x). Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed. Global Instance iprod_singleton_proper x : Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _. Robbert Krebbers committed Feb 08, 2016 102 Ralf Jung committed Feb 08, 2016 103 104 Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y. Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed. Robbert Krebbers committed Feb 08, 2016 105 Lemma iprod_lookup_singleton_ne x x' y: x ≠ x' → (iprod_singleton x y) x' = ∅. Ralf Jung committed Feb 08, 2016 106 Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed. Ralf Jung committed Feb 08, 2016 107 108 Global Instance iprod_singleton_timeless x (y : B x) : Robbert Krebbers committed Feb 08, 2016 109 110 (∀ x : A, Timeless (∅ : B x)) → Timeless y → Timeless (iprod_singleton x y). Proof. eauto using iprod_insert_timeless, iprod_empty_timeless. Qed. Ralf Jung committed Feb 08, 2016 111 112 113 114 115 116 117 End iprod_cofe. Arguments iprodC {_} _. Section iprod_cmra. Context {A} {B : A → cmraT}. Implicit Types f g : iprod B. Robbert Krebbers committed Feb 08, 2016 118 Ralf Jung committed Feb 08, 2016 119 120 Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x. Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x). Robbert Krebbers committed Feb 24, 2016 121 Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x. Robbert Krebbers committed Feb 11, 2016 122 Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x. Ralf Jung committed Feb 29, 2016 123 Instance iprod_div : Div (iprod B) := λ f g x, f x ÷ g x. Robbert Krebbers committed Feb 08, 2016 124 125 126 Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl. Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl. Ralf Jung committed Feb 29, 2016 127 Definition iprod_lookup_div f g x : (f ÷ g) x = f x ÷ g x := eq_refl. Robbert Krebbers committed Feb 08, 2016 128 Robbert Krebbers committed Feb 26, 2016 129 Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x. Ralf Jung committed Feb 08, 2016 130 131 Proof. split. Robbert Krebbers committed Feb 17, 2016 132 - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x). Ralf Jung committed Feb 29, 2016 133 134 - intros Hh; exists (g ÷ f)=> x; specialize (Hh x). by rewrite /op /iprod_op /div /iprod_div cmra_op_div. Ralf Jung committed Feb 08, 2016 135 Qed. Robbert Krebbers committed Feb 08, 2016 136 Ralf Jung committed Feb 08, 2016 137 138 139 Definition iprod_cmra_mixin : CMRAMixin (iprod B). Proof. split. Robbert Krebbers committed Feb 17, 2016 140 141 142 - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x). - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x). - by intros n f1 f2 Hf ? x; rewrite -(Hf x). Ralf Jung committed Feb 29, 2016 143 - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_div (Hf i) (Hg i). Robbert Krebbers committed Feb 24, 2016 144 145 146 - intros g; split. + intros Hg n i; apply cmra_valid_validN, Hg. + intros Hg i; apply cmra_valid_validN=> n; apply Hg. Robbert Krebbers committed Feb 17, 2016 147 148 149 150 151 - intros n f Hf x; apply cmra_validN_S, Hf. - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc. - by intros f1 f2 x; rewrite iprod_lookup_op comm. - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l. - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp. Robbert Krebbers committed Feb 26, 2016 152 153 - intros f1 f2; rewrite !iprod_included_spec=> Hf x. by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf. Robbert Krebbers committed Feb 17, 2016 154 - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. Robbert Krebbers committed Feb 26, 2016 155 - intros f1 f2; rewrite iprod_included_spec=> Hf x. Ralf Jung committed Feb 29, 2016 156 by rewrite iprod_lookup_op iprod_lookup_div cmra_op_div; try apply Hf. Robbert Krebbers committed Feb 24, 2016 157 158 159 160 - intros n f f1 f2 Hf Hf12. set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)). split_and?; intros x; apply (proj2_sig (g x)). Ralf Jung committed Feb 08, 2016 161 Qed. Robbert Krebbers committed Mar 01, 2016 162 Canonical Structure iprodR : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin. Ralf Jung committed Feb 08, 2016 163 Global Instance iprod_cmra_identity `{∀ x, Empty (B x)} : Robbert Krebbers committed Mar 01, 2016 164 (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodR. Ralf Jung committed Feb 08, 2016 165 166 Proof. intros ?; split. Robbert Krebbers committed Feb 24, 2016 167 - intros x; apply cmra_empty_valid. Robbert Krebbers committed Feb 17, 2016 168 169 - by intros f x; rewrite iprod_lookup_op left_id. - by apply _. Ralf Jung committed Feb 08, 2016 170 171 Qed. Robbert Krebbers committed Feb 13, 2016 172 173 (** Internalized properties *) Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I. Robbert Krebbers committed Feb 25, 2016 174 Proof. by uPred.unseal. Qed. Robbert Krebbers committed Feb 13, 2016 175 Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I. Robbert Krebbers committed Feb 25, 2016 176 Proof. by uPred.unseal. Qed. Robbert Krebbers committed Feb 13, 2016 177 Ralf Jung committed Feb 08, 2016 178 (** Properties of iprod_insert. *) Ralf Jung committed Feb 08, 2016 179 Context `{∀ x x' : A, Decision (x = x')}. Ralf Jung committed Feb 08, 2016 180 Ralf Jung committed Feb 08, 2016 181 182 183 184 Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 : y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) → iprod_insert x y1 g ~~>: Q. Proof. Robbert Krebbers committed Feb 18, 2016 185 intros Hy1 HP n gf Hg. destruct (Hy1 n (gf x)) as (y2&?&?). Ralf Jung committed Feb 08, 2016 186 187 188 189 190 191 192 193 194 195 196 197 198 199 { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. } exists (iprod_insert x y2 g); split; [auto|]. intros x'; destruct (decide (x' = x)) as [->|]; rewrite iprod_lookup_op ?iprod_lookup_insert //; []. move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne. Qed. Lemma iprod_insert_updateP' x (P : B x → Prop) g y1 : y1 ~~>: P → iprod_insert x y1 g ~~>: λ g', ∃ y2, g' = iprod_insert x y2 g ∧ P y2. Proof. eauto using iprod_insert_updateP. Qed. Lemma iprod_insert_update g x y1 y2 : y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g. Proof. Robbert Krebbers committed Feb 08, 2016 200 rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst. Ralf Jung committed Feb 08, 2016 201 202 Qed. Ralf Jung committed Feb 08, 2016 203 (** Properties of iprod_singleton. *) Robbert Krebbers committed Feb 08, 2016 204 Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}. Ralf Jung committed Feb 08, 2016 205 Robbert Krebbers committed Feb 11, 2016 206 Lemma iprod_singleton_validN n x (y: B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y. Ralf Jung committed Feb 08, 2016 207 Proof. Robbert Krebbers committed Feb 08, 2016 208 209 210 split; [by move=>/(_ x); rewrite iprod_lookup_singleton|]. move=>Hx x'; destruct (decide (x = x')) as [->|]; rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //. Robbert Krebbers committed Feb 24, 2016 211 by apply cmra_empty_validN. Ralf Jung committed Feb 08, 2016 212 213 Qed. Ralf Jung committed Feb 08, 2016 214 215 216 Lemma iprod_unit_singleton x (y : B x) : unit (iprod_singleton x y) ≡ iprod_singleton x (unit y). Proof. Robbert Krebbers committed Feb 08, 2016 217 218 219 by move=>x'; destruct (decide (x = x')) as [->|]; rewrite iprod_lookup_unit ?iprod_lookup_singleton ?iprod_lookup_singleton_ne // cmra_unit_empty. Ralf Jung committed Feb 08, 2016 220 221 Qed. Ralf Jung committed Feb 08, 2016 222 223 224 225 Lemma iprod_op_singleton (x : A) (y1 y2 : B x) : iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2). Proof. intros x'; destruct (decide (x' = x)) as [->|]. Robbert Krebbers committed Feb 17, 2016 226 227 - by rewrite iprod_lookup_op !iprod_lookup_singleton. - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id. Ralf Jung committed Feb 08, 2016 228 229 230 231 232 233 234 235 Qed. Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 : y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → iprod_singleton x y1 ~~>: Q. Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed. Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 : y1 ~~>: P → Ralf Jung committed Feb 09, 2016 236 iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2. Ralf Jung committed Feb 08, 2016 237 Proof. eauto using iprod_singleton_updateP. Qed. Robbert Krebbers committed Feb 08, 2016 238 239 240 Lemma iprod_singleton_update x y1 y2 : y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2. Proof. eauto using iprod_insert_update. Qed. Ralf Jung committed Feb 08, 2016 241 242 Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) : Robbert Krebbers committed Feb 08, 2016 243 ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q. Ralf Jung committed Feb 08, 2016 244 Proof. Robbert Krebbers committed Feb 18, 2016 245 intros Hx HQ n gf Hg. destruct (Hx n (gf x)) as (y2&?&?); first apply Hg. Robbert Krebbers committed Feb 08, 2016 246 247 exists (iprod_singleton x y2); split; [by apply HQ|]. intros x'; destruct (decide (x' = x)) as [->|]. Robbert Krebbers committed Feb 17, 2016 248 249 - by rewrite iprod_lookup_op iprod_lookup_singleton. - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg. Ralf Jung committed Feb 08, 2016 250 Qed. Ralf Jung committed Feb 09, 2016 251 252 253 Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) : ∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2. Proof. eauto using iprod_singleton_updateP_empty. Qed. Ralf Jung committed Feb 08, 2016 254 255 End iprod_cmra. Robbert Krebbers committed Mar 01, 2016 256 Arguments iprodR {_} _. Ralf Jung committed Feb 08, 2016 257 Robbert Krebbers committed Feb 08, 2016 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 (** * Functor *) Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) (g : iprod B1) : iprod B2 := λ x, f _ (g x). Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g : (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g. Proof. done. Qed. Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g. Proof. done. Qed. Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT} (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) : iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g). Proof. done. Qed. Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n : (∀ x, Proper (dist n ==> dist n) (f x)) → Proper (dist n ==> dist n) (iprod_map f). Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed. Ralf Jung committed Feb 08, 2016 276 277 278 Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) : (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f). Proof. Robbert Krebbers committed Feb 26, 2016 279 split; first apply _. Robbert Krebbers committed Feb 26, 2016 280 - intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg. Robbert Krebbers committed Feb 26, 2016 281 - intros g1 g2; rewrite !iprod_included_spec=> Hf x. Robbert Krebbers committed Feb 26, 2016 282 rewrite /iprod_map; apply (included_preserving _), Hf. Ralf Jung committed Feb 08, 2016 283 284 Qed. Robbert Krebbers committed Feb 08, 2016 285 286 287 288 289 290 Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) : iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f). Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n : Proper (dist n ==> dist n) (@iprodC_map A B1 B2). Proof. intros f1 f2 Hf g x; apply Hf. Qed. Robbert Krebbers committed Mar 02, 2016 291 292 293 Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {| cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B); cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg) Ralf Jung committed Feb 08, 2016 294 |}. Robbert Krebbers committed Mar 07, 2016 295 296 297 Next Obligation. intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne. Qed. Ralf Jung committed Feb 08, 2016 298 Next Obligation. Robbert Krebbers committed Mar 02, 2016 299 300 intros C F A B g; simpl. rewrite -{2}(iprod_map_id g). apply iprod_map_ext=> y; apply cFunctor_id. Ralf Jung committed Feb 08, 2016 301 302 Qed. Next Obligation. Robbert Krebbers committed Mar 02, 2016 303 304 305 intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose. apply iprod_map_ext=>y; apply cFunctor_compose. Qed. Ralf Jung committed Mar 07, 2016 306 307 308 309 310 311 312 Instance iprodCF_contractive {C} (F : C → cFunctor) : (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F). Proof. intros ? A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>c; apply cFunctor_contractive. Qed. Robbert Krebbers committed Mar 02, 2016 313 314 315 316 Program Definition iprodRF {C} (F : C → rFunctor) : rFunctor := {| rFunctor_car A B := iprodR (λ c, rFunctor_car (F c) A B); rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg) |}. Robbert Krebbers committed Mar 07, 2016 317 318 319 Next Obligation. intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply rFunctor_ne. Qed. Robbert Krebbers committed Mar 02, 2016 320 321 322 323 324 325 326 Next Obligation. intros C F A B g; simpl. rewrite -{2}(iprod_map_id g). apply iprod_map_ext=> y; apply rFunctor_id. Qed. Next Obligation. intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose. apply iprod_map_ext=>y; apply rFunctor_compose. Ralf Jung committed Feb 08, 2016 327 Qed. Ralf Jung committed Mar 07, 2016 328 329 330 331 332 333 Instance iprodRF_contractive {C} (F : C → rFunctor) : (∀ c, rFunctorContractive (F c)) → rFunctorContractive (iprodRF F). Proof. intros ? A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>c; apply rFunctor_contractive. Qed.