cofe.v 13.5 KB
 Robbert Krebbers committed Jan 13, 2016 1 ``````Require Export modures.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. `````` Robbert Krebbers committed Nov 11, 2015 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 ={_}= ?x) => 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 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 `````` Record chain (A : Type) `{Dist A} := { chain_car :> nat → A; chain_cauchy n i : n ≤ i → chain_car n ={n}= chain_car i }. Arguments chain_car {_ _} _ _. Arguments chain_cauchy {_ _} _ _ _ _. Class Compl A `{Dist A} := compl : chain A → A. Class Cofe A `{Equiv A, Compl A} := { equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y; dist_equivalence n :> Equivalence (dist n); dist_S n x y : x ={S n}= y → x ={n}= y; dist_0 x y : x ={0}= y; conv_compl (c : chain A) n : compl c ={n}= c n }. Hint Extern 0 (_ ={0}= _) => apply dist_0. Class Contractive `{Dist A, Dist B} (f : A -> B) := contractive n : Proper (dist n ==> dist (S n)) f. (** Bundeled version *) Structure cofeT := CofeT { cofe_car :> Type; cofe_equiv : Equiv cofe_car; cofe_dist : Dist cofe_car; cofe_compl : Compl cofe_car; cofe_cofe : Cofe cofe_car }. Arguments CofeT _ {_ _ _ _}. Add Printing Constructor cofeT. Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe. `````` Robbert Krebbers committed Nov 19, 2015 54 55 56 57 58 ``````Arguments cofe_car _ : simpl never. Arguments cofe_equiv _ _ _ : simpl never. Arguments cofe_dist _ _ _ _ : simpl never. Arguments cofe_compl _ _ : simpl never. Arguments cofe_cofe _ : simpl never. `````` Robbert Krebbers committed Nov 11, 2015 59 60 61 62 63 64 65 66 67 68 69 70 71 72 `````` (** General properties *) Section cofe. Context `{Cofe A}. 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. Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (dist n). Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Robbert Krebbers committed Dec 15, 2015 73 74 `````` * by transitivity x1; [|transitivity y1]. * by transitivity x2; [|transitivity y2]. `````` Robbert Krebbers committed Nov 11, 2015 75 76 77 `````` Qed. Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (dist n). Proof. `````` Robbert Krebbers committed Jan 13, 2016 78 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 79 80 81 82 83 `````` Qed. Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x). Proof. by apply dist_proper. Qed. Lemma dist_le x y n n' : x ={n}= y → n' ≤ n → x ={n'}= y. Proof. induction 2; eauto using dist_S. Qed. `````` Robbert Krebbers committed Nov 12, 2015 84 `````` Instance ne_proper `{Cofe B} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 85 86 `````` `{!∀ 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 Nov 12, 2015 87 `````` Instance ne_proper_2 `{Cofe B, Cofe C} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 88 89 90 91 `````` `{!∀ 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 92 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 93 94 `````` Qed. Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n → compl c1 ={n}= compl c2. `````` Robbert Krebbers committed Jan 13, 2016 95 `````` Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed. `````` Robbert Krebbers committed Nov 11, 2015 96 97 `````` Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2. Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed. `````` Robbert Krebbers committed Nov 12, 2015 98 99 100 101 102 `````` Global Instance contractive_ne `{Cofe B} (f : A → B) `{!Contractive f} n : Proper (dist n ==> dist n) f | 100. Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed. Global Instance contractive_proper `{Cofe B} (f : A → B) `{!Contractive f} : Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Nov 11, 2015 103 104 ``````End cofe. `````` Robbert Krebbers committed Nov 22, 2015 105 106 107 108 109 110 ``````(** 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) |}. Next Obligation. by intros A ? B ? f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 18, 2015 111 112 113 114 ``````(** Timeless elements *) Class Timeless `{Dist A, Equiv A} (x : A) := timeless y : x ={1}= y → x ≡ y. Arguments timeless {_ _ _} _ {_} _ _. `````` Robbert Krebbers committed Nov 11, 2015 115 ``````(** Fixpoint *) `````` Robbert Krebbers committed Nov 17, 2015 116 117 ``````Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 118 119 ``````Next Obligation. intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|]. `````` Robbert Krebbers committed Jan 13, 2016 120 `````` destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia. `````` Robbert Krebbers committed Nov 11, 2015 121 ``````Qed. `````` Robbert Krebbers committed Nov 17, 2015 122 123 ``````Program Definition fixpoint `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Nov 11, 2015 124 125 `````` Section fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 126 127 `````` Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}. Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 128 129 `````` Proof. apply equiv_dist; intros n; unfold fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 130 `````` rewrite (conv_compl (fixpoint_chain f) n). `````` Robbert Krebbers committed Jan 13, 2016 131 `````` by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia. `````` Robbert Krebbers committed Nov 11, 2015 132 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 133 134 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : (∀ z, f z ={n}= g z) → fixpoint f ={n}= fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 135 `````` Proof. `````` Robbert Krebbers committed Nov 17, 2015 136 `````` intros Hfg; unfold fixpoint. `````` Robbert Krebbers committed Jan 13, 2016 137 138 `````` rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n). induction n as [|n IH]; simpl in *; first done. `````` Robbert Krebbers committed Nov 11, 2015 139 140 `````` rewrite Hfg; apply contractive, IH; auto using dist_S. Qed. `````` Robbert Krebbers committed Nov 17, 2015 141 142 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 143 144 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. `````` Robbert Krebbers committed Nov 17, 2015 145 ``````Global Opaque fixpoint. `````` Robbert Krebbers committed Nov 11, 2015 146 147 `````` (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 148 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 `````` 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. Instance cofe_mor_proper `(f : cofeMor A B) : Proper ((≡) ==> (≡)) f := _. Instance cofe_mor_equiv {A B : cofeT} : Equiv (cofeMor A B) := λ f g, ∀ x, f x ≡ g x. Instance cofe_mor_dist (A B : cofeT) : Dist (cofeMor A B) := λ n f g, ∀ x, f x ={n}= g x. Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B := {| chain_car n := c n x |}. Next Obligation. intros A B c x n i ?. by apply (chain_cauchy c). Qed. Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c, {| cofe_mor_car x := compl (fun_chain c x) |}. Next Obligation. intros A B c n x y Hxy. `````` Robbert Krebbers committed Jan 13, 2016 168 169 `````` rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hxy. apply (chain_cauchy c); lia. `````` Robbert Krebbers committed Nov 11, 2015 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 ``````Qed. Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B). Proof. split. * intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|]. intros HXY k; apply equiv_dist; intros n; apply HXY. * 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. * by intros f g x. * intros c n x; simpl. rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia. Qed. `````` Robbert Krebbers committed Nov 12, 2015 185 186 187 188 189 ``````Instance cofe_mor_car_ne A B 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. Instance cofe_mor_car_proper A B : Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _. `````` Robbert Krebbers committed Nov 11, 2015 190 191 192 193 ``````Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x. Proof. done. Qed. Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B). Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Nov 17, 2015 194 195 ``````Instance cofe_more_inhabited (A B : cofeT) `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 196 197 198 199 200 201 202 203 204 205 `````` (** 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 : f1 ={n}= f2 → g1 ={n}= g2 → f1 ◎ g1 ={n}= f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 206 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 `````` (** Pre-composition as a functor *) Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n : Proper (dist n ==> dist n) (λ g : A -n> C, g ◎ f). Proof. by intros g1 g2 ?; apply ccompose_ne. Qed. Definition ccompose_l {A B C} (f : B -n> A) : (A -n> C) -n> (B -n> C) := CofeMor (λ g : A -n> C, g ◎ f). Instance ccompose_l_ne {A B C} : Proper (dist n ==> dist n) (@ccompose_l A B C). Proof. by intros n f1 f2 Hf g x; apply ccompose_ne. Qed. (** unit *) Instance unit_dist : Dist unit := λ _ _ _, True. Instance unit_compl : Compl unit := λ _, (). Instance unit_cofe : Cofe unit. Proof. by repeat split; try exists 0. Qed. (** Product *) Instance prod_dist `{Dist A, Dist B} : Dist (A * B) := λ n, prod_relation (dist n) (dist n). `````` Robbert Krebbers committed Nov 22, 2015 226 227 228 229 ``````Instance pair_ne `{Dist A, Dist B} : Proper (dist n ==> dist n ==> dist n) (@pair A B) := _. Instance fst_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@fst A B) := _. Instance snd_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@snd A B) := _. `````` Robbert Krebbers committed Nov 11, 2015 230 ``````Instance prod_compl `{Compl A, Compl B} : Compl (A * B) := λ c, `````` Robbert Krebbers committed Nov 22, 2015 231 `````` (compl (chain_map fst c), compl (chain_map snd c)). `````` Robbert Krebbers committed Nov 11, 2015 232 233 234 235 236 237 238 239 ``````Instance prod_cofe `{Cofe A, Cofe B} : Cofe (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. * by split. `````` Robbert Krebbers committed Nov 22, 2015 240 241 `````` * intros c n; split. apply (conv_compl (chain_map fst c) n). apply (conv_compl (chain_map snd c) n). `````` Robbert Krebbers committed Nov 11, 2015 242 ``````Qed. `````` Robbert Krebbers committed Nov 18, 2015 243 244 245 ``````Instance pair_timeless `{Dist A, Equiv A, Dist B, Equiv B} (x : A) (y : B) : Timeless x → Timeless y → Timeless (x,y). Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed. `````` Robbert Krebbers committed Nov 11, 2015 246 ``````Canonical Structure prodC (A B : cofeT) : cofeT := CofeT (A * B). `````` Robbert Krebbers committed Nov 16, 2015 247 ``````Instance prod_map_ne `{Dist A, Dist A', Dist B, Dist B'} n : `````` Robbert Krebbers committed Nov 11, 2015 248 249 250 251 252 253 254 255 256 257 `````` 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. Typeclasses Opaque prod_dist. `````` Robbert Krebbers committed Nov 16, 2015 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 `````` (** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. Instance discrete_dist : Dist A := λ n x y, match n with 0 => True | S n => x ≡ y end. Instance discrete_compl : Compl A := λ c, c 1. Instance discrete_cofe : Cofe A. Proof. split. * intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)]. * intros [|n]; [done|apply _]. * by intros [|n]. * done. * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia]. Qed. `````` Robbert Krebbers committed Nov 18, 2015 274 275 `````` Global Instance discrete_timeless (x : A) : Timeless x. Proof. by intros y. Qed. `````` Robbert Krebbers committed Nov 22, 2015 276 `````` Definition discreteC : cofeT := CofeT A. `````` Robbert Krebbers committed Nov 16, 2015 277 ``````End discrete_cofe. `````` Robbert Krebbers committed Nov 22, 2015 278 ``````Arguments discreteC _ {_ _}. `````` Robbert Krebbers committed Nov 16, 2015 279 `````` `````` Robbert Krebbers committed Nov 22, 2015 280 ``````Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _. `````` Robbert Krebbers committed Dec 11, 2015 281 282 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 283 `````` `````` Robbert Krebbers committed Nov 16, 2015 284 285 ``````(** Later *) Inductive later (A : Type) : Type := Later { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 286 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Nov 16, 2015 287 288 ``````Arguments Later {_} _. Arguments later_car {_} _. `````` Robbert Krebbers committed Dec 21, 2015 289 `````` `````` Robbert Krebbers committed Nov 16, 2015 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 ``````Section later. Instance later_equiv `{Equiv A} : Equiv (later A) := λ x y, later_car x ≡ later_car y. Instance later_dist `{Dist A} : Dist (later A) := λ n x y, match n with 0 => True | S n => later_car x ={n}= later_car y end. Program Definition later_chain `{Dist A} (c : chain (later A)) : chain A := {| chain_car n := later_car (c (S n)) |}. Next Obligation. intros A ? c n i ?; apply (chain_cauchy c (S n)); lia. Qed. Instance later_compl `{Compl A} : Compl (later A) := λ c, Later (compl (later_chain c)). Instance later_cofe `{Cofe A} : Cofe (later A). 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. * done. * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)]. Qed. Canonical Structure laterC (A : cofeT) : cofeT := CofeT (later A). `````` Robbert Krebbers committed Dec 21, 2015 315 316 `````` Global Instance Later_contractive `{Dist A} : Contractive (@Later A). Proof. by intros n ??. Qed. `````` Robbert Krebbers committed Dec 15, 2015 317 318 `````` Definition later_map {A B} (f : A → B) (x : later A) : later B := Later (f (later_car x)). `````` Robbert Krebbers committed Dec 21, 2015 319 320 321 322 `````` Global Instance later_map_ne `{Cofe A, Cofe B} (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. `````` Robbert Krebbers committed Dec 15, 2015 323 `````` Lemma later_fmap_id {A} (x : later A) : later_map id x = x. `````` Robbert Krebbers committed Nov 16, 2015 324 325 `````` Proof. by destruct x. Qed. Lemma later_fmap_compose {A B C} (f : A → B) (g : B → C) (x : later A) : `````` Robbert Krebbers committed Dec 15, 2015 326 `````` later_map (g ∘ f) x = later_map g (later_map f x). `````` Robbert Krebbers committed Nov 16, 2015 327 328 `````` Proof. by destruct x. Qed. Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B := `````` Robbert Krebbers committed Dec 15, 2015 329 `````` CofeMor (later_map f). `````` Robbert Krebbers committed Nov 16, 2015 330 `````` Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B). `````` Robbert Krebbers committed Nov 16, 2015 331 332 `````` Proof. intros n f g Hf n'; apply Hf. Qed. End later.``````