cofe.v 29.1 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.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; `````` Ralf Jung committed Feb 29, 2016 45 `````` chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car 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; `````` Ralf Jung committed Feb 29, 2016 55 `````` mixin_conv_compl n c : compl c ≡{n}≡ c 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 `````` (** Bundeled version *) `````` Robbert Krebbers committed Jun 15, 2016 61 ``````Structure cofeT := CofeT' { `````` Robbert Krebbers committed Nov 11, 2015 62 63 64 65 `````` cofe_car :> Type; cofe_equiv : Equiv cofe_car; cofe_dist : Dist cofe_car; cofe_compl : Compl cofe_car; `````` Robbert Krebbers committed Jun 15, 2016 66 67 `````` cofe_mixin : CofeMixin cofe_car; cofe_car' : Type `````` Robbert Krebbers committed Nov 11, 2015 68 ``````}. `````` Robbert Krebbers committed Jun 15, 2016 69 70 ``````Arguments CofeT' _ {_ _ _} _ _. Notation CofeT A m := (CofeT' A m A). `````` Robbert Krebbers committed Nov 11, 2015 71 ``````Add Printing Constructor cofeT. `````` Robbert Krebbers committed Jun 14, 2016 72 73 74 ``````Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances. Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances. Hint Extern 0 (Compl _) => eapply (@cofe_compl _) : typeclass_instances. `````` Robbert Krebbers committed Jan 14, 2016 75 76 77 78 79 80 81 82 83 84 ``````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 85 `````` Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 86 87 88 `````` 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 89 `````` Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y. `````` Robbert Krebbers committed Jan 14, 2016 90 `````` Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed. `````` Ralf Jung committed Feb 29, 2016 91 `````` Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c n. `````` Robbert Krebbers committed Jan 14, 2016 92 93 94 `````` Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed. End cofe_mixin. `````` Robbert Krebbers committed May 28, 2016 95 96 ``````Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption. `````` Robbert Krebbers committed Feb 24, 2016 97 ``````(** Discrete COFEs and Timeless elements *) `````` Ralf Jung committed Mar 15, 2016 98 ``````(* TODO: On paper, We called these "discrete elements". I think that makes `````` Ralf Jung committed Mar 07, 2016 99 `````` more sense. *) `````` Robbert Krebbers committed May 27, 2016 100 101 ``````Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_ _ _} _ {_} _ _. `````` Robbert Krebbers committed Feb 24, 2016 102 103 ``````Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x. `````` Robbert Krebbers committed Nov 11, 2015 104 105 ``````(** General properties *) Section cofe. `````` Robbert Krebbers committed Jan 14, 2016 106 107 `````` Context {A : cofeT}. Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 108 109 110 `````` Global Instance cofe_equivalence : Equivalence ((≡) : relation A). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 111 112 `````` - by intros x; rewrite equiv_dist. - by intros x y; rewrite !equiv_dist. `````` Ralf Jung committed Feb 20, 2016 113 `````` - by intros x y z; rewrite !equiv_dist; intros; trans y. `````` Robbert Krebbers committed Nov 11, 2015 114 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 115 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 116 117 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Ralf Jung committed Feb 20, 2016 118 119 `````` - by trans x1; [|trans y1]. - by trans x2; [|trans y2]. `````` Robbert Krebbers committed Nov 11, 2015 120 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 121 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 122 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 123 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 124 125 126 `````` 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 127 `````` Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. `````` Robbert Krebbers committed Nov 11, 2015 128 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Ralf Jung committed Feb 29, 2016 129 130 `````` Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y. Proof. intros; eauto using dist_le. Qed. `````` Robbert Krebbers committed Jan 14, 2016 131 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 132 133 `````` `{!∀ 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 134 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 135 136 137 138 `````` `{!∀ 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 139 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 140 `````` Qed. `````` Robbert Krebbers committed Feb 12, 2016 141 `````` Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y : `````` Robbert Krebbers committed Feb 10, 2016 142 143 `````` x ≡{n}≡ y → f x ≡{S n}≡ f y. Proof. eauto using contractive, dist_le with omega. Qed. `````` Robbert Krebbers committed Feb 12, 2016 144 145 146 `````` 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 147 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 148 `````` Proper (dist n ==> dist n) f | 100. `````` Robbert Krebbers committed Feb 10, 2016 149 `````` Proof. by intros x y ?; apply dist_S, contractive_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 150 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 151 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Feb 24, 2016 152 `````` `````` Ralf Jung committed Feb 29, 2016 153 154 155 156 157 `````` Lemma conv_compl' n (c : chain A) : compl c ≡{n}≡ c (S n). Proof. transitivity (c n); first by apply conv_compl. symmetry. apply chain_cauchy. omega. Qed. `````` Robbert Krebbers committed Feb 24, 2016 158 159 `````` Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y. Proof. `````` Robbert Krebbers committed May 28, 2016 160 `````` split; intros; auto. apply (timeless _), dist_le with n; auto with lia. `````` Robbert Krebbers committed Feb 24, 2016 161 `````` Qed. `````` Robbert Krebbers committed Nov 11, 2015 162 163 ``````End cofe. `````` Robbert Krebbers committed Mar 06, 2016 164 165 166 ``````Instance const_contractive {A B : cofeT} (x : A) : Contractive (@const A B x). Proof. by intros n y1 y2. Qed. `````` Robbert Krebbers committed Nov 22, 2015 167 168 169 170 ``````(** 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 171 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 172 `````` `````` Robbert Krebbers committed Nov 11, 2015 173 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 174 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 175 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 176 ``````Next Obligation. `````` Robbert Krebbers committed Mar 06, 2016 177 178 `````` intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega. `````` Robbert Krebbers committed Feb 17, 2016 179 180 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 181 ``````Qed. `````` Robbert Krebbers committed Mar 18, 2016 182 183 `````` Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 184 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Mar 18, 2016 185 186 187 ``````Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed. Definition fixpoint {A AiH} f {Hf} := proj1_sig fixpoint_aux A AiH f Hf. Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux. `````` Robbert Krebbers committed Nov 11, 2015 188 189 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 190 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 191 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 192 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 193 194 `````` apply equiv_dist=>n. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 195 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 196 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 197 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 198 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 199 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 200 `````` intros Hfg. rewrite fixpoint_eq /fixpoint_def `````` Robbert Krebbers committed Feb 18, 2016 201 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 202 203 `````` 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 204 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 205 206 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 207 208 209 210 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 211 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 212 213 214 215 216 217 218 `````` 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 219 220 221 222 223 ``````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 224 `````` Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 225 226 227 228 229 230 `````` 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 231 232 `````` 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 233 234 235 236 `````` Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 237 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 238 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 239 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 240 241 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 242 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 243 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 244 245 `````` - intros n c x; simpl. by rewrite (conv_compl n (fun_chain c x)) /=. `````` Robbert Krebbers committed Jan 14, 2016 246 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 247 `````` Canonical Structure cofe_mor : cofeT := CofeT (cofeMor A B) cofe_mor_cofe_mixin. `````` Robbert Krebbers committed Jan 14, 2016 248 249 250 251 252 253 254 255 256 257 258 `````` 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 259 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 260 261 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 262 `````` `````` Ralf Jung committed Mar 17, 2016 263 ``````(** Identity and composition and constant function *) `````` Robbert Krebbers committed Nov 11, 2015 264 265 ``````Definition cid {A} : A -n> A := CofeMor id. Instance: Params (@cid) 1. `````` Ralf Jung committed Mar 17, 2016 266 267 ``````Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x). Instance: Params (@cconst) 2. `````` Robbert Krebbers committed Mar 02, 2016 268 `````` `````` Robbert Krebbers committed Nov 11, 2015 269 270 271 272 273 ``````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 274 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 275 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 276 `````` `````` Ralf Jung committed Mar 02, 2016 277 ``````(* Function space maps *) `````` Robbert Krebbers committed Mar 02, 2016 278 ``````Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') `````` Ralf Jung committed Mar 02, 2016 279 `````` (h : A -n> B) : A' -n> B' := g ◎ h ◎ f. `````` Robbert Krebbers committed Mar 02, 2016 280 ``````Instance cofe_mor_map_ne {A A' B B'} n : `````` Ralf Jung committed Mar 02, 2016 281 `````` Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B'). `````` Robbert Krebbers committed Mar 02, 2016 282 ``````Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed. `````` Ralf Jung committed Mar 02, 2016 283 `````` `````` Robbert Krebbers committed Mar 02, 2016 284 ``````Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') : `````` Ralf Jung committed Mar 02, 2016 285 `````` (A -n> B) -n> (A' -n> B') := CofeMor (cofe_mor_map f g). `````` Robbert Krebbers committed Mar 02, 2016 286 ``````Instance cofe_morC_map_ne {A A' B B'} n : `````` Ralf Jung committed Mar 02, 2016 287 288 289 `````` Proper (dist n ==> dist n ==> dist n) (@cofe_morC_map A A' B B'). Proof. intros f f' Hf g g' Hg ?. rewrite /= /cofe_mor_map. `````` Robbert Krebbers committed Mar 02, 2016 290 `````` by repeat apply ccompose_ne. `````` Ralf Jung committed Mar 02, 2016 291 292 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 293 ``````(** unit *) `````` Robbert Krebbers committed Jan 14, 2016 294 295 296 297 298 ``````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. `````` Robbert Krebbers committed May 25, 2016 299 `````` Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 300 `````` Global Instance unit_discrete_cofe : Discrete unitC. `````` Robbert Krebbers committed Jan 31, 2016 301 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 302 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 303 304 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 305 306 307 308 309 310 311 312 313 314 315 316 317 ``````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 318 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 319 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 320 321 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 322 323 `````` - 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 324 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 325 `````` Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin. `````` Robbert Krebbers committed Jan 14, 2016 326 327 328 `````` 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 329 330 `````` Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC. Proof. intros ?? [??]; apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 331 332 333 334 335 336 ``````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 337 338 339 340 341 342 343 344 345 `````` 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 Mar 02, 2016 346 347 ``````(** Functors *) Structure cFunctor := CFunctor { `````` Robbert Krebbers committed May 27, 2016 348 `````` cFunctor_car : cofeT → cofeT → cofeT; `````` Robbert Krebbers committed Mar 02, 2016 349 350 `````` cFunctor_map {A1 A2 B1 B2} : ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2; `````` Robbert Krebbers committed Mar 07, 2016 351 352 `````` cFunctor_ne {A1 A2 B1 B2} n : Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2); `````` Robbert Krebbers committed Mar 02, 2016 353 354 355 356 357 358 `````` cFunctor_id {A B : cofeT} (x : cFunctor_car A B) : cFunctor_map (cid,cid) x ≡ x; cFunctor_compose {A1 A2 A3 B1 B2 B3} (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x : cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x) }. `````` Robbert Krebbers committed Mar 07, 2016 359 ``````Existing Instance cFunctor_ne. `````` Robbert Krebbers committed Mar 02, 2016 360 361 ``````Instance: Params (@cFunctor_map) 5. `````` Ralf Jung committed Mar 07, 2016 362 363 364 ``````Delimit Scope cFunctor_scope with CF. Bind Scope cFunctor_scope with cFunctor. `````` Ralf Jung committed Mar 07, 2016 365 366 367 ``````Class cFunctorContractive (F : cFunctor) := cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). `````` Robbert Krebbers committed Mar 02, 2016 368 369 370 371 372 373 374 ``````Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A. Coercion cFunctor_diag : cFunctor >-> Funclass. Program Definition constCF (B : cofeT) : cFunctor := {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}. Solve Obligations with done. `````` Ralf Jung committed Mar 07, 2016 375 ``````Instance constCF_contractive B : cFunctorContractive (constCF B). `````` Robbert Krebbers committed Mar 07, 2016 376 ``````Proof. rewrite /cFunctorContractive; apply _. Qed. `````` Ralf Jung committed Mar 07, 2016 377 378 379 380 381 `````` Program Definition idCF : cFunctor := {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}. Solve Obligations with done. `````` Robbert Krebbers committed Mar 02, 2016 382 383 384 385 386 ``````Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {| cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B); cFunctor_map A1 A2 B1 B2 fg := prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg) |}. `````` Robbert Krebbers committed Mar 07, 2016 387 388 389 ``````Next Obligation. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 390 391 392 393 394 395 ``````Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed. Next Obligation. intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl. by rewrite !cFunctor_compose. Qed. `````` Ralf Jung committed Mar 07, 2016 396 397 398 399 400 401 402 403 ``````Instance prodCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (prodCF F1 F2). Proof. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_contractive. Qed. `````` Ralf Jung committed Mar 02, 2016 404 405 406 407 408 ``````Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {| cFunctor_car A B := cofe_mor (cFunctor_car F1 B A) (cFunctor_car F2 A B); cFunctor_map A1 A2 B1 B2 fg := cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg) |}. `````` Robbert Krebbers committed Mar 07, 2016 409 410 411 412 ``````Next Obligation. intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. apply cofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg. Qed. `````` Ralf Jung committed Mar 02, 2016 413 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 414 415 `````` intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id. apply (ne_proper f). apply cFunctor_id. `````` Ralf Jung committed Mar 02, 2016 416 417 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 418 419 `````` intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *. rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose. `````` Ralf Jung committed Mar 02, 2016 420 421 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 422 423 424 425 426 427 428 429 ``````Instance cofe_morCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (cofe_morCF F1 F2). Proof. intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg. Qed. `````` Robbert Krebbers committed May 27, 2016 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 ``````(** Sum *) Section sum. Context {A B : cofeT}. Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n). Global Instance inl_ne : Proper (dist n ==> dist n) (@inl A B) := _. Global Instance inr_ne : Proper (dist n ==> dist n) (@inr A B) := _. Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _. Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _. Program Definition inl_chain (c : chain (A + B)) (a : A) : chain A := {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}. Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Program Definition inr_chain (c : chain (A + B)) (b : B) : chain B := {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}. Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Instance sum_compl : Compl (A + B) := λ c, match c 0 with | inl a => inl (compl (inl_chain c a)) | inr b => inr (compl (inr_chain c b)) end. Definition sum_cofe_mixin : CofeMixin (A + B). Proof. split. - intros x y; split=> Hx. + destruct Hx=> n; constructor; by apply equiv_dist. + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _). - apply _. - destruct 1; constructor; by apply dist_S. - intros n c; rewrite /compl /sum_compl. feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. + rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver. + rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver. Qed. Canonical Structure sumC : cofeT := CofeT (A + B) sum_cofe_mixin. Global Instance inl_timeless (x : A) : Timeless x → Timeless (inl x). Proof. inversion_clear 2; constructor; by apply (timeless _). Qed. Global Instance inr_timeless (y : B) : Timeless y → Timeless (inr y). Proof. inversion_clear 2; constructor; by apply (timeless _). Qed. Global Instance sum_discrete_cofe : Discrete A → Discrete B → Discrete sumC. Proof. intros ?? [?|?]; apply _. Qed. End sum. Arguments sumC : clear implicits. Typeclasses Opaque sum_dist. Instance sum_map_ne {A A' B B' : cofeT} n : Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n) (@sum_map A A' B B'). Proof. intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg]. Qed. Definition sumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') : sumC A B -n> sumC A' B' := CofeMor (sum_map f g). Instance sumC_map_ne {A A' B B'} n : Proper (dist n ==> dist n ==> dist n) (@sumC_map A A' B B'). Proof. intros f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed. Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {| cFunctor_car A B := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B); cFunctor_map A1 A2 B1 B2 fg := sumC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg) |}. Next Obligation. intros ?? A1 A2 B1 B2 n ???; by apply sumC_map_ne; apply cFunctor_ne. Qed. Next Obligation. by intros F1 F2 A B [?|?]; rewrite /= !cFunctor_id. Qed. Next Obligation. intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [?|?]; simpl; by rewrite !cFunctor_compose. Qed. Instance sumCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (sumCF F1 F2). Proof. intros ?? A1 A2 B1 B2 n ???; by apply sumC_map_ne; apply cFunctor_contractive. Qed. `````` Robbert Krebbers committed Nov 16, 2015 513 514 515 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Feb 10, 2016 516 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Ralf Jung committed Feb 29, 2016 517 `````` Instance discrete_compl : Compl A := λ c, c 0. `````` Robbert Krebbers committed Jan 14, 2016 518 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 519 520 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 521 522 523 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Ralf Jung committed Feb 29, 2016 524 525 `````` - intros n c. rewrite /compl /discrete_compl /=; symmetry; apply (chain_cauchy c 0 n). omega. `````` Robbert Krebbers committed Nov 16, 2015 526 527 528 `````` Qed. End discrete_cofe. `````` Robbert Krebbers committed May 25, 2016 529 530 531 532 533 534 535 536 ``````Notation discreteC A := (CofeT A discrete_cofe_mixin). Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)). Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} : Discrete (discreteC A). Proof. by intros x y. Qed. Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A). Proof. by intros x y. Qed. `````` Robbert Krebbers committed Jan 16, 2016 537 `````` `````` Robbert Krebbers committed Dec 11, 2015 538 539 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 540 `````` `````` Robbert Krebbers committed May 25, 2016 541 542 543 544 ``````(* Option *) Section option. Context {A : cofeT}. `````` Robbert Krebbers committed May 27, 2016 545 `````` Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n). `````` Robbert Krebbers committed May 25, 2016 546 `````` Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my. `````` Robbert Krebbers committed May 27, 2016 547 `````` Proof. done. Qed. `````` Robbert Krebbers committed May 25, 2016 548 549 `````` Program Definition option_chain (c : chain (option A)) (x : A) : chain A := `````` Robbert Krebbers committed May 27, 2016 550 `````` {| chain_car n := from_option id x (c n) |}. `````` Robbert Krebbers committed May 25, 2016 551 552 553 554 555 556 557 558 559 560 `````` Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Instance option_compl : Compl (option A) := λ c, match c 0 with Some x => Some (compl (option_chain c x)) | None => None end. Definition option_cofe_mixin : CofeMixin (option A). Proof. split. - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|]. intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist. by intros n; feed inversion (Hxy n). `````` Robbert Krebbers committed May 27, 2016 561 `````` - apply _. `````` Robbert Krebbers committed May 25, 2016 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 `````` - destruct 1; constructor; by apply dist_S. - intros n c; rewrite /compl /option_compl. feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver. Qed. Canonical Structure optionC := CofeT (option A) option_cofe_mixin. Global Instance option_discrete : Discrete A → Discrete optionC. Proof. destruct 2; constructor; by apply (timeless _). Qed. Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A). Proof. by constructor. Qed. Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A). Proof. destruct 1; split; eauto. Qed. Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A). Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed May 28, 2016 577 578 579 `````` Global Instance from_option_ne {B} (R : relation B) (f : A → B) n : Proper (dist n ==> R) f → Proper (R ==> dist n ==> R) (from_option f). Proof. destruct 3; simpl; auto. Qed. `````` Robbert Krebbers committed May 25, 2016 580 581 582 583 584 `````` Global Instance None_timeless : Timeless (@None A). Proof. inversion_clear 1; constructor. Qed. Global Instance Some_timeless x : Timeless x → Timeless (Some x). Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed. `````` Robbert Krebbers committed May 27, 2016 585 586 587 588 589 590 591 592 593 594 595 596 597 `````` Lemma dist_None n mx : mx ≡{n}≡ None ↔ mx = None. Proof. split; [by inversion_clear 1|by intros ->]. Qed. Lemma dist_Some_inv_l n mx my x : mx ≡{n}≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡{n}≡ y. Proof. destruct 1; naive_solver. Qed. Lemma dist_Some_inv_r n mx my y : mx ≡{n}≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡{n}≡ y. Proof. destruct 1; naive_solver. Qed. Lemma dist_Some_inv_l' n my x : Some x ≡{n}≡ my → ∃ x', Some x' = my ∧ x ≡{n}≡ x'. Proof. intros ?%(dist_Some_inv_l _ _ _ x); naive_solver. Qed. Lemma dist_Some_inv_r' n mx y : mx ≡{n}≡ Some y → ∃ y', mx = Some y' ∧ y ≡{n}≡ y'. Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed. `````` Robbert Krebbers committed May 25, 2016 598 599 ``````End option. `````` Robbert Krebbers committed May 27, 2016 600 ``````Typeclasses Opaque option_dist. `````` Robbert Krebbers committed May 25, 2016 601 602 ``````Arguments optionC : clear implicits. `````` Robbert Krebbers committed May 28, 2016 603 604 605 ``````Instance option_fmap_ne {A B : cofeT} n: Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B). Proof. intros f f' Hf ?? []; constructor; auto. Qed. `````` Robbert Krebbers committed May 25, 2016 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 ``````Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B := CofeMor (fmap f : optionC A → optionC B). Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B). Proof. by intros f f' Hf []; constructor; apply Hf. Qed. Program Definition optionCF (F : cFunctor) : cFunctor := {| cFunctor_car A B := optionC (cFunctor_car F A B); cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg) |}. Next Obligation. by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne. Qed. Next Obligation. intros F A B x. rewrite /= -{2}(option_fmap_id x). apply option_fmap_setoid_ext=>y; apply cFunctor_id. Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose. apply option_fmap_setoid_ext=>y; apply cFunctor_compose. Qed. Instance optionCF_contractive F : cFunctorContractive F → cFunctorContractive (optionCF F). Proof. by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive. Qed. `````` Robbert Krebbers committed Nov 16, 2015 633 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 634 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 635 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 636 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 637 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Feb 10, 2016 638 ``````Lemma later_eta {A} (x : later A) : Next (later_car x) = x. `````` Robbert Krebbers committed Jan 18, 2016 639 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 640 `````` `````` Robbert Krebbers committed Nov 16, 2015 641 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 642 643 644 `````` 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 645 `````` match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 646 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 647 `````` {| chain_car n := later_car (c (S n)) |}. `````` Ralf Jung committed Apr 24, 2016 648 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. `````` Robbert Krebbers committed Feb 10, 2016 649 `````` Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)). `````` Robbert Krebbers committed Jan 14, 2016 650 `````` Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 651 652 `````` Proof. split. `````` Ralf Jung committed Apr 24, 2016 653 654 `````` - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). `````` Robbert Krebbers committed Feb 17, 2016 655 `````` - intros [|n]; [by split|split]; unfold dist, later_dist. `````` Robbert Krebbers committed Nov 16, 2015 656 657 `````` + by intros [x]. + by intros [x] [y]. `````` Ralf Jung committed Feb 20, 2016 658 `````` + by intros [x] [y] [z] ??; trans y. `````` Robbert Krebbers committed Feb 17, 2016 659 `````` - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 660 `````` - intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. `````` Robbert Krebbers committed Nov 16, 2015 661 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 662 `````` Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin. `````` Robbert Krebbers committed Feb 10, 2016 663 664 `````` Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. `````` Robbert Krebbers committed Feb 11, 2016 665 `````` Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). `````` Robbert Krebbers committed Jan 16, 2016 666 `````` Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 667 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 668 669 670 671 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := `````` Robbert Krebbers committed Feb 10, 2016 672 `````` Next (f (later_car x)). `````` Robbert Krebbers committed Jan 14, 2016 673 674 675 676 677 678 679 680 681 ``````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. `````` Robbert Krebbers committed Mar 02, 2016 682 683 684 ``````Lemma later_map_ext {A B : cofeT} (f g : A → B) x : (∀ x, f x ≡ g x) → later_map f x ≡ later_map g x. Proof. destruct x; intros Hf; apply Hf. Qed. `````` Robbert Krebbers committed Jan 14, 2016 685 686 687 ``````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 688 ``````Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed. `````` Robbert Krebbers committed Mar 02, 2016 689 `````` `````` Ralf Jung committed Mar 07, 2016 690 691 692 ``````Program Definition laterCF (F : cFunctor) : cFunctor := {| cFunctor_car A B := laterC (cFunctor_car F A B); cFunctor_map A1 A2 B1 B2 fg := laterC_map (cFunctor_map F fg) `````` Robbert Krebbers committed Mar 02, 2016 693 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 694 695 696 697 ``````Next Obligation. intros F A1 A2 B1 B2 n fg fg' ?. by apply (contractive_ne laterC_map), cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 698 ``````Next Obligation. `````` Ralf Jung committed Mar 07, 2016 699 700 701 702 703 704 705 706 `````` intros F A B x; simpl. rewrite -{2}(later_map_id x). apply later_map_ext=>y. by rewrite cFunctor_id. Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose. apply later_map_ext=>y; apply cFunctor_compose. Qed. `````` Robbert Krebbers committed Mar 07, 2016 707 ``````Instance laterCF_contractive F : cFunctorContractive (laterCF F). `````` Ralf Jung committed Mar 07, 2016 708 ``````Proof. `````` Robbert Krebbers committed Mar 07, 2016 709 `````` intros A1 A2 B1 B2 n fg fg' Hfg. `````` Ralf Jung committed Mar 07, 2016 710 `````` apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg. `````` Robbert Krebbers committed Mar 02, 2016 711 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 712 713 714 715 `````` (** Notation for writing functors *) Notation "∙" := idCF : cFunctor_scope. Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope. `````` Robbert Krebbers committed May 27, 2016 716 ``````Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope. `````` Robbert Krebbers committed May 27, 2016 717 ``````Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope. `````` Ralf Jung committed Mar 07, 2016 718 719 ``````Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope. Coercion constCF : cofeT >-> cFunctor.``````