cofe.v 20.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 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.

157 158 159
Instance const_contractive {A B : cofeT} (x : A) : Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.

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

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

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

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

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

246 247 248
End cofe_mor.

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

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

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

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

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

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

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

334 335 336 337 338
(** 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;
339 340
  cFunctor_ne {A1 A2 B1 B2} n :
    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
341 342 343 344 345 346
  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)
}.
347
Existing Instance cFunctor_ne.
348 349
Instance: Params (@cFunctor_map) 5.

350 351 352
Class cFunctorContractive (F : cFunctor) :=
  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).

353 354 355 356 357 358 359
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.

360
Instance constCF_contractive B : cFunctorContractive (constCF B).
361
Proof. rewrite /cFunctorContractive; apply _. Qed.
362 363 364 365 366

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

367 368 369 370 371
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)
|}.
372 373 374
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
Qed.
375 376 377 378 379 380
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.

381 382 383 384 385 386 387 388
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's avatar
Ralf Jung committed
389 390 391 392 393
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)
|}.
394 395 396 397
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's avatar
Ralf Jung committed
398
Next Obligation.
399 400
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
401 402
Qed.
Next Obligation.
403 404
  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
405 406
Qed.

407 408 409 410 411 412 413 414
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.

415 416 417
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
418
  Instance discrete_dist : Dist A := λ n x y, x  y.
419
  Instance discrete_compl : Compl A := λ c, c 0.
420
  Definition discrete_cofe_mixin : CofeMixin A.
421 422
  Proof.
    split.
423 424 425
    - intros x y; split; [done|intros Hn; apply (Hn 0)].
    - done.
    - done.
426 427
    - intros n c. rewrite /compl /discrete_compl /=;
      symmetry; apply (chain_cauchy c 0 n). omega.
428
  Qed.
429
  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
430 431
  Global Instance discrete_discrete_cofe : Discrete discreteC.
  Proof. by intros x y. Qed.
432
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
Arguments discreteC _ {_ _}.
434

Robbert Krebbers's avatar
Robbert Krebbers committed
435
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
436 437 438
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
439 440
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
441

442
(** Later *)
443
Inductive later (A : Type) : Type := Next { later_car : A }.
444
Add Printing Constructor later.
445
Arguments Next {_} _.
446
Arguments later_car {_} _.
447
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
Proof. by destruct x. Qed.
449

450
Section later.
451 452 453
  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,
454
    match n with 0 => True | S n => later_car x {n} later_car y end.
455
  Program Definition later_chain (c : chain (later A)) : chain A :=
456
    {| chain_car n := later_car (c (S n)) |}.
457
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
458
  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
459
  Definition later_cofe_mixin : CofeMixin (later A).
460 461
  Proof.
    split.
462
    - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
463
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
464
    - intros [|n]; [by split|split]; unfold dist, later_dist.
465 466
      + by intros [x].
      + by intros [x] [y].
467
      + by intros [x] [y] [z] ??; trans y.
468
    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
470
  Qed.
471
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
472 473
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
474
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
475
  Proof. by intros x y. Qed.
476
End later.
477 478 479 480

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
481
  Next (f (later_car x)).
482 483 484 485 486 487 488 489 490
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.
491 492 493
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.
494 495 496
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).
497
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
498

499 500 501
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)
502
|}.
503 504 505 506
Next Obligation.
  intros F A1 A2 B1 B2 n fg fg' ?.
  by apply (contractive_ne laterC_map), cFunctor_ne.
Qed.
507
Next Obligation.
508 509 510 511 512 513 514 515
  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.

516
Instance laterCF_contractive F : cFunctorContractive (laterCF F).
517
Proof.
518
  intros A1 A2 B1 B2 n fg fg' Hfg.
519
  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
520
Qed.