iprod.v 12.2 KB
 Ralf Jung committed Feb 08, 2016 1 2 3 4 5 6 7 8 9 ``````Require Export algebra.cmra. Require Import algebra.functor. (** Indexed product *) (** Need to put this in a definition to make canonical structures to work. *) Definition iprod {A} (B : A → cofeT) := ∀ x, B x. Definition iprod_insert `{∀ x x' : A, Decision (x = x')} {B : A → cofeT} (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. `````` Ralf Jung committed Feb 08, 2016 10 ``````Global Instance iprod_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅. `````` Ralf Jung committed Feb 08, 2016 11 ``````Definition iprod_lookup_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} x : ∅ x = ∅ := eq_refl. `````` Ralf Jung committed Feb 08, 2016 12 13 ``````Definition iprod_singleton `{∀ x x' : A, Decision (x = x')} {B : A → cofeT} `{∀ x : A, Empty (B x)} `````` Ralf Jung committed Feb 08, 2016 14 `````` (x : A) (y : B x) : iprod B := iprod_insert x y ∅. `````` Ralf Jung committed Feb 08, 2016 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 `````` Section iprod_cofe. Context {A} {B : A → cofeT}. Implicit Types x : A. Implicit Types f g : iprod B. Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x. Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ={n}= g x. 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. * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. intros Hfg k; apply equiv_dist; intros n; apply Hfg. * intros n; split. + by intros f x. + by intros f g ? x. + by intros f g h ?? x; transitivity (g x). * intros n f g Hfg x; apply dist_S, Hfg. * by intros f g x. * intros c n x. rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n). apply (chain_cauchy c); lia. Qed. Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin. `````` Ralf Jung committed Feb 08, 2016 44 `````` (** Properties of iprod_insert. *) `````` Ralf Jung committed Feb 08, 2016 45 `````` Context `{∀ x x' : A, Decision (x = x')}. `````` Ralf Jung committed Feb 08, 2016 46 `````` `````` Ralf Jung committed Feb 08, 2016 47 48 49 50 51 52 `````` Global Instance iprod_insert_ne x n : 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. `````` Ralf Jung committed Feb 08, 2016 53 `````` `````` Ralf Jung committed Feb 08, 2016 54 55 `````` Global Instance iprod_insert_proper x : Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _. `````` Ralf Jung committed Feb 08, 2016 56 `````` `````` Ralf Jung committed Feb 08, 2016 57 58 59 60 61 `````` 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. `````` Ralf Jung committed Feb 08, 2016 62 `````` `````` Ralf Jung committed Feb 08, 2016 63 64 65 66 `````` 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. `````` Ralf Jung committed Feb 08, 2016 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 `````` Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x). Proof. intros ? y Hf. cut (f ≡ iprod_insert x y f). { move=>{Hf} Hf. by rewrite (Hf x) iprod_lookup_insert. } apply timeless; first by apply _. move=>x'. destruct (decide (x = x')). - subst x'. rewrite iprod_lookup_insert; done. - rewrite iprod_lookup_insert_ne //. Qed. Global Instance iprod_insert_timeless f x y : Timeless f → Timeless y → Timeless (iprod_insert x y f). Proof. intros ?? g Heq x'. destruct (decide (x = x')). - subst x'. rewrite iprod_lookup_insert. apply (timeless _). rewrite -(Heq x) iprod_lookup_insert; done. - rewrite iprod_lookup_insert_ne //. apply (timeless _). rewrite -(Heq x') iprod_lookup_insert_ne; done. Qed. (** Properties of iprod_singletom. *) `````` Ralf Jung committed Feb 08, 2016 92 93 94 95 96 97 98 99 100 101 102 `````` Context `{∀ x : A, Empty (B x)}. Global Instance iprod_singleton_ne x n : 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 _. Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y. Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed. Lemma iprod_lookup_singleton_ne x x' y : x ≠ x' → (iprod_singleton x y) x' = ∅. Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed. `````` Ralf Jung committed Feb 08, 2016 103 104 105 106 107 108 109 110 `````` Context `{∀ x : A, Timeless (∅ : B x)}. Instance iprod_empty_timeless : Timeless (∅ : iprod B). Proof. intros f Hf x. by apply (timeless _). Qed. Global Instance iprod_singleton_timeless x (y : B x) : Timeless y → Timeless (iprod_singleton x y) := _. `````` Ralf Jung committed Feb 08, 2016 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 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 ``````End iprod_cofe. Arguments iprodC {_} _. 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. 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. Section iprod_cmra. Context {A} {B : A → cmraT}. Implicit Types f g : iprod B. Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x. Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl. Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x). Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl. Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} (f x). Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x. Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl. Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x. Proof. split. * by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x). * intros Hh; exists (g ⩪ f)=> x; specialize (Hh x). by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus. Qed. Definition iprod_cmra_mixin : CMRAMixin (iprod B). Proof. split. * 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). * by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i). * by intros f x. * intros n f Hf x; apply cmra_validN_S, Hf. * by intros f1 f2 f3 x; rewrite iprod_lookup_op associative. * by intros f1 f2 x; rewrite iprod_lookup_op commutative. * by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l. * by intros f x; rewrite iprod_lookup_unit cmra_unit_idempotent. * intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x. by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf. * intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. * intros n f1 f2; rewrite iprod_includedN_spec=> Hf x. by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf. Qed. Definition iprod_cmra_extend_mixin : CMRAExtendMixin (iprod B). Proof. intros n f f1 f2 Hf Hf12. set (g x := cmra_extend_op 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_ands; intros x; apply (proj2_sig (g x)). Qed. Canonical Structure iprodRA : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin. Global Instance iprod_cmra_identity `{∀ x, Empty (B x)} : (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA. Proof. intros ?; split. * intros n x; apply cmra_empty_valid. * by intros f x; rewrite iprod_lookup_op left_id. * by intros f Hf x; apply (timeless _). Qed. `````` Ralf Jung committed Feb 08, 2016 190 `````` (** Properties of iprod_insert. *) `````` Ralf Jung committed Feb 08, 2016 191 `````` Context `{∀ x x' : A, Decision (x = x')}. `````` Ralf Jung committed Feb 08, 2016 192 `````` `````` Ralf Jung committed Feb 08, 2016 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 `````` 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. intros Hy1 HP gf n Hg. destruct (Hy1 (gf x) n) as (y2&?&?). { 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. rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with congruence. Qed. `````` Ralf Jung committed Feb 08, 2016 216 `````` (** Properties of iprod_singleton. *) `````` Ralf Jung committed Feb 08, 2016 217 `````` Context `{∀ x, Empty (B x)} `{∀ x, CMRAIdentity (B x)}. `````` Ralf Jung committed Feb 08, 2016 218 219 220 221 222 223 224 225 226 227 228 229 `````` Lemma iprod_validN_singleton n x (y : B x) : ✓{n} y <-> ✓{n} (iprod_singleton x y). Proof. split. - move=>Hx x'. destruct (decide (x = x')). + subst x'. by rewrite iprod_lookup_singleton. + rewrite iprod_lookup_singleton_ne //; []. by apply cmra_empty_valid. - move=>Hm. move: (Hm x). by rewrite iprod_lookup_singleton. Qed. `````` Ralf Jung committed Feb 08, 2016 230 231 232 233 234 235 236 237 238 `````` Lemma iprod_unit_singleton x (y : B x) : unit (iprod_singleton x y) ≡ iprod_singleton x (unit y). Proof. move=>x'. rewrite iprod_lookup_unit. destruct (decide (x = x')). - subst x'. by rewrite !iprod_lookup_singleton. - rewrite !iprod_lookup_singleton_ne //; []. by apply cmra_unit_empty. Qed. `````` Ralf Jung committed Feb 08, 2016 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 `````` 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 [->|]. * by rewrite iprod_lookup_op !iprod_lookup_singleton. * by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id. 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 → iprod_singleton x y1 ~~>: λ g', ∃ y2, g' = iprod_singleton x y2 ∧ P y2. Proof. eauto using iprod_singleton_updateP. Qed. Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) : (∅ ~~>: P) → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q. Proof. intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?). { apply: Hg. } exists (iprod_singleton x y2). split; first by apply HQ. intros x'; destruct (decide (x' = x)) as [->|]; rewrite iprod_lookup_op /iprod_singleton ?iprod_lookup_insert //; []. move:(Hg x'). by rewrite iprod_lookup_insert_ne // left_id. Qed. Lemma iprod_singleton_update x y1 y2 : y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2. Proof. by intros; apply iprod_insert_update. Qed. End iprod_cmra. Arguments iprodRA {_} _. 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. split. * intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x. rewrite /iprod_map; apply includedN_preserving, Hf. * intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg. Qed. Program Definition iprodF {A} (Σ : A → iFunctor) : iFunctor := {| ifunctor_car B := iprodRA (λ x, Σ x B); ifunctor_map B1 B2 f := iprodC_map (λ x, ifunctor_map (Σ x) f); |}. Next Obligation. by intros A Σ B1 B2 n f f' ? g; apply iprodC_map_ne=>x; apply ifunctor_map_ne. Qed. Next Obligation. intros A Σ B g. rewrite /= -{2}(iprod_map_id g). apply iprod_map_ext=> x; apply ifunctor_map_id. Qed. Next Obligation. intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose. apply iprod_map_ext=> y; apply ifunctor_map_compose. Qed.``````