iprod.v 13.9 KB
 Robbert Krebbers committed Oct 25, 2016 1 2 ``````From iris.algebra Require Export cmra. From iris.base_logic Require Import base_logic. `````` Robbert Krebbers committed Mar 11, 2016 3 ``````From iris.prelude Require Import finite. `````` Ralf Jung committed Jan 05, 2017 4 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Feb 08, 2016 5 `````` `````` Robbert Krebbers committed Feb 08, 2016 6 ``````(** * Indexed product *) `````` Ralf Jung committed Feb 08, 2016 7 ``````(** Need to put this in a definition to make canonical structures to work. *) `````` Ralf Jung committed Nov 22, 2016 8 9 ``````Definition iprod `{Finite A} (B : A → ofeT) := ∀ x, B x. Definition iprod_insert `{Finite A} {B : A → ofeT} `````` Ralf Jung committed Feb 08, 2016 10 11 `````` (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 May 27, 2016 12 ``````Instance: Params (@iprod_insert) 5. `````` Ralf Jung committed Feb 08, 2016 13 14 `````` Section iprod_cofe. `````` Ralf Jung committed Nov 22, 2016 15 `````` Context `{Finite A} {B : A → ofeT}. `````` Ralf Jung committed Feb 08, 2016 16 17 `````` Implicit Types x : A. Implicit Types f g : iprod B. `````` Robbert Krebbers committed Feb 08, 2016 18 `````` `````` Ralf Jung committed Feb 08, 2016 19 `````` Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x. `````` Ralf Jung committed Feb 10, 2016 20 `````` Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Ralf Jung committed Nov 22, 2016 21 `````` Definition iprod_ofe_mixin : OfeMixin (iprod B). `````` Ralf Jung committed Feb 08, 2016 22 23 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 24 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Ralf Jung committed Feb 08, 2016 25 `````` intros Hfg k; apply equiv_dist; intros n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 26 `````` - intros n; split. `````` Ralf Jung committed Feb 08, 2016 27 28 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 29 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 30 `````` - intros n f g Hfg x; apply dist_S, Hfg. `````` Ralf Jung committed Feb 08, 2016 31 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 32 33 34 35 36 37 38 39 40 41 42 43 `````` Canonical Structure iprodC : ofeT := OfeT (iprod B) iprod_ofe_mixin. Program Definition iprod_chain (c : chain iprodC) (x : A) : chain (B x) := {| chain_car n := c n x |}. Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed. Global Program Instance iprod_cofe `{∀ a, Cofe (B a)} : Cofe iprodC := {| compl c x := compl (iprod_chain c x) |}. Next Obligation. intros ? n c x. rewrite (conv_compl n (iprod_chain c x)). apply (chain_cauchy c); lia. Qed. `````` Ralf Jung committed Feb 08, 2016 44 `````` `````` Ralf Jung committed Feb 08, 2016 45 `````` (** Properties of iprod_insert. *) `````` Ralf Jung committed Jan 27, 2017 46 47 `````` Global Instance iprod_insert_ne x : NonExpansive2 (iprod_insert x). `````` Ralf Jung committed Feb 08, 2016 48 `````` Proof. `````` Ralf Jung committed Jan 27, 2017 49 `````` intros n y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert. `````` Ralf Jung committed Feb 08, 2016 50 51 52 53 `````` by destruct (decide _) as [[]|]. Qed. Global Instance iprod_insert_proper x : Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _. `````` Ralf Jung committed Feb 08, 2016 54 `````` `````` Ralf Jung committed Feb 08, 2016 55 56 57 58 59 60 61 62 63 `````` 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 64 `````` Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x). `````` Ralf Jung committed Feb 08, 2016 65 `````` Proof. `````` Robbert Krebbers committed Feb 08, 2016 66 `````` intros ? y ?. `````` Ralf Jung committed Feb 08, 2016 67 `````` cut (f ≡ iprod_insert x y f). `````` Robbert Krebbers committed Feb 08, 2016 68 `````` { by move=> /(_ x)->; rewrite iprod_lookup_insert. } `````` Robbert Krebbers committed May 27, 2016 69 70 `````` apply (timeless _)=> x'; destruct (decide (x = x')) as [->|]; by rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne. `````` Ralf Jung committed Feb 08, 2016 71 72 73 74 `````` 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 75 `````` intros ?? g Heq x'; destruct (decide (x = x')) as [->|]. `````` Robbert Krebbers committed Feb 17, 2016 76 `````` - rewrite iprod_lookup_insert. `````` Ralf Jung committed Feb 18, 2016 77 `````` apply: timeless. by rewrite -(Heq x') iprod_lookup_insert. `````` Robbert Krebbers committed Feb 17, 2016 78 `````` - rewrite iprod_lookup_insert_ne //. `````` Ralf Jung committed Feb 18, 2016 79 `````` apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne. `````` Ralf Jung committed Feb 08, 2016 80 `````` Qed. `````` Ralf Jung committed Feb 08, 2016 81 82 ``````End iprod_cofe. `````` Robbert Krebbers committed May 27, 2016 83 ``````Arguments iprodC {_ _ _} _. `````` Ralf Jung committed Feb 08, 2016 84 85 `````` Section iprod_cmra. `````` Robbert Krebbers committed May 27, 2016 86 `````` Context `{Finite A} {B : A → ucmraT}. `````` Ralf Jung committed Feb 08, 2016 87 `````` Implicit Types f g : iprod B. `````` Robbert Krebbers committed Feb 08, 2016 88 `````` `````` Ralf Jung committed Feb 08, 2016 89 `````` Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x. `````` Robbert Krebbers committed May 28, 2016 90 `````` Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)). `````` Robbert Krebbers committed Feb 24, 2016 91 `````` Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x. `````` Robbert Krebbers committed Feb 11, 2016 92 `````` Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x. `````` Robbert Krebbers committed Feb 08, 2016 93 94 `````` Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl. `````` Ralf Jung committed Mar 08, 2016 95 `````` Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl. `````` Robbert Krebbers committed Feb 08, 2016 96 `````` `````` Robbert Krebbers committed Feb 26, 2016 97 `````` Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x. `````` Ralf Jung committed Feb 08, 2016 98 `````` Proof. `````` Robbert Krebbers committed Mar 11, 2016 99 100 `````` split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|]. intros [h ?]%finite_choice. by exists h. `````` Ralf Jung committed Feb 08, 2016 101 `````` Qed. `````` Robbert Krebbers committed Feb 08, 2016 102 `````` `````` Robbert Krebbers committed May 27, 2016 103 `````` Lemma iprod_cmra_mixin : CMRAMixin (iprod B). `````` Ralf Jung committed Feb 08, 2016 104 `````` Proof. `````` Robbert Krebbers committed May 28, 2016 105 106 `````` apply cmra_total_mixin. - eauto. `````` Robbert Krebbers committed Feb 17, 2016 107 `````` - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x). `````` Ralf Jung committed Mar 08, 2016 108 `````` - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x). `````` Robbert Krebbers committed Feb 17, 2016 109 `````` - by intros n f1 f2 Hf ? x; rewrite -(Hf x). `````` Robbert Krebbers committed Feb 24, 2016 110 111 112 `````` - 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 113 114 115 `````` - 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. `````` Ralf Jung committed Mar 08, 2016 116 117 `````` - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l. - by intros f x; rewrite iprod_lookup_core cmra_core_idemp. `````` Robbert Krebbers committed Feb 26, 2016 118 `````` - intros f1 f2; rewrite !iprod_included_spec=> Hf x. `````` Ralf Jung committed Jul 25, 2016 119 `````` by rewrite iprod_lookup_core; apply cmra_core_mono, Hf. `````` Robbert Krebbers committed Feb 17, 2016 120 `````` - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. `````` Robbert Krebbers committed Feb 24, 2016 121 `````` - intros n f f1 f2 Hf Hf12. `````` Robbert Krebbers committed Aug 14, 2016 122 123 124 125 126 127 `````` destruct (finite_choice (λ x (yy : B x * B x), f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg]. { intros x. specialize (Hf12 x). destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto. exists (y1,y2); eauto. } exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver. `````` Ralf Jung committed Feb 08, 2016 128 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 129 `````` Canonical Structure iprodR := `````` Ralf Jung committed Nov 22, 2016 130 `````` CMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 131 132 133 134 135 `````` Instance iprod_empty : Empty (iprod B) := λ x, ∅. Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl. Lemma iprod_ucmra_mixin : UCMRAMixin (iprod B). `````` Ralf Jung committed Feb 08, 2016 136 `````` Proof. `````` Robbert Krebbers committed May 27, 2016 137 138 `````` split. - intros x; apply ucmra_unit_valid. `````` Robbert Krebbers committed Feb 17, 2016 139 `````` - by intros f x; rewrite iprod_lookup_op left_id. `````` Robbert Krebbers committed May 28, 2016 140 `````` - constructor=> x. apply persistent_core, _. `````` Ralf Jung committed Feb 08, 2016 141 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 142 `````` Canonical Structure iprodUR := `````` Ralf Jung committed Nov 22, 2016 143 `````` UCMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin iprod_ucmra_mixin. `````` Ralf Jung committed Feb 08, 2016 144 `````` `````` Robbert Krebbers committed Aug 20, 2016 145 146 147 148 `````` Global Instance iprod_empty_timeless : (∀ i, Timeless (∅ : B i)) → Timeless (∅ : iprod B). Proof. intros ? f Hf x. by apply: timeless. Qed. `````` Robbert Krebbers committed Feb 13, 2016 149 `````` (** Internalized properties *) `````` Robbert Krebbers committed May 31, 2016 150 `````` Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 151 `````` Proof. by uPred.unseal. Qed. `````` Robbert Krebbers committed May 31, 2016 152 `````` Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 153 `````` Proof. by uPred.unseal. Qed. `````` Robbert Krebbers committed Feb 13, 2016 154 `````` `````` Ralf Jung committed Feb 08, 2016 155 `````` (** Properties of iprod_insert. *) `````` Ralf Jung committed Feb 08, 2016 156 157 158 159 `````` 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 May 28, 2016 160 161 `````` intros Hy1 HP; apply cmra_total_updateP. intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?). `````` Ralf Jung committed Feb 08, 2016 162 163 164 165 166 167 168 169 170 171 172 173 174 175 `````` { 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 176 `````` rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst. `````` Ralf Jung committed Feb 08, 2016 177 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 178 179 180 181 182 183 184 185 186 187 188 189 190 ``````End iprod_cmra. Arguments iprodR {_ _ _} _. Arguments iprodUR {_ _ _} _. Definition iprod_singleton `{Finite A} {B : A → ucmraT} (x : A) (y : B x) : iprod B := iprod_insert x y ∅. Instance: Params (@iprod_singleton) 5. Section iprod_singleton. Context `{Finite A} {B : A → ucmraT}. Implicit Types x : A. `````` Ralf Jung committed Jan 27, 2017 191 192 193 `````` Global Instance iprod_singleton_ne x : NonExpansive (iprod_singleton x : B x → _). Proof. intros n y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed. `````` Robbert Krebbers committed May 27, 2016 194 195 `````` Global Instance iprod_singleton_proper x : Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _. `````` Ralf Jung committed Feb 08, 2016 196 `````` `````` Robbert Krebbers committed May 27, 2016 197 198 199 200 201 `````` Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y. Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed. Lemma iprod_lookup_singleton_ne x x' (y : B x) : x ≠ x' → (iprod_singleton x y) x' = ∅. Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed. `````` Ralf Jung committed Feb 08, 2016 202 `````` `````` Robbert Krebbers committed May 27, 2016 203 `````` Global Instance iprod_singleton_timeless x (y : B x) : `````` Robbert Krebbers committed Aug 20, 2016 204 205 `````` (∀ i, Timeless (∅ : B i)) → Timeless y → Timeless (iprod_singleton x y). Proof. apply _. Qed. `````` Robbert Krebbers committed May 27, 2016 206 207 `````` Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y. `````` Ralf Jung committed Feb 08, 2016 208 `````` Proof. `````` Robbert Krebbers committed Feb 08, 2016 209 210 211 `````` 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 May 27, 2016 212 `````` by apply ucmra_unit_validN. `````` Ralf Jung committed Feb 08, 2016 213 214 `````` Qed. `````` Ralf Jung committed Mar 08, 2016 215 216 `````` Lemma iprod_core_singleton x (y : B x) : core (iprod_singleton x y) ≡ iprod_singleton x (core y). `````` Ralf Jung committed Feb 08, 2016 217 `````` Proof. `````` Robbert Krebbers committed Mar 15, 2016 218 219 `````` move=>x'; destruct (decide (x = x')) as [->|]; by rewrite iprod_lookup_core ?iprod_lookup_singleton `````` Robbert Krebbers committed May 28, 2016 220 `````` ?iprod_lookup_singleton_ne // (persistent_core ∅). `````` Ralf Jung committed Feb 08, 2016 221 222 `````` Qed. `````` Robbert Krebbers committed Mar 15, 2016 223 224 `````` Global Instance iprod_singleton_persistent x (y : B x) : Persistent y → Persistent (iprod_singleton x y). `````` Robbert Krebbers committed May 28, 2016 225 `````` Proof. by rewrite !persistent_total iprod_core_singleton=> ->. Qed. `````` Robbert Krebbers committed Mar 15, 2016 226 `````` `````` Ralf Jung committed Feb 08, 2016 227 228 229 230 `````` 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 231 232 `````` - 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 233 234 235 236 237 238 239 240 `````` 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 241 `````` iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2. `````` Ralf Jung committed Feb 08, 2016 242 `````` Proof. eauto using iprod_singleton_updateP. Qed. `````` Robbert Krebbers committed May 27, 2016 243 `````` Lemma iprod_singleton_update x (y1 y2 : B x) : `````` Robbert Krebbers committed Feb 08, 2016 244 245 `````` y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2. Proof. eauto using iprod_insert_update. Qed. `````` Ralf Jung committed Feb 08, 2016 246 247 `````` Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) : `````` Robbert Krebbers committed Feb 08, 2016 248 `````` ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q. `````` Ralf Jung committed Feb 08, 2016 249 `````` Proof. `````` Robbert Krebbers committed May 28, 2016 250 251 `````` intros Hx HQ; apply cmra_total_updateP. intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg. `````` Robbert Krebbers committed Feb 08, 2016 252 253 `````` exists (iprod_singleton x y2); split; [by apply HQ|]. intros x'; destruct (decide (x' = x)) as [->|]. `````` Robbert Krebbers committed Feb 17, 2016 254 255 `````` - by rewrite iprod_lookup_op iprod_lookup_singleton. - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg. `````` Ralf Jung committed Feb 08, 2016 256 `````` Qed. `````` Ralf Jung committed Feb 09, 2016 257 258 259 `````` 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. `````` Robbert Krebbers committed May 27, 2016 260 261 262 263 264 265 266 `````` Lemma iprod_singleton_update_empty x (y : B x) : ∅ ~~> y → ∅ ~~> iprod_singleton x y. Proof. rewrite !cmra_update_updateP; eauto using iprod_singleton_updateP_empty with subst. Qed. End iprod_singleton. `````` Ralf Jung committed Feb 08, 2016 267 `````` `````` Robbert Krebbers committed Feb 08, 2016 268 ``````(** * Functor *) `````` Ralf Jung committed Nov 22, 2016 269 ``````Definition iprod_map `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) `````` Robbert Krebbers committed Feb 08, 2016 270 271 `````` (g : iprod B1) : iprod B2 := λ x, f _ (g x). `````` Ralf Jung committed Nov 22, 2016 272 ``````Lemma iprod_map_ext `{Finite A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x) (g : iprod B1) : `````` Robbert Krebbers committed Feb 08, 2016 273 274 `````` (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g. Proof. done. Qed. `````` Ralf Jung committed Nov 22, 2016 275 ``````Lemma iprod_map_id `{Finite A} {B : A → ofeT} (g : iprod B) : `````` Robbert Krebbers committed May 27, 2016 276 `````` iprod_map (λ _, id) g = g. `````` Robbert Krebbers committed Feb 08, 2016 277 ``````Proof. done. Qed. `````` Ralf Jung committed Nov 22, 2016 278 ``````Lemma iprod_map_compose `{Finite A} {B1 B2 B3 : A → ofeT} `````` Robbert Krebbers committed Feb 08, 2016 279 280 281 282 `````` (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. `````` Ralf Jung committed Nov 22, 2016 283 ``````Instance iprod_map_ne `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n : `````` Robbert Krebbers committed Feb 08, 2016 284 285 286 `````` (∀ 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. `````` Robbert Krebbers committed May 27, 2016 287 288 ``````Instance iprod_map_cmra_monotone `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) : `````` Ralf Jung committed Feb 08, 2016 289 290 `````` (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f). Proof. `````` Robbert Krebbers committed Feb 26, 2016 291 `````` split; first apply _. `````` Robbert Krebbers committed Sep 28, 2016 292 `````` - intros n g Hg x; rewrite /iprod_map; apply (cmra_monotone_validN (f _)), Hg. `````` Robbert Krebbers committed Feb 26, 2016 293 `````` - intros g1 g2; rewrite !iprod_included_spec=> Hf x. `````` Ralf Jung committed Jul 25, 2016 294 `````` rewrite /iprod_map; apply (cmra_monotone _), Hf. `````` Ralf Jung committed Feb 08, 2016 295 296 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 297 ``````Definition iprodC_map `{Finite A} {B1 B2 : A → ofeT} `````` Robbert Krebbers committed May 27, 2016 298 `````` (f : iprod (λ x, B1 x -n> B2 x)) : `````` Robbert Krebbers committed Feb 08, 2016 299 `````` iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f). `````` Ralf Jung committed Jan 27, 2017 300 301 302 ``````Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} : NonExpansive (@iprodC_map A _ _ B1 B2). Proof. intros n f1 f2 Hf g x; apply Hf. Qed. `````` Robbert Krebbers committed Feb 08, 2016 303 `````` `````` Robbert Krebbers committed May 27, 2016 304 ``````Program Definition iprodCF `{Finite C} (F : C → cFunctor) : cFunctor := {| `````` Robbert Krebbers committed Mar 02, 2016 305 306 `````` 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 307 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 308 ``````Next Obligation. `````` Robbert Krebbers committed May 27, 2016 309 `````` intros C ?? F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne. `````` Robbert Krebbers committed Mar 07, 2016 310 ``````Qed. `````` Ralf Jung committed Feb 08, 2016 311 ``````Next Obligation. `````` Robbert Krebbers committed May 27, 2016 312 `````` intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g). `````` Robbert Krebbers committed Mar 02, 2016 313 `````` apply iprod_map_ext=> y; apply cFunctor_id. `````` Ralf Jung committed Feb 08, 2016 314 315 ``````Qed. Next Obligation. `````` Robbert Krebbers committed May 27, 2016 316 `````` intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose. `````` Robbert Krebbers committed Mar 02, 2016 317 318 `````` apply iprod_map_ext=>y; apply cFunctor_compose. Qed. `````` Robbert Krebbers committed May 27, 2016 319 ``````Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) : `````` Ralf Jung committed Mar 07, 2016 320 321 322 323 324 325 `````` (∀ 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 May 27, 2016 326 327 328 ``````Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {| urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B); urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg) `````` Robbert Krebbers committed Mar 02, 2016 329 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 330 ``````Next Obligation. `````` Robbert Krebbers committed Mar 11, 2016 331 `````` intros C ?? F A1 A2 B1 B2 n ?? g. `````` Robbert Krebbers committed May 27, 2016 332 `````` by apply iprodC_map_ne=>?; apply urFunctor_ne. `````` Robbert Krebbers committed Mar 07, 2016 333 ``````Qed. `````` Robbert Krebbers committed Mar 02, 2016 334 ``````Next Obligation. `````` Robbert Krebbers committed Mar 11, 2016 335 `````` intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g). `````` Robbert Krebbers committed May 27, 2016 336 `````` apply iprod_map_ext=> y; apply urFunctor_id. `````` Robbert Krebbers committed Mar 02, 2016 337 338 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 11, 2016 339 `````` intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose. `````` Robbert Krebbers committed May 27, 2016 340 `````` apply iprod_map_ext=>y; apply urFunctor_compose. `````` Ralf Jung committed Feb 08, 2016 341 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 342 343 ``````Instance iprodURF_contractive `{Finite C} (F : C → urFunctor) : (∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F). `````` Ralf Jung committed Mar 07, 2016 344 345 ``````Proof. intros ? A1 A2 B1 B2 n ?? g. `````` Robbert Krebbers committed May 27, 2016 346 `````` by apply iprodC_map_ne=>c; apply urFunctor_contractive. `````` Ralf Jung committed Mar 07, 2016 347 ``Qed.``