cofe.v 14.3 KB
 Robbert Krebbers committed Jan 13, 2016 1 ``````Require Export modures.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 Nov 18, 2015 132 `````` `````` Robbert Krebbers committed Nov 11, 2015 133 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 134 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 135 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 136 ``````Next Obligation. `````` Robbert Krebbers committed Jan 14, 2016 137 `````` intros A ? f ? n; induction n as [|n IH]; intros i ?; first done. `````` Robbert Krebbers committed Jan 13, 2016 138 `````` destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia. `````` Robbert Krebbers committed Nov 11, 2015 139 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 140 ``````Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 141 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Nov 11, 2015 142 143 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 144 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 145 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 146 147 `````` Proof. apply equiv_dist; intros n; unfold fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 148 `````` rewrite (conv_compl (fixpoint_chain f) n). `````` Robbert Krebbers committed Jan 13, 2016 149 `````` by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia. `````` Robbert Krebbers committed Nov 11, 2015 150 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 151 152 `````` 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 153 `````` Proof. `````` Robbert Krebbers committed Nov 17, 2015 154 `````` intros Hfg; unfold fixpoint. `````` Robbert Krebbers committed Jan 13, 2016 155 156 `````` 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 157 158 `````` rewrite Hfg; apply contractive, IH; auto using dist_S. Qed. `````` Robbert Krebbers committed Nov 17, 2015 159 160 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 161 162 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 163 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 164 165 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 166 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 167 168 169 170 171 172 173 `````` 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 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 ``````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. * intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|]. intros HXY k; apply equiv_dist; intros n; apply HXY. * 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 216 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 217 218 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 219 220 221 222 223 224 225 226 227 228 `````` (** 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 229 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 230 231 `````` (** unit *) `````` Robbert Krebbers committed Jan 14, 2016 232 233 234 235 236 237 ``````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 238 239 `````` Global Instance unit_timeless (x : ()) : Timeless x. Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 240 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 241 242 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 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 ``````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 274 275 276 277 278 279 280 281 282 `````` 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 283 284 285 286 287 288 ``````(** 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 289 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 290 291 292 293 294 295 296 297 `````` 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 298 299 `````` Definition discreteC : cofeT := CofeT discrete_cofe_mixin. Global Instance discrete_timeless (x : A) : Timeless (x : discreteC). `````` Robbert Krebbers committed Nov 18, 2015 300 `````` Proof. by intros y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 301 ``````End discrete_cofe. `````` Robbert Krebbers committed Nov 22, 2015 302 ``````Arguments discreteC _ {_ _}. `````` Robbert Krebbers committed Nov 16, 2015 303 `````` `````` Robbert Krebbers committed Nov 22, 2015 304 ``````Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _. `````` Robbert Krebbers committed Jan 16, 2016 305 306 307 ``````Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A). Proof. by intros A x y. Qed. `````` Robbert Krebbers committed Dec 11, 2015 308 309 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 310 `````` `````` Robbert Krebbers committed Nov 16, 2015 311 312 ``````(** Later *) Inductive later (A : Type) : Type := Later { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 313 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Nov 16, 2015 314 315 ``````Arguments Later {_} _. Arguments later_car {_} _. `````` Robbert Krebbers committed Jan 18, 2016 316 317 ``````Lemma later_eta {A} (x : later A) : Later (later_car x) = x. Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 318 `````` `````` Robbert Krebbers committed Nov 16, 2015 319 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 320 321 322 `````` 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 323 `````` match n with 0 => True | S n => later_car x ={n}= later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 324 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 325 `````` {| chain_car n := later_car (c (S n)) |}. `````` Robbert Krebbers committed Jan 14, 2016 326 327 328 `````` 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 329 330 331 332 333 334 335 336 337 338 339 340 `````` 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 341 342 `````` Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. Global Instance Later_contractive : Contractive (@Later A). `````` Robbert Krebbers committed Dec 21, 2015 343 `````` Proof. by intros n ??. Qed. `````` Robbert Krebbers committed Jan 16, 2016 344 345 `````` 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 346 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 `````` 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.``````