iprod.v 12.2 KB
 Ralf Jung committed Feb 08, 2016 1 2 3 ``````Require Export algebra.cmra. Require Import algebra.functor. `````` Robbert Krebbers committed Feb 08, 2016 4 ``````(** * Indexed product *) `````` Ralf Jung committed Feb 08, 2016 5 6 7 8 9 ``````(** 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. `````` 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 ∅. `````` Ralf Jung committed Feb 08, 2016 15 16 17 18 19 `````` Section iprod_cofe. Context {A} {B : A → cofeT}. Implicit Types x : A. Implicit Types f g : iprod B. `````` Robbert Krebbers committed Feb 08, 2016 20 `````` `````` Ralf Jung committed Feb 08, 2016 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 `````` 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. `````` Robbert Krebbers committed Feb 08, 2016 45 46 47 48 49 50 51 52 53 `````` (** Properties of empty *) Section empty. Context `{∀ x, Empty (B x)}. Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl. Instance iprod_empty_timeless : (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B). Proof. intros ? f Hf x. by apply (timeless _). Qed. End empty. `````` Ralf Jung committed Feb 08, 2016 54 `````` (** Properties of iprod_insert. *) `````` Ralf Jung committed Feb 08, 2016 55 `````` Context `{∀ x x' : A, Decision (x = x')}. `````` Ralf Jung committed Feb 08, 2016 56 `````` `````` Ralf Jung committed Feb 08, 2016 57 58 59 60 61 62 63 64 `````` 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. Global Instance iprod_insert_proper x : Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _. `````` Ralf Jung committed Feb 08, 2016 65 `````` `````` Ralf Jung committed Feb 08, 2016 66 67 68 69 70 71 72 73 74 `````` 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 75 `````` Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x). `````` Ralf Jung committed Feb 08, 2016 76 `````` Proof. `````` Robbert Krebbers committed Feb 08, 2016 77 `````` intros ? y ?. `````` Ralf Jung committed Feb 08, 2016 78 `````` cut (f ≡ iprod_insert x y f). `````` Robbert Krebbers committed Feb 08, 2016 79 80 81 `````` { by move=> /(_ x)->; rewrite iprod_lookup_insert. } by apply (timeless _)=>x'; destruct (decide (x = x')) as [->|]; rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne. `````` Ralf Jung committed Feb 08, 2016 82 83 84 85 `````` 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 86 87 88 89 90 `````` intros ?? g Heq x'; destruct (decide (x = x')) as [->|]. * rewrite iprod_lookup_insert. apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert. * rewrite iprod_lookup_insert_ne //. apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert_ne. `````` Ralf Jung committed Feb 08, 2016 91 92 93 `````` Qed. (** Properties of iprod_singletom. *) `````` Ralf Jung committed Feb 08, 2016 94 `````` Context `{∀ x : A, Empty (B x)}. `````` Robbert Krebbers committed Feb 08, 2016 95 `````` `````` Ralf Jung committed Feb 08, 2016 96 97 98 99 100 `````` 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 _. `````` Robbert Krebbers committed Feb 08, 2016 101 `````` `````` Ralf Jung committed Feb 08, 2016 102 103 `````` 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 104 `````` Lemma iprod_lookup_singleton_ne x x' y: x ≠ x' → (iprod_singleton x y) x' = ∅. `````` Ralf Jung committed Feb 08, 2016 105 `````` Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed. `````` Ralf Jung committed Feb 08, 2016 106 107 `````` Global Instance iprod_singleton_timeless x (y : B x) : `````` Robbert Krebbers committed Feb 08, 2016 108 109 `````` (∀ 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 110 111 112 113 114 115 116 ``````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 117 `````` `````` Ralf Jung committed Feb 08, 2016 118 119 120 121 `````` Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x. Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x). 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. `````` Robbert Krebbers committed Feb 08, 2016 122 123 124 `````` 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 08, 2016 125 `````` Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl. `````` Robbert Krebbers committed Feb 08, 2016 126 `````` `````` Ralf Jung committed Feb 08, 2016 127 128 129 130 131 132 133 `````` 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. `````` Robbert Krebbers committed Feb 08, 2016 134 `````` `````` Ralf Jung committed Feb 08, 2016 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 `````` 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 172 `````` (** Properties of iprod_insert. *) `````` Ralf Jung committed Feb 08, 2016 173 `````` Context `{∀ x x' : A, Decision (x = x')}. `````` Ralf Jung committed Feb 08, 2016 174 `````` `````` Ralf Jung committed Feb 08, 2016 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 `````` 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. `````` Robbert Krebbers committed Feb 08, 2016 194 `````` rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst. `````` Ralf Jung committed Feb 08, 2016 195 196 `````` Qed. `````` Ralf Jung committed Feb 08, 2016 197 `````` (** Properties of iprod_singleton. *) `````` Robbert Krebbers committed Feb 08, 2016 198 `````` Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}. `````` Ralf Jung committed Feb 08, 2016 199 `````` `````` Robbert Krebbers committed Feb 08, 2016 200 201 `````` Lemma iprod_singleton_validN n x (y : B x) : ✓{n} (iprod_singleton x y) ↔ ✓{n} y. `````` Ralf Jung committed Feb 08, 2016 202 `````` Proof. `````` Robbert Krebbers committed Feb 08, 2016 203 204 205 206 `````` split; [by move=>/(_ x); rewrite iprod_lookup_singleton|]. move=>Hx x'; destruct (decide (x = x')) as [->|]; rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //. by apply cmra_empty_valid. `````` Ralf Jung committed Feb 08, 2016 207 208 `````` Qed. `````` Ralf Jung committed Feb 08, 2016 209 210 211 `````` 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 212 213 214 `````` 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 215 216 `````` Qed. `````` Ralf Jung committed Feb 08, 2016 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 `````` 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. `````` Robbert Krebbers committed Feb 08, 2016 233 234 235 `````` 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 236 237 `````` Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) : `````` Robbert Krebbers committed Feb 08, 2016 238 `````` ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q. `````` Ralf Jung committed Feb 08, 2016 239 `````` Proof. `````` Robbert Krebbers committed Feb 08, 2016 240 241 242 243 244 `````` intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?); first apply Hg. exists (iprod_singleton x y2); split; [by apply HQ|]. intros x'; destruct (decide (x' = x)) as [->|]. * by rewrite iprod_lookup_op iprod_lookup_singleton. * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg. `````` Ralf Jung committed Feb 08, 2016 245 246 247 248 249 `````` Qed. End iprod_cmra. Arguments iprodRA {_} _. `````` Robbert Krebbers committed Feb 08, 2016 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 ``````(** * 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 268 269 270 271 272 273 274 275 276 ``````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. `````` Robbert Krebbers committed Feb 08, 2016 277 278 279 280 281 282 ``````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. `````` Ralf Jung committed Feb 08, 2016 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 ``````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.``````