cofe.v 15.5 KB
Newer Older
1
From algebra Require Export base.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

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's avatar
Robbert Krebbers committed
22 23
(** Unbundeled version *)
Class Dist A := dist : nat  relation A.
24
Instance: Params (@dist) 3.
25 26
Notation "x ≡{ n }≡ y" := (dist n x y)
  (at level 70, n at next level, format "x  ≡{ n }≡  y").
27
Hint Extern 0 (_ {_} _) => reflexivity.
28
Hint Extern 0 (_ {_} _) => symmetry; assumption.
29 30 31

Tactic Notation "cofe_subst" ident(x) :=
  repeat match goal with
32
  | _ => progress simplify_eq/=
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" :=
37
  repeat match goal with
38
  | _ => progress simplify_eq/=
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
41
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
42

Ralf Jung's avatar
Ralf Jung committed
43
Tactic Notation "solve_ne" := intros; solve_proper.
44

Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
Record chain (A : Type) `{Dist A} := {
  chain_car :> nat  A;
47
  chain_cauchy n i : n < i  chain_car i {n} chain_car (S n)
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51 52
}.
Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
Class Compl A `{Dist A} := compl : chain A  A.

53
Record CofeMixin A `{Equiv A, Compl A} := {
54
  mixin_equiv_dist x y : x  y   n, x {n} y;
55
  mixin_dist_equivalence n : Equivalence (dist n);
56
  mixin_dist_S n x y : x {S n} y  x {n} y;
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  mixin_conv_compl n c : compl c {n} c (S n)
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
60
  contractive n x y : ( i, i < n  x {i} y)  f x {n} f y.
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62 63 64 65 66 67

(** Bundeled version *)
Structure cofeT := CofeT {
  cofe_car :> Type;
  cofe_equiv : Equiv cofe_car;
  cofe_dist : Dist cofe_car;
  cofe_compl : Compl cofe_car;
68
  cofe_mixin : CofeMixin cofe_car
Robbert Krebbers's avatar
Robbert Krebbers committed
69
}.
70
Arguments CofeT {_ _ _ _} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Add Printing Constructor cofeT.
72 73 74 75 76 77 78 79 80 81 82
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.
83
  Lemma equiv_dist x y : x  y   n, x {n} y.
84 85 86
  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.
87
  Lemma dist_S n x y : x {S n} y  x {n} y.
88
  Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  Lemma conv_compl n (c : chain A) : compl c {n} c (S n).
90 91 92
  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.

Robbert Krebbers's avatar
Robbert Krebbers committed
93 94
(** General properties *)
Section cofe.
95 96
  Context {A : cofeT}.
  Implicit Types x y : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99
  Global Instance cofe_equivalence : Equivalence (() : relation A).
  Proof.
    split.
100 101
    - by intros x; rewrite equiv_dist.
    - by intros x y; rewrite !equiv_dist.
102
    - by intros x y z; rewrite !equiv_dist; intros; trans y.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  Qed.
104
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
107 108
    - by trans x1; [|trans y1].
    - by trans x2; [|trans y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  Qed.
110
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115
  Qed.
  Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  Lemma dist_le n n' x y : x {n} y  n'  n  x {n'} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  Proof. induction 2; eauto using dist_S. Qed.
118
  Instance ne_proper {B : cofeT} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120
    `{! 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.
121
  Instance ne_proper_2 {B C : cofeT} (f : A  B  C)
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123 124 125
    `{! n, Proper (dist n ==> dist n ==> dist n) f} :
    Proper (() ==> () ==> ()) f | 100.
  Proof.
     unfold Proper, respectful; setoid_rewrite equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  Qed.
128
  Lemma contractive_S {B : cofeT} (f : A  B) `{!Contractive f} n x y :
129 130
    x {n} y  f x {S n} f y.
  Proof. eauto using contractive, dist_le with omega. Qed.
131 132 133
  Lemma contractive_0 {B : cofeT} (f : A  B) `{!Contractive f} x y :
    f x {0} f y.
  Proof. eauto using contractive with omega. Qed.
134
  Global Instance contractive_ne {B : cofeT} (f : A  B) `{!Contractive f} n :
135
    Proper (dist n ==> dist n) f | 100.
136
  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
137
  Global Instance contractive_proper {B : cofeT} (f : A  B) `{!Contractive f} :
138
    Proper (() ==> ()) f | 100 := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
End cofe.

Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143 144
(** 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) |}.
145
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
146

Robbert Krebbers's avatar
Robbert Krebbers committed
147
(** Timeless elements *)
148
Class Timeless {A : cofeT} (x : A) := timeless y : x {0} y  x  y.
149
Arguments timeless {_} _ {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x  y  x {n} y.
151 152
Proof.
  split; intros; [by apply equiv_dist|].
153
  apply (timeless _), dist_le with n; auto with lia.
154
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155

Robbert Krebbers's avatar
Robbert Krebbers committed
156
(** Fixpoint *)
157
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A  A)
158
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Next Obligation.
160
  intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
161 162
  - apply (contractive_0 f).
  - apply (contractive_S f), IH; auto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Qed.
164
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A  A)
165
  `{!Contractive f} : A := compl (fixpoint_chain f).
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167

Section fixpoint.
168
  Context {A : cofeT} `{Inhabited A} (f : A  A) `{!Contractive f}.
169
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
    apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //.
172
    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Qed.
174
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
175
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  Proof.
177
    intros Hfg. rewrite /fixpoint
Robbert Krebbers's avatar
Robbert Krebbers committed
178
      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
179 180
    induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
    rewrite Hfg; apply contractive_S, IH; auto using dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
  Qed.
182 183
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
186
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188

(** Function space *)
Robbert Krebbers's avatar
Robbert Krebbers committed
189
Record cofeMor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191 192 193 194 195 196
  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.

197 198 199 200 201
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.
202
  Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g,  x, f x {n} g x.
203 204 205 206 207 208
  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's avatar
Robbert Krebbers committed
209 210
    intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x))
      (conv_compl n (fun_chain c y)) /= Hx.
