cofe.v 19.3 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
43
44

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

51
Record CofeMixin A `{Equiv A, Compl A} := {
52
  mixin_equiv_dist x y : x  y   n, x {n} y;
53
  mixin_dist_equivalence n : Equivalence (dist n);
54
  mixin_dist_S n x y : x {S n} y  x {n} y;
55
  mixin_conv_compl n c : compl c {n} c n
Robbert Krebbers's avatar
Robbert Krebbers committed
56
}.
57
Class Contractive `{Dist A, Dist B} (f : A  B) :=
58
  contractive n x y : ( i, i < n  x {i} y)  f x {n} f y.
Robbert Krebbers's avatar
Robbert Krebbers committed
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;
66
  cofe_mixin : CofeMixin cofe_car
Robbert Krebbers's avatar
Robbert Krebbers committed
67
}.
68
Arguments CofeT {_ _ _ _} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Add Printing Constructor cofeT.
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.
81
  Lemma equiv_dist x y : x  y   n, x {n} y.
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.
85
  Lemma dist_S n x y : x {S n} y  x {n} y.
86
  Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
87
  Lemma conv_compl n (c : chain A) : compl c {n} c n.
88
89
90
  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.

91
92
93
94
95
(** Discrete COFEs and Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x {0} y  x  y.
Arguments timeless {_} _ {_} _ _.
Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.

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

145
146
147
148
149
  Lemma conv_compl' n (c : chain A) : compl c {n} c (S n).
  Proof.
    transitivity (c n); first by apply conv_compl. symmetry.
    apply chain_cauchy. omega.
  Qed.
150
151
152
153
154
  Lemma timeless_iff n (x : A) `{!Timeless x} y : x  y  x {n} y.
  Proof.
    split; intros; [by apply equiv_dist|].
    apply (timeless _), dist_le with n; auto with lia.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
End cofe.

Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
159
160
(** 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) |}.
161
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
162

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

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

(** Function space *)
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Record cofeMor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
201
202
203
204
  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.

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

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

243
244
245
End cofe_mor.

Arguments cofe_mor : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Infix "-n>" := cofe_mor (at level 45, right associativity).
247
248
Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
249
250
251
252

(** Identity and composition *)
Definition cid {A} : A -n> A := CofeMor id.
Instance: Params (@cid) 1.
253

Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
256
257
258
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 :
259
  f1 {n} f2  g1 {n} g2  f1  g1 {n} f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
261

Ralf Jung's avatar
Ralf Jung committed
262
(* Function space maps *)
263
Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
Ralf Jung's avatar
Ralf Jung committed
264
  (h : A -n> B) : A' -n> B' := g  h  f.
265
Instance cofe_mor_map_ne {A A' B B'} n :
Ralf Jung's avatar
Ralf Jung committed
266
  Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B').
267
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Ralf Jung's avatar
Ralf Jung committed
268

269
Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
Ralf Jung's avatar
Ralf Jung committed
270
  (A -n> B) -n> (A' -n>  B') := CofeMor (cofe_mor_map f g).
271
Instance cofe_morC_map_ne {A A' B B'} n :
Ralf Jung's avatar
Ralf Jung committed
272
273
274
  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.
275
  by repeat apply ccompose_ne.
Ralf Jung's avatar
Ralf Jung committed
276
277
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
278
(** unit *)
279
280
281
282
283
284
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.
285
  Global Instance unit_discrete_cofe : Discrete unitC.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
  Proof. done. Qed.
287
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
289

(** Product *)
290
291
292
293
294
295
296
297
298
299
300
301
302
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.
303
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
304
      rewrite !equiv_dist; naive_solver.
305
306
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
308
    - intros n c; split. apply (conv_compl n (chain_map fst c)).
      apply (conv_compl n (chain_map snd c)).
309
310
311
312
313
  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.
314
315
  Global Instance prod_discrete_cofe : Discrete A  Discrete B  Discrete prodC.
  Proof. intros ?? [??]; apply _. Qed.
316
317
318
319
320
321
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
322
323
324
325
326
327
328
329
330
  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.

331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
(** Functors *)
Structure cFunctor := CFunctor {
  cFunctor_car : cofeT  cofeT -> cofeT;
  cFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
  cFunctor_ne {A1 A2 B1 B2} n :
    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
  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 (fg, g'f') x  cFunctor_map (g,g') (cFunctor_map (f,f') x)
}.
Existing Instances cFunctor_ne.
Instance: Params (@cFunctor_map) 5.

Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
Coercion cFunctor_diag : cFunctor >-> Funclass.

Program Definition idCF : cFunctor :=
  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
Solve Obligations with done.

Program Definition constCF (B : cofeT) : cFunctor :=
  {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.

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)
|}.
Next Obligation.
  by intros F1 F2 A1 A2 B1 B2 n ???; apply prodC_map_ne; apply cFunctor_ne.
Qed.
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's avatar
Ralf Jung committed
372
373
374
375
376
377
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)
|}.
Next Obligation.
378
379
  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] [??]; simpl in *.
  apply cofe_morC_map_ne; apply cFunctor_ne; by apply pair_ne.
Ralf Jung's avatar
Ralf Jung committed
380
381
Qed.
Next Obligation.
382
383
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
384
385
Qed.
Next Obligation.
386
387
  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's avatar
Ralf Jung committed
388
389
Qed.

390
391
392
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
393
  Instance discrete_dist : Dist A := λ n x y, x  y.
394
  Instance discrete_compl : Compl A := λ c, c 0.
395
  Definition discrete_cofe_mixin : CofeMixin A.
396
397
  Proof.
    split.
398
399
400
    - intros x y; split; [done|intros Hn; apply (Hn 0)].
    - done.
    - done.
401
402
    - intros n c. rewrite /compl /discrete_compl /=;
      symmetry; apply (chain_cauchy c 0 n). omega.
403
  Qed.
404
  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
405
406
  Global Instance discrete_discrete_cofe : Discrete discreteC.
  Proof. by intros x y. Qed.
407
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
Arguments discreteC _ {_ _}.
409

Robbert Krebbers's avatar
Robbert Krebbers committed
410
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
411
412
413
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
416

417
(** Later *)
418
Inductive later (A : Type) : Type := Next { later_car : A }.
419
Add Printing Constructor later.
420
Arguments Next {_} _.
421
Arguments later_car {_} _.
422
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
Proof. by destruct x. Qed.
424

425
Section later.
426
427
428
  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,
429
    match n with 0 => True | S n => later_car x {n} later_car y end.
430
  Program Definition later_chain (c : chain (later A)) : chain A :=
431
    {| chain_car n := later_car (c (S n)) |}.
432
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
433
  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
434
  Definition later_cofe_mixin : CofeMixin (later A).
435
436
  Proof.
    split.
437
    - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
438
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
439
    - intros [|n]; [by split|split]; unfold dist, later_dist.
440
441
      + by intros [x].
      + by intros [x] [y].
442
      + by intros [x] [y] [z] ??; trans y.
443
    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
445
  Qed.
446
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
447
448
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
449
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
450
  Proof. by intros x y. Qed.
451
End later.
452
453
454
455

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
456
  Next (f (later_car x)).
457
458
459
460
461
462
463
464
465
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.
466
467
468
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.
469
470
471
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).
472
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
473
474
475
476
477
478
479
480
481
482

Program Definition laterCF : cFunctor := {|
  cFunctor_car A B := laterC B;
  cFunctor_map A1 A2 B1 B2 fg := laterC_map (fg.2)
|}.
Next Obligation.
  intros F A1 A2 B1 B2 n ? [??]; simpl. by apply (contractive_ne laterC_map).
Qed.
Next Obligation. by intros A B []. Qed.
Next Obligation. by intros A1 A2 A3 B1 B2 B3 f g f' g' []. Qed.