cofe.v 14.4 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. `````` Ralf Jung committed Feb 10, 2016 6 7 8 9 ``````Notation "x ≡{ n }≡ y" := (dist n x y) (at level 70, n at next level, format "x ≡{ n }≡ y"). Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity. 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 `````` `````` Ralf Jung committed Feb 11, 2016 24 ``````Tactic Notation "solve_ne" := intros; solve_proper. `````` Ralf Jung committed Feb 11, 2016 25 `````` `````` Robbert Krebbers committed Nov 11, 2015 26 27 ``````Record chain (A : Type) `{Dist A} := { chain_car :> nat → A; `````` Robbert Krebbers committed Feb 10, 2016 28 `````` chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n) `````` Robbert Krebbers committed Nov 11, 2015 29 30 31 32 33 ``````}. Arguments chain_car {_ _} _ _. Arguments chain_cauchy {_ _} _ _ _ _. Class Compl A `{Dist A} := compl : chain A → A. `````` Robbert Krebbers committed Jan 14, 2016 34 ``````Record CofeMixin A `{Equiv A, Compl A} := { `````` Ralf Jung committed Feb 10, 2016 35 `````` mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; `````` Robbert Krebbers committed Jan 14, 2016 36 `````` mixin_dist_equivalence n : Equivalence (dist n); `````` Ralf Jung committed Feb 10, 2016 37 `````` mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y; `````` Robbert Krebbers committed Feb 10, 2016 38 `````` mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n) `````` Robbert Krebbers committed Nov 11, 2015 39 40 ``````}. Class Contractive `{Dist A, Dist B} (f : A -> B) := `````` Robbert Krebbers committed Feb 10, 2016 41 `````` contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y. `````` Robbert Krebbers committed Nov 11, 2015 42 43 44 45 46 47 48 `````` (** 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 49 `````` cofe_mixin : CofeMixin cofe_car `````` Robbert Krebbers committed Nov 11, 2015 50 ``````}. `````` Robbert Krebbers committed Jan 14, 2016 51 ``````Arguments CofeT {_ _ _ _} _. `````` Robbert Krebbers committed Nov 11, 2015 52 ``````Add Printing Constructor cofeT. `````` Robbert Krebbers committed Jan 14, 2016 53 54 55 56 57 58 59 60 61 62 63 ``````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 64 `````` Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 65 66 67 `````` 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 68 `````` Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 69 `````` Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed. `````` Robbert Krebbers committed Feb 10, 2016 70 `````` Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n). `````` Robbert Krebbers committed Jan 14, 2016 71 72 73 `````` Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed. End cofe_mixin. `````` Robbert Krebbers committed Nov 11, 2015 74 75 ``````(** General properties *) Section cofe. `````` Robbert Krebbers committed Jan 14, 2016 76 77 `````` Context {A : cofeT}. Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 78 79 80 81 82 83 84 `````` 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 85 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 86 87 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Robbert Krebbers committed Dec 15, 2015 88 89 `````` * by transitivity x1; [|transitivity y1]. * by transitivity x2; [|transitivity y2]. `````` Robbert Krebbers committed Nov 11, 2015 90 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 91 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 92 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 93 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 94 95 96 `````` Qed. Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x). Proof. by apply dist_proper. Qed. `````` Ralf Jung committed Feb 10, 2016 97 `````` Lemma dist_le (x y : A) n n' : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. `````` Robbert Krebbers committed Nov 11, 2015 98 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 99 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 100 101 `````` `{!∀ 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 102 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 103 104 105 106 `````` `{!∀ 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 107 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 108 `````` Qed. `````` Robbert Krebbers committed Feb 12, 2016 109 `````` Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y : `````` Robbert Krebbers committed Feb 10, 2016 110 111 `````` x ≡{n}≡ y → f x ≡{S n}≡ f y. Proof. eauto using contractive, dist_le with omega. Qed. `````` Robbert Krebbers committed Feb 12, 2016 112 113 114 `````` 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 115 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 116 `````` Proper (dist n ==> dist n) f | 100. `````` Robbert Krebbers committed Feb 10, 2016 117 `````` Proof. by intros x y ?; apply dist_S, contractive_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 118 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 119 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Nov 11, 2015 120 121 ``````End cofe. `````` Robbert Krebbers committed Nov 22, 2015 122 123 124 125 ``````(** 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 126 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 127 `````` `````` Robbert Krebbers committed Nov 18, 2015 128 ``````(** Timeless elements *) `````` Robbert Krebbers committed Feb 10, 2016 129 ``````Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. `````` Robbert Krebbers committed Jan 14, 2016 130 ``````Arguments timeless {_} _ {_} _ _. `````` Robbert Krebbers committed Feb 10, 2016 131 ``````Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{n}≡ y. `````` Robbert Krebbers committed Feb 01, 2016 132 133 ``````Proof. split; intros; [by apply equiv_dist|]. `````` Robbert Krebbers committed Feb 10, 2016 134 `````` apply (timeless _), dist_le with n; auto with lia. `````` Robbert Krebbers committed Feb 01, 2016 135 ``````Qed. `````` Robbert Krebbers committed Nov 18, 2015 136 `````` `````` Robbert Krebbers committed Nov 11, 2015 137 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 138 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 139 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 140 ``````Next Obligation. `````` Robbert Krebbers committed Feb 10, 2016 141 `````` intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega. `````` Robbert Krebbers committed Feb 12, 2016 142 143 `````` * apply (contractive_0 f). * apply (contractive_S f), IH; auto with omega. `````` 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 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 152 `````` apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //. `````` Robbert Krebbers committed Feb 12, 2016 153 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 154 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 155 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 156 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 157 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 158 159 160 161 `````` intros Hfg. rewrite /fixpoint (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=. 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 162 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 163 164 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 165 166 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 167 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 168 169 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 170 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 171 172 173 174 175 176 177 `````` 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 178 179 180 181 182 ``````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 183 `````` Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 184 185 186 187 188 189 `````` 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 10, 2016 190 191 `````` intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx. `````` Robbert Krebbers committed Jan 14, 2016 192 193 194 195 `````` Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 02, 2016 196 197 `````` * 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 198 199 200 201 202 203 `````` * 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. * intros c n x; simpl. `````` Robbert Krebbers committed Feb 10, 2016 204 `````` by rewrite (conv_compl (fun_chain c x) n) /=. `````` Robbert Krebbers committed Jan 14, 2016 205 206 207 208 209 210 211 212 213 214 215 216 217 `````` 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 218 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 219 220 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 221 222 223 224 225 226 227 228 229 `````` (** 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 230 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 231 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 232 233 `````` (** unit *) `````` Robbert Krebbers committed Jan 14, 2016 234 235 236 237 238 239 ``````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 240 241 `````` Global Instance unit_timeless (x : ()) : Timeless x. Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 242 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 243 244 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 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 274 ``````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. * 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 275 276 277 278 279 280 281 282 283 `````` 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 284 285 286 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Feb 10, 2016 287 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Robbert Krebbers committed Nov 16, 2015 288 `````` 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 `````` Proof. split. `````` Robbert Krebbers committed Feb 10, 2016 292 293 `````` * intros x y; split; [done|intros Hn; apply (Hn 0)]. * done. `````` Robbert Krebbers committed Nov 16, 2015 294 `````` * done. `````` Robbert Krebbers committed Feb 10, 2016 295 296 `````` * intros c n. rewrite /compl /discrete_compl /=. symmetry; apply (chain_cauchy c 0 (S n)); omega. `````` Robbert Krebbers committed Nov 16, 2015 297 `````` 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 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 312 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 313 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 314 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 315 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Feb 10, 2016 316 ``````Lemma later_eta {A} (x : later A) : Next (later_car x) = x. `````` Robbert Krebbers committed Jan 18, 2016 317 ``````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, `````` Ralf Jung committed Feb 10, 2016 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 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. `````` Robbert Krebbers committed Feb 10, 2016 327 `````` Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)). `````` Robbert Krebbers committed Jan 14, 2016 328 `````` Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 329 330 331 332 333 334 335 336 337 338 339 `````` 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. * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 340 `````` Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. `````` Robbert Krebbers committed Feb 10, 2016 341 342 `````` Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. `````` Robbert Krebbers committed Feb 11, 2016 343 `````` Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). `````` Robbert Krebbers committed Jan 16, 2016 344 `````` Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 345 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 346 347 348 349 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := `````` Robbert Krebbers committed Feb 10, 2016 350 `````` Next (f (later_car x)). `````` Robbert Krebbers committed Jan 14, 2016 351 352 353 354 355 356 357 358 359 360 361 362 ``````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 363 ``Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.``