211 212 213 214
  Qed.
  Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
  Proof.
    split.
215
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
Robbert Krebbers's avatar
Robbert Krebbers committed
216
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
217
    - intros n; split.
218 219
      + by intros f x.
      + by intros f g ? x.
220
      + by intros f g h ?? x; trans (g x).
221
    - by intros n f g ? x; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
222 223
    - intros n c x; simpl.
      by rewrite (conv_compl n (fun_chain c x)) /=.
224 225 226 227 228 229 230 231 232 233 234 235 236
  Qed.
  Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.

  Global Instance cofe_mor_car_ne n :
    Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
  Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
  Global Instance cofe_mor_car_proper :
    Proper (() ==> () ==> ()) (@cofe_mor_car A B) := ne_proper_2 _.
  Lemma cofe_mor_ext (f g : cofeMor A B) : f  g   x, f x  g x.
  Proof. done. Qed.
End cofe_mor.

Arguments cofe_mor : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Infix "-n>" := cofe_mor (at level 45, right associativity).
238 239
Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242 243 244 245 246 247 248

(** 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 :
249
  f1 {n} f2  g1 {n} g2  f1  g1 {n} f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
251 252

(** unit *)
253 254 255 256 257 258
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's avatar
Robbert Krebbers committed
259 260
  Global Instance unit_timeless (x : ()) : Timeless x.
  Proof. done. Qed.
261
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
262 263

(** Product *)
264 265 266 267 268 269 270 271 272 273 274 275 276
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.
277
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
278
      rewrite !equiv_dist; naive_solver.
279 280
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
281 282
    - intros n c; split. apply (conv_compl n (chain_map fst c)).
      apply (conv_compl n (chain_map snd c)).
283 284 285 286 287 288 289 290 291 292 293
  Qed.
  Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
  Global Instance pair_timeless (x : A) (y : B) :
    Timeless x  Timeless y  Timeless (x,y).
  Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
End product.

Arguments prodC : clear implicits.
Typeclasses Opaque prod_dist.

Instance prod_map_ne {A A' B B' : cofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296 297 298 299 300 301 302
  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.

303 304 305
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
306
  Instance discrete_dist : Dist A := λ n x y, x  y.
307
  Instance discrete_compl : Compl A := λ c, c 1.
308
  Definition discrete_cofe_mixin : CofeMixin A.
309 310
  Proof.
    split.
311 312 313
    - intros x y; split; [done|intros Hn; apply (Hn 0)].
    - done.
    - done.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
    - intros n c. rewrite /compl /discrete_compl /=.
315
      symmetry; apply (chain_cauchy c 0 (S n)); omega.
316
  Qed.
317 318
  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
  Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
Robbert Krebbers's avatar
Robbert Krebbers committed
319
  Proof. by intros y. Qed.
320
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
Arguments discreteC _ {_ _}.
322

Robbert Krebbers's avatar
Robbert Krebbers committed
323
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
324 325 326
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
327 328
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
329

330
(** Later *)
331
Inductive later (A : Type) : Type := Next { later_car : A }.
332
Add Printing Constructor later.
333
Arguments Next {_} _.
334
Arguments later_car {_} _.
335
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Proof. by destruct x. Qed.
337

338
Section later.
339 340 341
  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,
342
    match n with 0 => True | S n => later_car x {n} later_car y end.
343
  Program Definition later_chain (c : chain (later A)) : chain A :=
344
    {| chain_car n := later_car (c (S n)) |}.
345
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
346
  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
347
  Definition later_cofe_mixin : CofeMixin (later A).
348 349
  Proof.
    split.
350
    - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
351
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
352
    - intros [|n]; [by split|split]; unfold dist, later_dist.
353 354
      + by intros [x].
      + by intros [x] [y].
355
      + by intros [x] [y] [z] ??; trans y.
356
    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
357
    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
358
  Qed.
359
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
360 361
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
362
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
363
  Proof. by intros x y. Qed.
364
End later.
365 366 367 368

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
369
  Next (f (later_car x)).
370 371 372 373 374 375 376 377 378 379 380 381
Instance later_map_ne {A B : cofeT} (f : A  B) n :
  Proper (dist (pred n) ==> dist (pred n)) f 
  Proper (dist n ==> dist n) (later_map f) | 0.
Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
Lemma later_map_id {A} (x : later A) : later_map id x = x.
Proof. by destruct x. Qed.
Lemma later_map_compose {A B C} (f : A  B) (g : B  C) (x : later A) :
  later_map (g  f) x = later_map g (later_map f x).
Proof. by destruct x. Qed.
Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
  CofeMor (later_map f).
Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
382
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.