cofe.v 18.6 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.base. `````` Robbert Krebbers committed Nov 11, 2015 2 3 4 `````` (** Unbundeled version *) Class Dist A := dist : nat → relation A. `````` Robbert Krebbers committed Nov 12, 2015 5 ``````Instance: Params (@dist) 3. `````` Robbert Krebbers committed Nov 11, 2015 6 7 ``````Notation "x ={ n }= y" := (dist n x y) (at level 70, n at next level, format "x ={ n }= y"). `````` Robbert Krebbers committed Jan 16, 2016 8 ``````Hint Extern 0 (?x ={_}= ?y) => reflexivity. `````` Robbert Krebbers committed Nov 11, 2015 9 ``````Hint Extern 0 (_ ={_}= _) => symmetry; assumption. `````` Robbert Krebbers committed Jan 13, 2016 10 11 12 13 14 15 16 17 `````` Tactic Notation "cofe_subst" ident(x) := repeat match goal with | _ => progress simplify_equality' | H:@dist ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x end. Tactic Notation "cofe_subst" := `````` Robbert Krebbers committed Nov 17, 2015 18 19 `````` repeat match goal with | _ => progress simplify_equality' `````` Robbert Krebbers committed Dec 21, 2015 20 21 `````` | H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x `````` Robbert Krebbers committed Nov 17, 2015 22 `````` end. `````` Robbert Krebbers committed Nov 11, 2015 23 24 25 26 27 28 29 30 31 `````` Record chain (A : Type) `{Dist A} := { chain_car :> nat → A; chain_cauchy n i : n ≤ i → chain_car n ={n}= chain_car i }. Arguments chain_car {_ _} _ _. Arguments chain_cauchy {_ _} _ _ _ _. Class Compl A `{Dist A} := compl : chain A → A. `````` Robbert Krebbers committed Jan 14, 2016 32 33 34 35 36 37 ``````Record CofeMixin A `{Equiv A, Compl A} := { mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y; mixin_dist_equivalence n : Equivalence (dist n); mixin_dist_S n x y : x ={S n}= y → x ={n}= y; mixin_dist_0 x y : x ={0}= y; mixin_conv_compl (c : chain A) n : compl c ={n}= c n `````` Robbert Krebbers committed Nov 11, 2015 38 39 40 41 42 43 44 45 46 47 ``````}. Class Contractive `{Dist A, Dist B} (f : A -> B) := contractive n : Proper (dist n ==> dist (S n)) f. (** Bundeled version *) Structure cofeT := CofeT { cofe_car :> Type; cofe_equiv : Equiv cofe_car; cofe_dist : Dist cofe_car; cofe_compl : Compl cofe_car; `````` Robbert Krebbers committed Jan 14, 2016 48 `````` cofe_mixin : CofeMixin cofe_car `````` Robbert Krebbers committed Nov 11, 2015 49 ``````}. `````` Robbert Krebbers committed Jan 14, 2016 50 ``````Arguments CofeT {_ _ _ _} _. `````` Robbert Krebbers committed Nov 11, 2015 51 ``````Add Printing Constructor cofeT. `````` Robbert Krebbers committed Jan 14, 2016 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 ``````Existing Instances cofe_equiv cofe_dist cofe_compl. Arguments cofe_car : simpl never. Arguments cofe_equiv : simpl never. Arguments cofe_dist : simpl never. Arguments cofe_compl : simpl never. Arguments cofe_mixin : simpl never. (** Lifting properties from the mixin *) Section cofe_mixin. Context {A : cofeT}. Implicit Types x y : A. Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y. Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed. Global Instance dist_equivalence n : Equivalence (@dist A _ n). Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed. Lemma dist_S n x y : x ={S n}= y → x ={n}= y. Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed. Lemma dist_0 x y : x ={0}= y. Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed. Lemma conv_compl (c : chain A) n : compl c ={n}= c n. Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed. End cofe_mixin. Hint Extern 0 (_ ={0}= _) => apply dist_0. `````` Robbert Krebbers committed Nov 11, 2015 76 77 78 `````` (** General properties *) Section cofe. `````` Robbert Krebbers committed Jan 14, 2016 79 80 `````` Context {A : cofeT}. Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 81 82 83 84 85 86 87 `````` Global Instance cofe_equivalence : Equivalence ((≡) : relation A). Proof. split. * by intros x; rewrite equiv_dist. * by intros x y; rewrite !equiv_dist. * by intros x y z; rewrite !equiv_dist; intros; transitivity y. Qed. `````` Robbert Krebbers committed Jan 14, 2016 88 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 89 90 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Robbert Krebbers committed Dec 15, 2015 91 92 `````` * by transitivity x1; [|transitivity y1]. * by transitivity x2; [|transitivity y2]. `````` Robbert Krebbers committed Nov 11, 2015 93 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 94 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 95 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 96 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 97 98 99 `````` Qed. Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x). Proof. by apply dist_proper. Qed. `````` Robbert Krebbers committed Jan 14, 2016 100 `````` Lemma dist_le (x y : A) n n' : x ={n}= y → n' ≤ n → x ={n'}= y. `````` Robbert Krebbers committed Nov 11, 2015 101 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 102 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 103 104 `````` `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100. Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed. `````` Robbert Krebbers committed Jan 14, 2016 105 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 106 107 108 109 `````` `{!∀ n, Proper (dist n ==> dist n ==> dist n) f} : Proper ((≡) ==> (≡) ==> (≡)) f | 100. Proof. unfold Proper, respectful; setoid_rewrite equiv_dist. `````` Robbert Krebbers committed Jan 13, 2016 110 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 111 112 `````` Qed. Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n → compl c1 ={n}= compl c2. `````` Robbert Krebbers committed Jan 13, 2016 113 `````` Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed. `````` Robbert Krebbers committed Nov 11, 2015 114 115 `````` Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2. Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed. `````` Robbert Krebbers committed Jan 14, 2016 116 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 117 118 `````` Proper (dist n ==> dist n) f | 100. Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed. `````` Robbert Krebbers committed Jan 14, 2016 119 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 120 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Nov 11, 2015 121 122 ``````End cofe. `````` Robbert Krebbers committed Nov 22, 2015 123 124 125 126 ``````(** Mapping a chain *) Program Definition chain_map `{Dist A, Dist B} (f : A → B) `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B := {| chain_car n := f (c n) |}. `````` Robbert Krebbers committed Jan 14, 2016 127 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 128 `````` `````` Robbert Krebbers committed Nov 18, 2015 129 ``````(** Timeless elements *) `````` Robbert Krebbers committed Jan 14, 2016 130 131 ``````Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y → x ≡ y. Arguments timeless {_} _ {_} _ _. `````` Robbert Krebbers committed Feb 01, 2016 132 133 134 135 136 ``````Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ={S n}= y. Proof. split; intros; [by apply equiv_dist|]. apply (timeless _), dist_le with (S n); auto with lia. Qed. `````` Robbert Krebbers committed Nov 18, 2015 137 `````` `````` Robbert Krebbers committed Nov 11, 2015 138 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 139 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 140 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 141 ``````Next Obligation. `````` Robbert Krebbers committed Jan 14, 2016 142 `````` intros A ? f ? n; induction n as [|n IH]; intros i ?; first done. `````` Robbert Krebbers committed Jan 13, 2016 143 `````` destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia. `````` Robbert Krebbers committed Nov 11, 2015 144 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 145 ``````Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 146 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Nov 11, 2015 147 148 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 149 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 150 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 151 152 `````` Proof. apply equiv_dist; intros n; unfold fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 153 `````` rewrite (conv_compl (fixpoint_chain f) n). `````` Robbert Krebbers committed Jan 13, 2016 154 `````` by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia. `````` Robbert Krebbers committed Nov 11, 2015 155 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 156 157 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : (∀ z, f z ={n}= g z) → fixpoint f ={n}= fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 158 `````` Proof. `````` Robbert Krebbers committed Nov 17, 2015 159 `````` intros Hfg; unfold fixpoint. `````` Robbert Krebbers committed Jan 13, 2016 160 161 `````` rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n). induction n as [|n IH]; simpl in *; first done. `````` Robbert Krebbers committed Nov 11, 2015 162 163 `````` rewrite Hfg; apply contractive, IH; auto using dist_S. Qed. `````` Robbert Krebbers committed Nov 17, 2015 164 165 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 166 167 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 168 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 169 170 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 171 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 172 173 174 175 176 177 178 `````` cofe_mor_car :> A → B; cofe_mor_ne n : Proper (dist n ==> dist n) cofe_mor_car }. Arguments CofeMor {_ _} _ {_}. Add Printing Constructor cofeMor. Existing Instance cofe_mor_ne. `````` Robbert Krebbers committed Jan 14, 2016 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 ``````Section cofe_mor. Context {A B : cofeT}. Global Instance cofe_mor_proper (f : cofeMor A B) : Proper ((≡) ==> (≡)) f. Proof. apply ne_proper, cofe_mor_ne. Qed. Instance cofe_mor_equiv : Equiv (cofeMor A B) := λ f g, ∀ x, f x ≡ g x. Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ={n}= g x. Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B := {| chain_car n := c n x |}. Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed. Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c, {| cofe_mor_car x := compl (fun_chain c x) |}. Next Obligation. intros c n x y Hx. rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx. apply (chain_cauchy c); lia. Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 02, 2016 198 199 `````` * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. intros Hfg k; apply equiv_dist; intros n; apply Hfg. `````` Robbert Krebbers committed Jan 14, 2016 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 `````` * intros n; split. + by intros f x. + by intros f g ? x. + by intros f g h ?? x; transitivity (g x). * by intros n f g ? x; apply dist_S. * by intros f g x. * intros c n x; simpl. rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia. Qed. Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin. Global Instance cofe_mor_car_ne n : Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B). Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed. Global Instance cofe_mor_car_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _. Lemma cofe_mor_ext (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x. Proof. done. Qed. End cofe_mor. Arguments cofe_mor : clear implicits. `````` Robbert Krebbers committed Nov 11, 2015 221 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 222 223 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 224 225 226 227 228 229 230 231 232 233 `````` (** Identity and composition *) Definition cid {A} : A -n> A := CofeMor id. Instance: Params (@cid) 1. Definition ccompose {A B C} (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g). Instance: Params (@ccompose) 3. Infix "◎" := ccompose (at level 40, left associativity). Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n : f1 ={n}= f2 → g1 ={n}= g2 → f1 ◎ g1 ={n}= f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 234 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 235 236 `````` (** unit *) `````` Robbert Krebbers committed Jan 14, 2016 237 238 239 240 241 242 ``````Section unit. Instance unit_dist : Dist unit := λ _ _ _, True. Instance unit_compl : Compl unit := λ _, (). Definition unit_cofe_mixin : CofeMixin unit. Proof. by repeat split; try exists 0. Qed. Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin. `````` Robbert Krebbers committed Jan 31, 2016 243 244 `````` Global Instance unit_timeless (x : ()) : Timeless x. Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 245 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 246 247 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 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 ``````Section product. Context {A B : cofeT}. Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n). Global Instance pair_ne : Proper (dist n ==> dist n ==> dist n) (@pair A B) := _. Global Instance fst_ne : Proper (dist n ==> dist n) (@fst A B) := _. Global Instance snd_ne : Proper (dist n ==> dist n) (@snd A B) := _. Instance prod_compl : Compl (A * B) := λ c, (compl (chain_map fst c), compl (chain_map snd c)). Definition prod_cofe_mixin : CofeMixin (A * B). Proof. split. * intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. rewrite !equiv_dist; naive_solver. * apply _. * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. * by split. * intros c n; split. apply (conv_compl (chain_map fst c) n). apply (conv_compl (chain_map snd c) n). Qed. Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin. Global Instance pair_timeless (x : A) (y : B) : Timeless x → Timeless y → Timeless (x,y). Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed. End product. Arguments prodC : clear implicits. Typeclasses Opaque prod_dist. Instance prod_map_ne {A A' B B' : cofeT} n : `````` Robbert Krebbers committed Nov 11, 2015 279 280 281 282 283 284 285 286 287 `````` Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n) (@prod_map A A' B B'). Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed. Definition prodC_map {A A' B B'} (f : A -n> A') (g : B -n> B') : prodC A B -n> prodC A' B' := CofeMor (prod_map f g). Instance prodC_map_ne {A A' B B'} n : Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B'). Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed. `````` Robbert Krebbers committed Nov 16, 2015 288 289 290 291 292 293 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. Instance discrete_dist : Dist A := λ n x y, match n with 0 => True | S n => x ≡ y end. Instance discrete_compl : Compl A := λ c, c 1. `````` Robbert Krebbers committed Jan 14, 2016 294 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 295 296 297 298 299 300 301 302 `````` Proof. split. * intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)]. * intros [|n]; [done|apply _]. * by intros [|n]. * done. * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 303 304 `````` Definition discreteC : cofeT := CofeT discrete_cofe_mixin. Global Instance discrete_timeless (x : A) : Timeless (x : discreteC). `````` Robbert Krebbers committed Nov 18, 2015 305 `````` Proof. by intros y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 306 ``````End discrete_cofe. `````` Robbert Krebbers committed Nov 22, 2015 307 ``````Arguments discreteC _ {_ _}. `````` Robbert Krebbers committed Nov 16, 2015 308 `````` `````` Robbert Krebbers committed Nov 22, 2015 309 ``````Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _. `````` Robbert Krebbers committed Jan 16, 2016 310 311 312 ``````Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A). Proof. by intros A x y. Qed. `````` Robbert Krebbers committed Dec 11, 2015 313 314 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 315 `````` `````` Robbert Krebbers committed Nov 16, 2015 316 317 ``````(** Later *) Inductive later (A : Type) : Type := Later { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 318 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Nov 16, 2015 319 320 ``````Arguments Later {_} _. Arguments later_car {_} _. `````` Robbert Krebbers committed Jan 18, 2016 321 322 ``````Lemma later_eta {A} (x : later A) : Later (later_car x) = x. Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 323 `````` `````` Robbert Krebbers committed Nov 16, 2015 324 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 325 326 327 `````` Context {A : cofeT}. Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y. Instance later_dist : Dist (later A) := λ n x y, `````` Robbert Krebbers committed Nov 16, 2015 328 `````` match n with 0 => True | S n => later_car x ={n}= later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 329 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 330 `````` {| chain_car n := later_car (c (S n)) |}. `````` Robbert Krebbers committed Jan 14, 2016 331 332 333 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. Instance later_compl : Compl (later A) := λ c, Later (compl (later_chain c)). Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 334 335 336 337 338 339 340 341 342 343 344 345 `````` Proof. split. * intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). * intros [|n]; [by split|split]; unfold dist, later_dist. + by intros [x]. + by intros [x] [y]. + by intros [x] [y] [z] ??; transitivity y. * intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. * done. * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 346 347 `````` Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. Global Instance Later_contractive : Contractive (@Later A). `````` Robbert Krebbers committed Dec 21, 2015 348 `````` Proof. by intros n ??. Qed. `````` Robbert Krebbers committed Jan 16, 2016 349 350 `````` Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A). Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 351 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := Later (f (later_car x)). Instance later_map_ne {A B : cofeT} (f : A → B) n : Proper (dist (pred n) ==> dist (pred n)) f → Proper (dist n ==> dist n) (later_map f) | 0. Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed. Lemma later_map_id {A} (x : later A) : later_map id x = x. Proof. by destruct x. Qed. Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) : later_map (g ∘ f) x = later_map g (later_map f x). Proof. by destruct x. Qed. Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B := CofeMor (later_map f). Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B). Proof. intros n f g Hf n'; apply Hf. Qed. `````` Robbert Krebbers committed Feb 02, 2016 370 371 372 373 `````` (** Indexed product *) (** 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 04, 2016 374 375 376 377 378 379 ``````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. Definition iprod_singleton `{∀ x x' : A, Decision (x = x')} {B : A → cofeT} `{∀ x : A, Empty (B x)} (x : A) (y : B x) : iprod B := iprod_insert x y (λ _, ∅). `````` Robbert Krebbers committed Feb 02, 2016 380 381 382 `````` Section iprod_cofe. Context {A} {B : A → cofeT}. `````` Robbert Krebbers committed Feb 04, 2016 383 384 `````` Implicit Types x : A. Implicit Types f g : iprod B. `````` Robbert Krebbers committed Feb 02, 2016 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 `````` 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 04, 2016 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 `````` Context `{∀ x x' : A, Decision (x = x')}. 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 _. 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. 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. `````` Robbert Krebbers committed Feb 02, 2016 438 439 ``````End iprod_cofe. `````` Robbert Krebbers committed Feb 03, 2016 440 ``````Arguments iprodC {_} _. `````` Robbert Krebbers committed Feb 04, 2016 441 442 443 `````` Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) (g : iprod B1) : iprod B2 := λ x, f _ (g x). `````` Robbert Krebbers committed Feb 04, 2016 444 445 446 447 448 449 450 451 452 ``````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. `````` Robbert Krebbers committed Feb 04, 2016 453 454 455 456 457 458 ``````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). `````` Robbert Krebbers committed Feb 04, 2016 459 ``````Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n : `````` Robbert Krebbers committed Feb 04, 2016 460 461 `````` Proper (dist n ==> dist n) (@iprodC_map A B1 B2). Proof. intros f1 f2 Hf g x; apply Hf. Qed.``````