cofe.v 15.5 KB
 Robbert Krebbers committed Feb 13, 2016 1 ``````From algebra Require Export base. `````` Robbert Krebbers committed Nov 11, 2015 2 `````` `````` Ralf Jung committed Feb 16, 2016 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````(** This files defines (a shallow embedding of) the category of COFEs: Complete ordered families of equivalences. This is a cartesian closed category, and mathematically speaking, the entire development lives in this category. However, we will generally prefer to work with raw Coq functions plus some registered Proper instances for non-expansiveness. This makes writing such functions much easier. It turns out that it many cases, we do not even need non-expansiveness. In principle, it would be possible to perform a large part of the development on OFEs, i.e., on bisected metric spaces that are not necessary complete. This is because the function space A → B has a completion if B has one - for A, the metric itself suffices. That would result in a simplification of some constructions, becuase no completion would have to be provided. However, on the other hand, we would have to introduce the notion of OFEs into our alebraic hierarchy, which we'd rather avoid. Furthermore, on paper, justifying this mix of OFEs and COFEs is a little fuzzy. *) `````` Robbert Krebbers committed Nov 11, 2015 22 23 ``````(** Unbundeled version *) Class Dist A := dist : nat → relation A. `````` Robbert Krebbers committed Nov 12, 2015 24 ``````Instance: Params (@dist) 3. `````` Ralf Jung committed Feb 10, 2016 25 26 ``````Notation "x ≡{ n }≡ y" := (dist n x y) (at level 70, n at next level, format "x ≡{ n }≡ y"). `````` Robbert Krebbers committed Feb 13, 2016 27 ``````Hint Extern 0 (_ ≡{_}≡ _) => reflexivity. `````` Ralf Jung committed Feb 10, 2016 28 ``````Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption. `````` Robbert Krebbers committed Jan 13, 2016 29 30 31 `````` Tactic Notation "cofe_subst" ident(x) := repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 32 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Jan 13, 2016 33 34 35 36 `````` | 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 37 `````` repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 38 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Dec 21, 2015 39 40 `````` | 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 41 `````` end. `````` Robbert Krebbers committed Nov 11, 2015 42 `````` `````` Ralf Jung committed Feb 11, 2016 43 ``````Tactic Notation "solve_ne" := intros; solve_proper. `````` Ralf Jung committed Feb 11, 2016 44 `````` `````` Robbert Krebbers committed Nov 11, 2015 45 46 ``````Record chain (A : Type) `{Dist A} := { chain_car :> nat → A; `````` Robbert Krebbers committed Feb 10, 2016 47 `````` chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n) `````` Robbert Krebbers committed Nov 11, 2015 48 49 50 51 52 ``````}. Arguments chain_car {_ _} _ _. Arguments chain_cauchy {_ _} _ _ _ _. Class Compl A `{Dist A} := compl : chain A → A. `````` Robbert Krebbers committed Jan 14, 2016 53 ``````Record CofeMixin A `{Equiv A, Compl A} := { `````` Ralf Jung committed Feb 10, 2016 54 `````` mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; `````` Robbert Krebbers committed Jan 14, 2016 55 `````` mixin_dist_equivalence n : Equivalence (dist n); `````` Ralf Jung committed Feb 10, 2016 56 `````` mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y; `````` Robbert Krebbers committed Feb 18, 2016 57 `````` mixin_conv_compl n c : compl c ≡{n}≡ c (S n) `````` Robbert Krebbers committed Nov 11, 2015 58 59 ``````}. Class Contractive `{Dist A, Dist B} (f : A -> B) := `````` Robbert Krebbers committed Feb 10, 2016 60 `````` contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y. `````` Robbert Krebbers committed Nov 11, 2015 61 62 63 64 `````` (** Bundeled version *) Structure cofeT := CofeT { cofe_car :> Type; `````` Robbert Krebbers committed Feb 22, 2016 65 66 67 68 `````` _ : Equiv cofe_car; _ : Dist cofe_car; _ : Compl cofe_car; _ : CofeMixin cofe_car `````` Robbert Krebbers committed Nov 11, 2015 69 ``````}. `````` Robbert Krebbers committed Jan 14, 2016 70 ``````Arguments CofeT {_ _ _ _} _. `````` Robbert Krebbers committed Nov 11, 2015 71 ``````Add Printing Constructor cofeT. `````` Robbert Krebbers committed Feb 22, 2016 72 73 74 ``````Instance cofe_equiv (A : cofeT) : Equiv A := let 'CofeT _ e _ _ _ := A in e. Instance cofe_dist (A : cofeT) : Dist A := let 'CofeT _ _ d _ _ := A in d. Instance cofe_compl (A : cofeT) : Compl A := let 'CofeT _ _ _ c _ := A in c. `````` Robbert Krebbers committed Jan 14, 2016 75 76 77 78 79 80 81 82 83 ``````Arguments cofe_car : simpl never. Arguments cofe_equiv : simpl never. Arguments cofe_dist : simpl never. Arguments cofe_compl : simpl never. (** Lifting properties from the mixin *) Section cofe_mixin. Context {A : cofeT}. Implicit Types x y : A. `````` Ralf Jung committed Feb 10, 2016 84 `````` Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y. `````` Robbert Krebbers committed Feb 22, 2016 85 `````` Proof. by destruct A as [???? []]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 86 `````` Global Instance dist_equivalence n : Equivalence (@dist A _ n). `````` Robbert Krebbers committed Feb 22, 2016 87 `````` Proof. by destruct A as [???? []]. Qed. `````` Ralf Jung committed Feb 10, 2016 88 `````` Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y. `````` Robbert Krebbers committed Feb 22, 2016 89 `````` Proof. destruct A as [???? []]; auto. Qed. `````` Robbert Krebbers committed Feb 18, 2016 90 `````` Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c (S n). `````` Robbert Krebbers committed Feb 22, 2016 91 `````` Proof. destruct A as [???? []]; auto. Qed. `````` Robbert Krebbers committed Jan 14, 2016 92 93 ``````End cofe_mixin. `````` Robbert Krebbers committed Nov 11, 2015 94 95 ``````(** General properties *) Section cofe. `````` Robbert Krebbers committed Jan 14, 2016 96 97 `````` Context {A : cofeT}. Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 98 99 100 `````` Global Instance cofe_equivalence : Equivalence ((≡) : relation A). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 101 102 `````` - by intros x; rewrite equiv_dist. - by intros x y; rewrite !equiv_dist. `````` Ralf Jung committed Feb 20, 2016 103 `````` - by intros x y z; rewrite !equiv_dist; intros; trans y. `````` Robbert Krebbers committed Nov 11, 2015 104 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 105 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 106 107 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Ralf Jung committed Feb 20, 2016 108 109 `````` - by trans x1; [|trans y1]. - by trans x2; [|trans y2]. `````` Robbert Krebbers committed Nov 11, 2015 110 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 111 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 112 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 113 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 114 115 116 `````` Qed. Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x). Proof. by apply dist_proper. Qed. `````` Robbert Krebbers committed Feb 18, 2016 117 `````` Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. `````` Robbert Krebbers committed Nov 11, 2015 118 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 119 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 120 121 `````` `{!∀ 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 122 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 123 124 125 126 `````` `{!∀ 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 127 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 128 `````` Qed. `````` Robbert Krebbers committed Feb 12, 2016 129 `````` Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y : `````` Robbert Krebbers committed Feb 10, 2016 130 131 `````` x ≡{n}≡ y → f x ≡{S n}≡ f y. Proof. eauto using contractive, dist_le with omega. Qed. `````` Robbert Krebbers committed Feb 12, 2016 132 133 134 `````` Lemma contractive_0 {B : cofeT} (f : A → B) `{!Contractive f} x y : f x ≡{0}≡ f y. Proof. eauto using contractive with omega. Qed. `````` Robbert Krebbers committed Jan 14, 2016 135 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 136 `````` Proper (dist n ==> dist n) f | 100. `````` Robbert Krebbers committed Feb 10, 2016 137 `````` Proof. by intros x y ?; apply dist_S, contractive_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 138 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 139 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Nov 11, 2015 140 141 ``````End cofe. `````` Robbert Krebbers committed Nov 22, 2015 142 143 144 145 ``````(** 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 146 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 147 `````` `````` Robbert Krebbers committed Nov 18, 2015 148 ``````(** Timeless elements *) `````` Robbert Krebbers committed Feb 10, 2016 149 ``````Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. `````` Robbert Krebbers committed Jan 14, 2016 150 ``````Arguments timeless {_} _ {_} _ _. `````` Robbert Krebbers committed Feb 18, 2016 151 ``````Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y. `````` Robbert Krebbers committed Feb 01, 2016 152 153 ``````Proof. split; intros; [by apply equiv_dist|]. `````` Robbert Krebbers committed Feb 10, 2016 154 `````` apply (timeless _), dist_le with n; auto with lia. `````` Robbert Krebbers committed Feb 01, 2016 155 ``````Qed. `````` Robbert Krebbers committed Nov 18, 2015 156 `````` `````` Robbert Krebbers committed Nov 11, 2015 157 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 158 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 159 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 160 ``````Next Obligation. `````` Robbert Krebbers committed Feb 10, 2016 161 `````` intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega. `````` Robbert Krebbers committed Feb 17, 2016 162 163 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 164 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 165 ``````Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 166 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Nov 11, 2015 167 168 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 169 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 170 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 171 `````` Proof. `````` Robbert Krebbers committed Feb 18, 2016 172 `````` apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 173 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 174 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 175 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 176 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 177 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 178 `````` intros Hfg. rewrite /fixpoint `````` Robbert Krebbers committed Feb 18, 2016 179 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 180 181 `````` induction n as [|n IH]; simpl in *; [by rewrite !Hfg|]. rewrite Hfg; apply contractive_S, IH; auto using dist_S. `````` Robbert Krebbers committed Nov 11, 2015 182 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 183 184 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 185 186 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 187 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 188 189 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 190 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 191 192 193 194 195 196 197 `````` 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 198 199 200 201 202 ``````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. `````` Ralf Jung committed Feb 10, 2016 203 `````` Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 204 205 206 207 208 209 `````` 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. `````` Robbert Krebbers committed Feb 18, 2016 210 211 `````` intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x)) (conv_compl n (fun_chain c y)) /= Hx. `````` Robbert Krebbers committed Jan 14, 2016 212 213 214 215 `````` Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 216 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 217 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 218 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 219 220 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 221 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 222 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 223 224 `````` - intros n c x; simpl. by rewrite (conv_compl n (fun_chain c x)) /=. `````` Robbert Krebbers committed Jan 14, 2016 225 226 227 228 229 230 231 232 233 234 235 236 237 `````` 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 238 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 239 240 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 241 242 243 244 245 246 247 248 249 `````` (** 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 : `````` Ralf Jung committed Feb 10, 2016 250 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 251 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 252 253 `````` (** unit *) `````` Robbert Krebbers committed Jan 14, 2016 254 255 256 257 258 259 ``````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 260 261 `````` Global Instance unit_timeless (x : ()) : Timeless x. Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 262 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 263 264 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 265 266 267 268 269 270 271 272 273 274 275 276 277 ``````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. `````` Robbert Krebbers committed Feb 17, 2016 278 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 279 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 280 281 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 282 283 `````` - intros n c; split. apply (conv_compl n (chain_map fst c)). apply (conv_compl n (chain_map snd c)). `````` Robbert Krebbers committed Jan 14, 2016 284 285 286 287 288 289 290 291 292 293 294 `````` 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 295 296 297 298 299 300 301 302 303 `````` 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 304 305 306 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Feb 10, 2016 307 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Robbert Krebbers committed Nov 16, 2015 308 `````` Instance discrete_compl : Compl A := λ c, c 1. `````` Robbert Krebbers committed Jan 14, 2016 309 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 310 311 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 312 313 314 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Robbert Krebbers committed Feb 18, 2016 315 `````` - intros n c. rewrite /compl /discrete_compl /=. `````` Robbert Krebbers committed Feb 10, 2016 316 `````` symmetry; apply (chain_cauchy c 0 (S n)); omega. `````` Robbert Krebbers committed Nov 16, 2015 317 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 318 319 `````` Definition discreteC : cofeT := CofeT discrete_cofe_mixin. Global Instance discrete_timeless (x : A) : Timeless (x : discreteC). `````` Robbert Krebbers committed Nov 18, 2015 320 `````` Proof. by intros y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 321 ``````End discrete_cofe. `````` Robbert Krebbers committed Nov 22, 2015 322 ``````Arguments discreteC _ {_ _}. `````` Robbert Krebbers committed Nov 16, 2015 323 `````` `````` Robbert Krebbers committed Nov 22, 2015 324 ``````Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _. `````` Robbert Krebbers committed Jan 16, 2016 325 326 327 ``````Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A). Proof. by intros A x y. Qed. `````` Robbert Krebbers committed Dec 11, 2015 328 329 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 330 `````` `````` Robbert Krebbers committed Nov 16, 2015 331 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 332 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 333 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 334 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 335 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Feb 10, 2016 336 ``````Lemma later_eta {A} (x : later A) : Next (later_car x) = x. `````` Robbert Krebbers committed Jan 18, 2016 337 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 338 `````` `````` Robbert Krebbers committed Nov 16, 2015 339 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 340 341 342 `````` 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, `````` Ralf Jung committed Feb 10, 2016 343 `````` match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 344 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 345 `````` {| chain_car n := later_car (c (S n)) |}. `````` Robbert Krebbers committed Jan 14, 2016 346 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. `````` Robbert Krebbers committed Feb 10, 2016 347 `````` Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)). `````` Robbert Krebbers committed Jan 14, 2016 348 `````` Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 349 350 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 351 `````` - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. `````` Robbert Krebbers committed Nov 16, 2015 352 `````` split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). `````` Robbert Krebbers committed Feb 17, 2016 353 `````` - intros [|n]; [by split|split]; unfold dist, later_dist. `````` Robbert Krebbers committed Nov 16, 2015 354 355 `````` + by intros [x]. + by intros [x] [y]. `````` Ralf Jung committed Feb 20, 2016 356 `````` + by intros [x] [y] [z] ??; trans y. `````` Robbert Krebbers committed Feb 17, 2016 357 `````` - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 358 `````` - intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. `````` Robbert Krebbers committed Nov 16, 2015 359 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 360 `````` Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. `````` Robbert Krebbers committed Feb 10, 2016 361 362 `````` Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. `````` Robbert Krebbers committed Feb 11, 2016 363 `````` Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). `````` Robbert Krebbers committed Jan 16, 2016 364 `````` Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 365 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 366 367 368 369 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := `````` Robbert Krebbers committed Feb 10, 2016 370 `````` Next (f (later_car x)). `````` Robbert Krebbers committed Jan 14, 2016 371 372 373 374 375 376 377 378 379 380 381 382 ``````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). `````` Robbert Krebbers committed Feb 10, 2016 383 ``Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.``