cofe.v 24.6 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 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 May 25, 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 ``````(** Discrete COFEs and Timeless elements *) `````` Ralf Jung committed Mar 15, 2016 92 ``````(* TODO: On paper, We called these "discrete elements". I think that makes `````` Ralf Jung committed Mar 07, 2016 93 `````` more sense. *) `````` Robbert Krebbers committed Feb 24, 2016 94 95 96 97 ``````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 98 99 ``````(** General properties *) Section cofe. `````` Robbert Krebbers committed Jan 14, 2016 100 101 `````` Context {A : cofeT}. Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 102 103 104 `````` Global Instance cofe_equivalence : Equivalence ((≡) : relation A). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 105 106 `````` - by intros x; rewrite equiv_dist. - by intros x y; rewrite !equiv_dist. `````` Ralf Jung committed Feb 20, 2016 107 `````` - by intros x y z; rewrite !equiv_dist; intros; trans y. `````` Robbert Krebbers committed Nov 11, 2015 108 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 109 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 110 111 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Ralf Jung committed Feb 20, 2016 112 113 `````` - by trans x1; [|trans y1]. - by trans x2; [|trans y2]. `````` Robbert Krebbers committed Nov 11, 2015 114 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 115 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 116 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 117 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 118 119 120 `````` 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 121 `````` Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. `````` Robbert Krebbers committed Nov 11, 2015 122 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Ralf Jung committed Feb 29, 2016 123 124 `````` 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 125 `````` Instance ne_proper {B : cofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 126 127 `````` `{!∀ 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 128 `````` Instance ne_proper_2 {B C : cofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 129 130 131 132 `````` `{!∀ 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 133 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 134 `````` Qed. `````` Robbert Krebbers committed Feb 12, 2016 135 `````` Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y : `````` Robbert Krebbers committed Feb 10, 2016 136 137 `````` x ≡{n}≡ y → f x ≡{S n}≡ f y. Proof. eauto using contractive, dist_le with omega. Qed. `````` Robbert Krebbers committed Feb 12, 2016 138 139 140 `````` 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 141 `````` Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n : `````` Robbert Krebbers committed Nov 12, 2015 142 `````` Proper (dist n ==> dist n) f | 100. `````` Robbert Krebbers committed Feb 10, 2016 143 `````` Proof. by intros x y ?; apply dist_S, contractive_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 144 `````` Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : `````` Robbert Krebbers committed Nov 12, 2015 145 `````` Proper ((≡) ==> (≡)) f | 100 := _. `````` Robbert Krebbers committed Feb 24, 2016 146 `````` `````` Ralf Jung committed Feb 29, 2016 147 148 149 150 151 `````` 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 152 153 154 155 156 `````` 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 157 158 ``````End cofe. `````` Robbert Krebbers committed Mar 06, 2016 159 160 161 ``````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 162 163 164 165 ``````(** 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 166 ``````Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Robbert Krebbers committed Nov 22, 2015 167 `````` `````` Robbert Krebbers committed Nov 11, 2015 168 ``````(** Fixpoint *) `````` Robbert Krebbers committed Jan 14, 2016 169 ``````Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 170 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 171 ``````Next Obligation. `````` Robbert Krebbers committed Mar 06, 2016 172 173 `````` intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega. `````` Robbert Krebbers committed Feb 17, 2016 174 175 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 176 ``````Qed. `````` Robbert Krebbers committed Mar 18, 2016 177 178 `````` Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 179 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Mar 18, 2016 180 181 182 ``````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 183 184 `````` Section fixpoint. `````` Robbert Krebbers committed Jan 14, 2016 185 `````` Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Nov 17, 2015 186 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 187 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 188 189 `````` apply equiv_dist=>n. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 190 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 191 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 192 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 193 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 194 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 195 `````` intros Hfg. rewrite fixpoint_eq /fixpoint_def `````` Robbert Krebbers committed Feb 18, 2016 196 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 197 198 `````` 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 199 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 200 201 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 202 203 204 205 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. (** Function space *) `````` Robbert Krebbers committed Dec 15, 2015 206 ``````Record cofeMor (A B : cofeT) : Type := CofeMor { `````` Robbert Krebbers committed Nov 11, 2015 207 208 209 210 211 212 213 `````` 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 214 215 216 217 218 ``````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 219 `````` Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 220 221 222 223 224 225 `````` 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 226 227 `````` 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 228 229 230 231 `````` Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 232 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 233 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 234 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 235 236 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 237 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 238 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 239 240 `````` - intros n c x; simpl. by rewrite (conv_compl n (fun_chain c x)) /=. `````` Robbert Krebbers committed Jan 14, 2016 241 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 242 `````` Canonical Structure cofe_mor : cofeT := CofeT (cofeMor A B) cofe_mor_cofe_mixin. `````` Robbert Krebbers committed Jan 14, 2016 243 244 245 246 247 248 249 250 251 252 253 `````` 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 254 ``````Infix "-n>" := cofe_mor (at level 45, right associativity). `````` Robbert Krebbers committed Jan 14, 2016 255 256 ``````Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). `````` Robbert Krebbers committed Nov 11, 2015 257 `````` `````` Ralf Jung committed Mar 17, 2016 258 ``````(** Identity and composition and constant function *) `````` Robbert Krebbers committed Nov 11, 2015 259 260 ``````Definition cid {A} : A -n> A := CofeMor id. Instance: Params (@cid) 1. `````` Ralf Jung committed Mar 17, 2016 261 262 ``````Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x). Instance: Params (@cconst) 2. `````` Robbert Krebbers committed Mar 02, 2016 263 `````` `````` Robbert Krebbers committed Nov 11, 2015 264 265 266 267 268 ``````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 269 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 270 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 271 `````` `````` Ralf Jung committed Mar 02, 2016 272 ``````(* Function space maps *) `````` Robbert Krebbers committed Mar 02, 2016 273 ``````Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') `````` Ralf Jung committed Mar 02, 2016 274 `````` (h : A -n> B) : A' -n> B' := g ◎ h ◎ f. `````` Robbert Krebbers committed Mar 02, 2016 275 ``````Instance cofe_mor_map_ne {A A' B B'} n : `````` Ralf Jung committed Mar 02, 2016 276 `````` Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B'). `````` Robbert Krebbers committed Mar 02, 2016 277 ``````Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed. `````` Ralf Jung committed Mar 02, 2016 278 `````` `````` Robbert Krebbers committed Mar 02, 2016 279 ``````Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') : `````` Ralf Jung committed Mar 02, 2016 280 `````` (A -n> B) -n> (A' -n> B') := CofeMor (cofe_mor_map f g). `````` Robbert Krebbers committed Mar 02, 2016 281 ``````Instance cofe_morC_map_ne {A A' B B'} n : `````` Ralf Jung committed Mar 02, 2016 282 283 284 `````` 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 285 `````` by repeat apply ccompose_ne. `````` Ralf Jung committed Mar 02, 2016 286 287 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 288 ``````(** unit *) `````` Robbert Krebbers committed Jan 14, 2016 289 290 291 292 293 ``````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 294 `````` Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 295 `````` Global Instance unit_discrete_cofe : Discrete unitC. `````` Robbert Krebbers committed Jan 31, 2016 296 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 297 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 298 299 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 300 301 302 303 304 305 306 307 308 309 310 311 312 ``````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 313 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 314 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 315 316 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 317 318 `````` - 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 319 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 320 `````` Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin. `````` Robbert Krebbers committed Jan 14, 2016 321 322 323 `````` 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 324 325 `````` Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC. Proof. intros ?? [??]; apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 326 327 328 329 330 331 ``````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 332 333 334 335 336 337 338 339 340 `````` 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 341 342 ``````(** Functors *) Structure cFunctor := CFunctor { `````` Robbert Krebbers committed May 27, 2016 343 `````` cFunctor_car : cofeT → cofeT → cofeT; `````` Robbert Krebbers committed Mar 02, 2016 344 345 `````` 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 346 347 `````` cFunctor_ne {A1 A2 B1 B2} n : Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2); `````` Robbert Krebbers committed Mar 02, 2016 348 349 350 351 352 353 `````` 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 354 ``````Existing Instance cFunctor_ne. `````` Robbert Krebbers committed Mar 02, 2016 355 356 ``````Instance: Params (@cFunctor_map) 5. `````` Ralf Jung committed Mar 07, 2016 357 358 359 ``````Delimit Scope cFunctor_scope with CF. Bind Scope cFunctor_scope with cFunctor. `````` Ralf Jung committed Mar 07, 2016 360 361 362 ``````Class cFunctorContractive (F : cFunctor) := cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). `````` Robbert Krebbers committed Mar 02, 2016 363 364 365 366 367 368 369 ``````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 370 ``````Instance constCF_contractive B : cFunctorContractive (constCF B). `````` Robbert Krebbers committed Mar 07, 2016 371 ``````Proof. rewrite /cFunctorContractive; apply _. Qed. `````` Ralf Jung committed Mar 07, 2016 372 373 374 375 376 `````` 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 377 378 379 380 381 ``````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 382 383 384 ``````Next Obligation. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 385 386 387 388 389 390 ``````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 391 392 393 394 395 396 397 398 ``````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 399 400 401 402 403 ``````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 404 405 406 407 ``````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 408 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 409 410 `````` intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id. apply (ne_proper f). apply cFunctor_id. `````` Ralf Jung committed Mar 02, 2016 411 412 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 413 414 `````` 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 415 416 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 417 418 419 420 421 422 423 424 ``````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 Nov 16, 2015 425 426 427 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Feb 10, 2016 428 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Ralf Jung committed Feb 29, 2016 429 `````` Instance discrete_compl : Compl A := λ c, c 0. `````` Robbert Krebbers committed Jan 14, 2016 430 `````` Definition discrete_cofe_mixin : CofeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 431 432 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 433 434 435 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Ralf Jung committed Feb 29, 2016 436 437 `````` - intros n c. rewrite /compl /discrete_compl /=; symmetry; apply (chain_cauchy c 0 n). omega. `````` Robbert Krebbers committed Nov 16, 2015 438 439 440 `````` Qed. End discrete_cofe. `````` Robbert Krebbers committed May 25, 2016 441 442 443 444 445 446 447 448 ``````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 449 `````` `````` Robbert Krebbers committed Dec 11, 2015 450 451 ``````Canonical Structure natC := leibnizC nat. Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Nov 19, 2015 452 `````` `````` Robbert Krebbers committed May 25, 2016 453 454 455 456 ``````(* Option *) Section option. Context {A : cofeT}. `````` Robbert Krebbers committed May 27, 2016 457 `````` Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n). `````` Robbert Krebbers committed May 25, 2016 458 459 `````` Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my. `````` Robbert Krebbers committed May 27, 2016 460 `````` Proof. done. Qed. `````` Robbert Krebbers committed May 25, 2016 461 462 463 464 465 466 467 468 469 470 471 472 473 `````` Program Definition option_chain (c : chain (option A)) (x : A) : chain A := {| chain_car n := from_option x (c n) |}. 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 474 `````` - apply _. `````` Robbert Krebbers committed May 25, 2016 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 `````` - 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. Global Instance from_option_ne n : Proper (dist n ==> dist n ==> dist n) (@from_option A). Proof. by destruct 2. Qed. 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. End option. `````` Robbert Krebbers committed May 27, 2016 500 ``````Typeclasses Opaque option_dist. `````` Robbert Krebbers committed May 25, 2016 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 ``````Arguments optionC : clear implicits. Instance option_fmap_ne {A B : cofeT} (f : A → B) n: Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f). Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed. 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 533 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 534 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 535 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 536 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 537 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Feb 10, 2016 538 ``````Lemma later_eta {A} (x : later A) : Next (later_car x) = x. `````` Robbert Krebbers committed Jan 18, 2016 539 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Dec 21, 2015 540 `````` `````` Robbert Krebbers committed Nov 16, 2015 541 ``````Section later. `````` Robbert Krebbers committed Jan 14, 2016 542 543 544 `````` 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 545 `````` match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end. `````` Robbert Krebbers committed Jan 14, 2016 546 `````` Program Definition later_chain (c : chain (later A)) : chain A := `````` Robbert Krebbers committed Nov 16, 2015 547 `````` {| chain_car n := later_car (c (S n)) |}. `````` Ralf Jung committed Apr 24, 2016 548 `````` Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. `````` Robbert Krebbers committed Feb 10, 2016 549 `````` Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)). `````` Robbert Krebbers committed Jan 14, 2016 550 `````` Definition later_cofe_mixin : CofeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 551 552 `````` Proof. split. `````` Ralf Jung committed Apr 24, 2016 553 554 `````` - 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 555 `````` - intros [|n]; [by split|split]; unfold dist, later_dist. `````` Robbert Krebbers committed Nov 16, 2015 556 557 `````` + by intros [x]. + by intros [x] [y]. `````` Ralf Jung committed Feb 20, 2016 558 `````` + by intros [x] [y] [z] ??; trans y. `````` Robbert Krebbers committed Feb 17, 2016 559 `````` - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 560 `````` - intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. `````` Robbert Krebbers committed Nov 16, 2015 561 `````` Qed. `````` Robbert Krebbers committed May 25, 2016 562 `````` Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin. `````` Robbert Krebbers committed Feb 10, 2016 563 564 `````` Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. `````` Robbert Krebbers committed Feb 11, 2016 565 `````` Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). `````` Robbert Krebbers committed Jan 16, 2016 566 `````` Proof. by intros x y. Qed. `````` Robbert Krebbers committed Nov 16, 2015 567 ``````End later. `````` Robbert Krebbers committed Jan 14, 2016 568 569 570 571 `````` Arguments laterC : clear implicits. Definition later_map {A B} (f : A → B) (x : later A) : later B := `````` Robbert Krebbers committed Feb 10, 2016 572 `````` Next (f (later_car x)). `````` Robbert Krebbers committed Jan 14, 2016 573 574 575 576 577 578 579 580 581 ``````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 582 583 584 ``````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 585 586 587 ``````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 588 ``````Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed. `````` Robbert Krebbers committed Mar 02, 2016 589 `````` `````` Ralf Jung committed Mar 07, 2016 590 591 592 ``````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 593 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 594 595 596 597 ``````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 598 ``````Next Obligation. `````` Ralf Jung committed Mar 07, 2016 599 600 601 602 603 604 605 606 `````` 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 607 ``````Instance laterCF_contractive F : cFunctorContractive (laterCF F). `````` Ralf Jung committed Mar 07, 2016 608 ``````Proof. `````` Robbert Krebbers committed Mar 07, 2016 609 `````` intros A1 A2 B1 B2 n fg fg' Hfg. `````` Ralf Jung committed Mar 07, 2016 610 `````` apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg. `````` Robbert Krebbers committed Mar 02, 2016 611 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 612 613 614 615 `````` (** 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 616 ``````Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope. `````` Ralf Jung committed Mar 07, 2016 617 618 ``````Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope. Coercion constCF : cofeT >-> cFunctor.``````