cofe.v 21 KB
Newer Older
1
From iris.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
(** Discrete COFEs and Timeless elements *)
Ralf Jung's avatar
Ralf Jung committed
92
(* TODO: On paper, We called these "discrete elements". I think that makes
93
   more sense. *)
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's avatar
Robbert Krebbers committed
98 99
(** General properties *)
Section cofe.
100 101
  Context {A : cofeT}.
  Implicit Types x y : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104
  Global Instance cofe_equivalence : Equivalence (() : relation A).
  Proof.
    split.
105 106
    - by intros x; rewrite equiv_dist.
    - by intros x y; rewrite !equiv_dist.
107
    - by intros x y z; rewrite !equiv_dist; intros; trans y.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Qed.
109
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
112 113
    - by trans x1; [|trans y1].
    - by trans x2; [|trans y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  Qed.
115
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  Proof.
117
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119 120
  Qed.
  Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.
121
  Lemma dist_le n n' x y : x {n} y  n'  n  x {n'} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
  Proof. induction 2; eauto using dist_S. Qed.
123 124
  Lemma dist_le' n n' x y : n'  n  x {n} y  x {n'} y.
  Proof. intros; eauto using dist_le. Qed.
125
  Instance ne_proper {B : cofeT} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
128
  Instance ne_proper_2 {B C : cofeT} (f : A  B  C)
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132
    `{! n, Proper (dist n ==> dist n ==> dist n) f} :
    Proper (() ==> () ==> ()) f | 100.
  Proof.
     unfold Proper, respectful; setoid_rewrite equiv_dist.
133
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
134
  Qed.
135
  Lemma contractive_S {B : cofeT} (f : A  B) `{!Contractive f} n x y :
136 137
    x {n} y  f x {S n} f y.
  Proof. eauto using contractive, dist_le with omega. Qed.
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.
141
  Global Instance contractive_ne {B : cofeT} (f : A  B) `{!Contractive f} n :
142
    Proper (dist n ==> dist n) f | 100.
143
  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
144
  Global Instance contractive_proper {B : cofeT} (f : A  B) `{!Contractive f} :
145
    Proper (() ==> ()) f | 100 := _.
146

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.
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's avatar
Robbert Krebbers committed
157 158
End cofe.

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's avatar
Robbert Krebbers committed
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) |}.
166
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
167

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

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

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

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

248 249 250
End cofe_mor.

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

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

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

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

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

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

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

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

352 353 354
Delimit Scope cFunctor_scope with CF.
Bind Scope cFunctor_scope with cFunctor.

355 356 357
Class cFunctorContractive (F : cFunctor) :=
  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).

358 359 360 361 362 363 364
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.

365
Instance constCF_contractive B : cFunctorContractive (constCF B).
366
Proof. rewrite /cFunctorContractive; apply _. Qed.
367 368 369 370 371

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

372 373 374 375 376
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)
|}.
377 378 379
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
Qed.
380 381 382 383 384 385
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.

386 387 388 389 390 391 392 393
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.

394 395 396 397 398
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)
|}.
399 400 401 402
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.
403
Next Obligation.
404 405
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
406 407
Qed.
Next Obligation.
408 409
  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.
410 411
Qed.

412 413 414 415 416 417 418 419
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.

420

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

Robbert Krebbers's avatar
Robbert Krebbers committed
441
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
442 443 444
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.

445 446
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
447

448
(** Later *)
449
Inductive later (A : Type) : Type := Next { later_car : A }.
450
Add Printing Constructor later.
451
Arguments Next {_} _.
452
Arguments later_car {_} _.
453
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
Proof. by destruct x. Qed.
455

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

Arguments laterC : clear implicits.

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

505 506 507
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)
508
|}.
509 510 511 512
Next Obligation.
  intros F A1 A2 B1 B2 n fg fg' ?.
  by apply (contractive_ne laterC_map), cFunctor_ne.
Qed.
513
Next Obligation.
514 515 516 517 518 519 520 521
  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.

522
Instance laterCF_contractive F : cFunctorContractive (laterCF F).
523
Proof.
524
  intros A1 A2 B1 B2 n fg fg' Hfg.
525
  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
526
Qed.
527 528 529 530 531 532 533

(** Notation for writing functors *)
Notation "∙" := idCF : cFunctor_scope.
Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
Notation "( F1 , F2 , .. , Fn )" := (prodCF .. (prodCF F1%CF F2%CF) .. Fn%CF) : cFunctor_scope.
Notation "▶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
Coercion constCF : cofeT >-> cFunctor.