cofe.v 20.9 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; `````` 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 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. `````` Ralf Jung committed Feb 29, 2016 87 `````` Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c 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. `````` Ralf Jung committed Feb 29, 2016 121 122 `````` 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 123 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 124 125 `````` `{!∀ 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 126 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 127 128 129 130 `````` `{!∀ 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 131 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 132 `````` Qed. `````` Robbert Krebbers committed Feb 12, 2016 133 `````` Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y : `````` Robbert Krebbers committed Feb 10, 2016 134 135 `````` x ≡{n}≡ y → f x ≡{S n}≡ f y. Proof. eauto using contractive, dist_le with omega. Qed. `````` Robbert Krebbers committed Feb 12, 2016 136 137 138 `````` 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 139 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 140 `````` Proper (dist n ==> dist n) f | 100. `````` Robbert Krebbers committed Feb 10, 2016 141 `````` Proof. by intros x y ?; apply dist_S, contractive_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 142 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 143 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Feb 24, 2016 144 `````` `````` Ralf Jung committed Feb 29, 2016 145 146 147 148 149 `````` 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 150 151 152 153 154 `````` 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 155 156 ``````End cofe. `````` Robbert Krebbers committed Mar 06, 2016 157 158 159 ``````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 160 161 162 163 ``````(** 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 164 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 165 `````` `````` Robbert Krebbers committed Nov 11, 2015 166 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 167 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 168 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 169 ``````Next Obligation. `````` Robbert Krebbers committed Mar 06, 2016 170 171 `````` intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega. `````` Robbert Krebbers committed Feb 17, 2016 172 173 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 174 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 175 ``````Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 176 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Nov 11, 2015 177 178 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 179 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 180 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 181 `````` Proof. `````` Robbert Krebbers committed Feb 18, 2016 182 `````` apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 183 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 184 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 185 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 186 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 187 `````` Proof. `````` Robbert Krebbers committed Feb 10, 2016 188 `````` intros Hfg. rewrite /fixpoint `````` Robbert Krebbers committed Feb 18, 2016 189 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 190 191 `````` 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 192 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 193 194 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 195 196 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 197 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 198 199 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 200 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 201 202 203 204 205 206 207 `````` 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 208 209 210 211 212 ``````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 213 `````` Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 214 215 216 217 218 219 `````` 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 220 221 `````` 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 222 223 224 225 `````` Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 226 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 227 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 228 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 229 230 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 231 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 232 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 233 234 `````` - intros n c x; simpl. by rewrite (conv_compl n (fun_chain c x)) /=. `````` Robbert Krebbers committed Jan 14, 2016 235 236 237 238 239 240 241 242 243 244 `````` 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. `````` Ralf Jung committed Mar 02, 2016 245 `````` `````` Robbert Krebbers committed Jan 14, 2016 246 247 248 ``````End cofe_mor. Arguments cofe_mor : clear implicits. `````` Robbert Krebbers committed Nov 11, 2015 249 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 250 251 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 252 253 254 255 `````` (** Identity and composition *) Definition cid {A} : A -n> A := CofeMor id. Instance: Params (@cid) 1. `````` Robbert Krebbers committed Mar 02, 2016 256 `````` `````` Robbert Krebbers committed Nov 11, 2015 257 258 259 260 261 ``````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 262 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 263 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 264 `````` `````` Ralf Jung committed Mar 02, 2016 265 ``````(* Function space maps *) `````` Robbert Krebbers committed Mar 02, 2016 266 ``````Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') `````` Ralf Jung committed Mar 02, 2016 267 `````` (h : A -n> B) : A' -n> B' := g ◎ h ◎ f. `````` Robbert Krebbers committed Mar 02, 2016 268 ``````Instance cofe_mor_map_ne {A A' B B'} n : `````` Ralf Jung committed Mar 02, 2016 269 `````` Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B'). `````` Robbert Krebbers committed Mar 02, 2016 270 ``````Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed. `````` Ralf Jung committed Mar 02, 2016 271 `````` `````` Robbert Krebbers committed Mar 02, 2016 272 ``````Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') : `````` Ralf Jung committed Mar 02, 2016 273 `````` (A -n> B) -n> (A' -n> B') := CofeMor (cofe_mor_map f g). `````` Robbert Krebbers committed Mar 02, 2016 274 ``````Instance cofe_morC_map_ne {A A' B B'} n : `````` Ralf Jung committed Mar 02, 2016 275 276 277 `````` 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 278 `````` by repeat apply ccompose_ne. `````` Ralf Jung committed Mar 02, 2016 279 280 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 281 ``````(** unit *) `````` Robbert Krebbers committed Jan 14, 2016 282 283 284 285 286 287 ``````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 288 `````` Global Instance unit_discrete_cofe : Discrete unitC. `````` Robbert Krebbers committed Jan 31, 2016 289 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 290 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 291 292 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 293 294 295 296 297 298 299 300 301 302 303 304 305 ``````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 306 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 307 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 308 309 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 310 311 `````` - 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 312 313 314 315 316 `````` 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 317 318 `````` Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC. Proof. intros ?? [??]; apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 319 320 321 322 323 324 ``````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 325 326 327 328 329 330 331 332 333 `````` 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 334 335 336 337 338 ``````(** Functors *) Structure cFunctor := CFunctor { cFunctor_car : cofeT → cofeT -> cofeT; 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 339 340 `````` cFunctor_ne {A1 A2 B1 B2} n : Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2); `````` Robbert Krebbers committed Mar 02, 2016 341 342 343 344 345 346 `````` 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 347 ``````Existing Instance cFunctor_ne. `````` Robbert Krebbers committed Mar 02, 2016 348 349 ``````Instance: Params (@cFunctor_map) 5. `````` Ralf Jung committed Mar 07, 2016 350 351 352 ``````Delimit Scope cFunctor_scope with CF. Bind Scope cFunctor_scope with cFunctor. `````` Ralf Jung committed Mar 07, 2016 353 354 355 ``````Class cFunctorContractive (F : cFunctor) := cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). `````` Robbert Krebbers committed Mar 02, 2016 356 357 358 359 360 361 362 ``````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 363 ``````Instance constCF_contractive B : cFunctorContractive (constCF B). `````` Robbert Krebbers committed Mar 07, 2016 364 ``````Proof. rewrite /cFunctorContractive; apply _. Qed. `````` Ralf Jung committed Mar 07, 2016 365 366 367 368 369 `````` 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 370 371 372 373 374 ``````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 375 376 377 ``````Next Obligation. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 378 379 380 381 382 383 ``````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 384 385 386 387 388 389 390 391 ``````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 392 393 394 395 396 ``````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 397 398 399 400 ``````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 401 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 402 403 `````` intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id. apply (ne_proper f). apply cFunctor_id. `````` Ralf Jung committed Mar 02, 2016 404 405 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 406 407 `````` 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 408 409 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 410 411 412 413 414 415 416 417 ``````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. `````` Ralf Jung committed Mar 07, 2016 418 `````` `````` Robbert Krebbers committed Nov 16, 2015 419 420 421 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Feb 10, 2016 422 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Ralf Jung committed Feb 29, 2016 423 `````` Instance discrete_compl : Compl A := λ c, c 0. `````` Robbert Krebbers committed Jan 14, 2016 424 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 425 426 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 427 428 429 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Ralf Jung committed Feb 29, 2016 430 431 `````` - intros n c. rewrite /compl /discrete_compl /=; symmetry; apply (chain_cauchy c 0 n). omega. `````` Robbert Krebbers committed Nov 16, 2015 432 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 433 `````` Definition discreteC : cofeT := CofeT discrete_cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 434 435 `````` Global Instance discrete_discrete_cofe : Discrete discreteC. Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 436 ``````End discrete_cofe. `````` Robbert Krebbers committed Nov 22, 2015 437 ``````Arguments discreteC _ {_ _}. `````` Robbert Krebbers committed Nov 16, 2015 438 `````` `````` Robbert Krebbers committed Nov 22, 2015 439 ``````Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _. `````` Robbert Krebbers committed Jan 16, 2016 440 441 442 ``````Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A). Proof. by intros A x y. Qed. `````` Robbert Krebbers committed Dec 11, 2015 443 444 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 445 `````` `````` Robbert Krebbers committed Nov 16, 2015 446 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 447 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 448 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 449 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 450 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Feb 10, 2016 451 ``````Lemma later_eta {A} (x : later A) : Next (later_car x) = x. `````` Robbert Krebbers committed Jan 18, 2016 452 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 453 `````` `````` Robbert Krebbers committed Nov 16, 2015 454 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 455 456 457 `````` 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 458 `````` match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 459 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 460 `````` {| chain_car n := later_car (c (S n)) |}. `````` Robbert Krebbers committed Jan 14, 2016 461 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. `````` Robbert Krebbers committed Feb 10, 2016 462 `````` Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)). `````` Robbert Krebbers committed Jan 14, 2016 463 `````` Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 464 465 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 466 `````` - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. `````` Robbert Krebbers committed Nov 16, 2015 467 `````` split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). `````` Robbert Krebbers committed Feb 17, 2016 468 `````` - intros [|n]; [by split|split]; unfold dist, later_dist. `````` Robbert Krebbers committed Nov 16, 2015 469 470 `````` + by intros [x]. + by intros [x] [y]. `````` Ralf Jung committed Feb 20, 2016 471 `````` + by intros [x] [y] [z] ??; trans y. `````` Robbert Krebbers committed Feb 17, 2016 472 `````` - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 473 `````` - intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. `````` Robbert Krebbers committed Nov 16, 2015 474 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 475 `````` Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. `````` Robbert Krebbers committed Feb 10, 2016 476 477 `````` Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. `````` Robbert Krebbers committed Feb 11, 2016 478 `````` Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). `````` Robbert Krebbers committed Jan 16, 2016 479 `````` Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 480 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 481 482 483 484 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := `````` Robbert Krebbers committed Feb 10, 2016 485 `````` Next (f (later_car x)). `````` Robbert Krebbers committed Jan 14, 2016 486 487 488 489 490 491 492 493 494 ``````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 495 496 497 ``````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 498 499 500 ``````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 501 ``````Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed. `````` Robbert Krebbers committed Mar 02, 2016 502 `````` `````` Ralf Jung committed Mar 07, 2016 503 504 505 ``````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 506 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 507 508 509 510 ``````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 511 ``````Next Obligation. `````` Ralf Jung committed Mar 07, 2016 512 513 514 515 516 517 518 519 `````` 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 520 ``````Instance laterCF_contractive F : cFunctorContractive (laterCF F). `````` Ralf Jung committed Mar 07, 2016 521 ``````Proof. `````` Robbert Krebbers committed Mar 07, 2016 522 `````` intros A1 A2 B1 B2 n fg fg' Hfg. `````` Ralf Jung committed Mar 07, 2016 523 `````` apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg. `````` Robbert Krebbers committed Mar 02, 2016 524 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 525 526 527 528 529 530 531 `````` (** Notation for writing functors *) Notation "∙" := idCF : cFunctor_scope. Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope. Notation "( F1 , F2 , .. , Fn )" := (prodCF .. (prodCF F1%CF F2%CF) .. Fn%CF) : cFunctor_scope. Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope. Coercion constCF : cofeT >-> cFunctor.``````