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

(** Bundeled version *)
Structure cofeT := CofeT {
  cofe_car :> Type;
65
66
67
68
  _ : Equiv cofe_car;
  _ : Dist cofe_car;
  _ : Compl cofe_car;
  _ : 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
Instance cofe_equiv (A : cofeT) : Equiv A := let 'CofeT _ e _ _ _ := A in e.
Instance cofe_dist (A : cofeT) : Dist A := let 'CofeT _ _ d _ _ := A in d.
Instance cofe_compl (A : cofeT) : Compl A := let 'CofeT _ _ _ c _ := A in c.
75
76
77
78
79
80
81
82
83
Arguments cofe_car : simpl never.
Arguments cofe_equiv : simpl never.
Arguments cofe_dist : simpl never.
Arguments cofe_compl : simpl never.

(** Lifting properties from the mixin *)
Section cofe_mixin.
  Context {A : cofeT}.
  Implicit Types x y : A.
84
  Lemma equiv_dist x y : x  y   n, x {n} y.
85
  Proof. by destruct A as [???? []]. Qed.
86
  Global Instance dist_equivalence n : Equivalence (@dist A _ n).
87
  Proof. by destruct A as [???? []]. Qed.
88
  Lemma dist_S n x y : x {S n} y  x {n} y.
89
  Proof. destruct A as [???? []]; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  Lemma conv_compl n (c : chain A) : compl c {n} c (S n).
91
  Proof. destruct A as [???? []]; auto. Qed.
92
93
End cofe_mixin.

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

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

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

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

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

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

198
199
200
201
202
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.
203
  Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g,  x, f x {n} g x.
204
205
206
207
208
209
  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
210
211
    intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x))
      (conv_compl n (fun_chain c y)) /= Hx.
212
213
214
215
  Qed.
  Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
  Proof.
    split.
216
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
Robbert Krebbers's avatar
Robbert Krebbers committed
217
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
218
    - intros n; split.
219
220
      + by intros f x.
      + by intros f g ? x.
221
      + by intros f g h ?? x; trans (g x).
222
    - by intros n f g ? x; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
    - intros n c x; simpl.
      by rewrite (conv_compl n (fun_chain c x)) /=.
225
226
227
228
229
230
231
232
233
234
235
236
237
  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
238
Infix "-n>" := cofe_mor (at level 45, right associativity).
239
240
Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
244
245
246
247
248
249

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

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

(** Product *)
265
266
267
268
269
270
271
272
273
274
275
276
277
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.
278
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
279
      rewrite !equiv_dist; naive_solver.
280
281
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
    - intros n c; split. apply (conv_compl n (chain_map fst c)).
      apply (conv_compl n (chain_map snd c)).
284
285
286
287
288
289
290
291
292
293
294
  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
295
296
297
298
299
300
301
302
303
  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.

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

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

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

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

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

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
370
  Next (f (later_car x)).
371
372
373
374
375
376
377
378
379
380
381
382
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).
383
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.