cofe.v 15.6 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 43 44 `````` Record chain (A : Type) `{Dist A} := { chain_car :> nat → A; `````` Robbert Krebbers committed Feb 10, 2016 45 `````` chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n) `````` Robbert Krebbers committed Nov 11, 2015 46 47 48 49 50 ``````}. Arguments chain_car {_ _} _ _. Arguments chain_cauchy {_ _} _ _ _ _. Class Compl A `{Dist A} := compl : chain A → A. `````` Robbert Krebbers committed Jan 14, 2016 51 ``````Record CofeMixin A `{Equiv A, Compl A} := { `````` Ralf Jung committed Feb 10, 2016 52 `````` mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; `````` Robbert Krebbers committed Jan 14, 2016 53 `````` mixin_dist_equivalence n : Equivalence (dist n); `````` Ralf Jung committed Feb 10, 2016 54 `````` mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y; `````` Robbert Krebbers committed Feb 18, 2016 55 `````` mixin_conv_compl n c : compl c ≡{n}≡ c (S n) `````` Robbert Krebbers committed Nov 11, 2015 56 ``````}. `````` Robbert Krebbers committed Feb 27, 2016 57 ``````Class Contractive `{Dist A, Dist B} (f : A → B) := `````` Robbert Krebbers committed Feb 10, 2016 58 `````` contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y. `````` Robbert Krebbers committed Nov 11, 2015 59 60 61 62 63 64 65 `````` (** 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 66 `````` cofe_mixin : CofeMixin cofe_car `````` Robbert Krebbers committed Nov 11, 2015 67 ``````}. `````` Robbert Krebbers committed Jan 14, 2016 68 ``````Arguments CofeT {_ _ _ _} _. `````` Robbert Krebbers committed Nov 11, 2015 69 ``````Add Printing Constructor cofeT. `````` Robbert Krebbers committed Jan 14, 2016 70 71 72 73 74 75 76 77 78 79 80 ``````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. `````` Ralf Jung committed Feb 10, 2016 81 `````` Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 82 83 84 `````` 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. `````` Ralf Jung committed Feb 10, 2016 85 `````` Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 86 `````` Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed. `````` Robbert Krebbers committed Feb 18, 2016 87 `````` Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c (S n). `````` Robbert Krebbers committed Jan 14, 2016 88 89 90 `````` Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed. End cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 91 92 93 94 95 ``````(** Discrete COFEs and Timeless elements *) Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_} _ {_} _ _. Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x. `````` Robbert Krebbers committed Nov 11, 2015 96 97 ``````(** General properties *) Section cofe. `````` Robbert Krebbers committed Jan 14, 2016 98 99 `````` Context {A : cofeT}. Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 100 101 102 `````` Global Instance cofe_equivalence : Equivalence ((≡) : relation A). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 103 104 `````` - by intros x; rewrite equiv_dist. - by intros x y; rewrite !equiv_dist. `````` Ralf Jung committed Feb 20, 2016 105 `````` - by intros x y z; rewrite !equiv_dist; intros; trans y. `````` Robbert Krebbers committed Nov 11, 2015 106 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 107 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 108 109 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Ralf Jung committed Feb 20, 2016 110 111 `````` - by trans x1; [|trans y1]. - by trans x2; [|trans y2]. `````` Robbert Krebbers committed Nov 11, 2015 112 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 113 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 114 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 115 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 116 117 118 `````` 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 119 `````` Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. `````` Robbert Krebbers committed Nov 11, 2015 120 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 121 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 122 123 `````` `{!∀ 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 124 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 125 126 127 128 `````` `{!∀ 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 129 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 130 `````` Qed. `````` Robbert Krebbers committed Feb 12, 2016 131 `````` Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y : `````` Robbert Krebbers committed Feb 10, 2016 132 133 `````` x ≡{n}≡ y → f x ≡{S n}≡ f y. Proof. eauto using contractive, dist_le with omega. Qed. `````` Robbert Krebbers committed Feb 12, 2016 134 135 136 `````` 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 137 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 138 `````` Proper (dist n ==> dist n) f | 100. `````` Robbert Krebbers committed Feb 10, 2016 139 `````` Proof. by intros x y ?; apply dist_S, contractive_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 140 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 141 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Feb 24, 2016 142 143 144 145 146 147 `````` Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y. Proof. split; intros; [by apply equiv_dist|]. apply (timeless _), dist_le with n; auto with lia. Qed. `````` Robbert Krebbers committed Nov 11, 2015 148 149 ``````End cofe. `````` Robbert Krebbers committed Nov 22, 2015 150 151 152 153 ``````(** 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 154 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 155 `````` `````` Robbert Krebbers committed Nov 11, 2015 156 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 157 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 158 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 159 ``````Next Obligation. `````` Robbert Krebbers committed Feb 10, 2016 160 `````` intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega. `````` Robbert Krebbers committed Feb 17, 2016 161 162 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 163 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 164 ``````Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 165 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Nov 11, 2015 166 167 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 168 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 169 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 170 `````` Proof. `````` Robbert Krebbers committed Feb 18, 2016 171 `````` apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 172 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 173 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 174 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 175 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 176 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 177 `````` intros Hfg. rewrite /fixpoint `````` Robbert Krebbers committed Feb 18, 2016 178 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 179 180 `````` 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 181 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 182 183 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 184 185 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 186 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 187 188 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 189 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 190 191 192 193 194 195 196 `````` 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 197 198 199 200 201 ``````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 202 `````` Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 203 204 205 206 207 208 `````` 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 209 210 `````` 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 211 212 213 214 `````` Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 215 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 216 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 217 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 218 219 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 220 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 221 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 222 223 `````` - intros n c x; simpl. by rewrite (conv_compl n (fun_chain c x)) /=. `````` Robbert Krebbers committed Jan 14, 2016 224 225 226 227 228 229 230 231 232 233 234 235 236 `````` 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 237 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 238 239 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 240 241 242 243 244 245 246 247 248 `````` (** 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 249 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 250 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 251 252 `````` (** unit *) `````` Robbert Krebbers committed Jan 14, 2016 253 254 255 256 257 258 ``````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 Feb 24, 2016 259 `````` Global Instance unit_discrete_cofe : Discrete unitC. `````` Robbert Krebbers committed Jan 31, 2016 260 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 261 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 262 263 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 264 265 266 267 268 269 270 271 272 273 274 275 276 ``````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 277 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 278 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 279 280 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 281 282 `````` - 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 283 284 285 286 287 `````` 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. `````` Robbert Krebbers committed Feb 24, 2016 288 289 `````` Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC. Proof. intros ?? [??]; apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 290 291 292 293 294 295 ``````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 296 297 298 299 300 301 302 303 304 `````` 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 305 306 307 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Feb 10, 2016 308 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Robbert Krebbers committed Nov 16, 2015 309 `````` Instance discrete_compl : Compl A := λ c, c 1. `````` Robbert Krebbers committed Jan 14, 2016 310 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 311 312 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 313 314 315 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Robbert Krebbers committed Feb 18, 2016 316 `````` - intros n c. rewrite /compl /discrete_compl /=. `````` Robbert Krebbers committed Feb 10, 2016 317 `````` symmetry; apply (chain_cauchy c 0 (S n)); omega. `````` Robbert Krebbers committed Nov 16, 2015 318 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 319 `````` Definition discreteC : cofeT := CofeT discrete_cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 320 321 `````` Global Instance discrete_discrete_cofe : Discrete discreteC. Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 322 ``````End discrete_cofe. `````` Robbert Krebbers committed Nov 22, 2015 323 ``````Arguments discreteC _ {_ _}. `````` Robbert Krebbers committed Nov 16, 2015 324 `````` `````` Robbert Krebbers committed Nov 22, 2015 325 ``````Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _. `````` Robbert Krebbers committed Jan 16, 2016 326 327 328 ``````Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A). Proof. by intros A x y. Qed. `````` Robbert Krebbers committed Dec 11, 2015 329 330 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 331 `````` `````` Robbert Krebbers committed Nov 16, 2015 332 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 333 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 334 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 335 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 336 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Feb 10, 2016 337 ``````Lemma later_eta {A} (x : later A) : Next (later_car x) = x. `````` Robbert Krebbers committed Jan 18, 2016 338 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 339 `````` `````` Robbert Krebbers committed Nov 16, 2015 340 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 341 342 343 `````` 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 344 `````` match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 345 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 346 `````` {| chain_car n := later_car (c (S n)) |}. `````` Robbert Krebbers committed Jan 14, 2016 347 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. `````` Robbert Krebbers committed Feb 10, 2016 348 `````` Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)). `````` Robbert Krebbers committed Jan 14, 2016 349 `````` Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 350 351 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 352 `````` - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. `````` Robbert Krebbers committed Nov 16, 2015 353 `````` split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). `````` Robbert Krebbers committed Feb 17, 2016 354 `````` - intros [|n]; [by split|split]; unfold dist, later_dist. `````` Robbert Krebbers committed Nov 16, 2015 355 356 `````` + by intros [x]. + by intros [x] [y]. `````` Ralf Jung committed Feb 20, 2016 357 `````` + by intros [x] [y] [z] ??; trans y. `````` Robbert Krebbers committed Feb 17, 2016 358 `````` - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 359 `````` - intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. `````` Robbert Krebbers committed Nov 16, 2015 360 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 361 `````` Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. `````` Robbert Krebbers committed Feb 10, 2016 362 363 `````` Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. `````` Robbert Krebbers committed Feb 11, 2016 364 `````` Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). `````` Robbert Krebbers committed Jan 16, 2016 365 `````` Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 366 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 367 368 369 370 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := `````` Robbert Krebbers committed Feb 10, 2016 371 `````` Next (f (later_car x)). `````` Robbert Krebbers committed Jan 14, 2016 372 373 374 375 376 377 378 379 380 381 382 383 ``````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 384 ``Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.``