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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
95 96
Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption.

97
(** Discrete COFEs and Timeless elements *)
Ralf Jung's avatar
Ralf Jung committed
98
(* TODO: On paper, We called these "discrete elements". I think that makes
Ralf Jung's avatar
Ralf Jung committed
99
   more sense. *)
100 101
Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x {0} y  x  y.
Arguments timeless {_ _ _} _ {_} _ _.
102 103
Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.

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

153 154 155 156 157
  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.
158 159
  Lemma timeless_iff n (x : A) `{!Timeless x} y : x  y  x {n} y.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
    split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
161
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163
End cofe.

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

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

Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A  A)
184
  `{!Contractive f} : A := compl (fixpoint_chain f).
185 186 187
Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
Definition fixpoint {A AiH} f {Hf} := proj1_sig fixpoint_aux A AiH f Hf.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
188 189

Section fixpoint.
190
  Context {A : cofeT} `{Inhabited A} (f : A  A) `{!Contractive f}.
191
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  Proof.
193 194
    apply equiv_dist=>n.
    rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
195
    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
  Qed.
197
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
198
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  Proof.
200
    intros Hfg. rewrite fixpoint_eq /fixpoint_def
Robbert Krebbers's avatar
Robbert Krebbers committed
201
      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
202 203
    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
204
  Qed.
205 206
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
207 208 209
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.

210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
(** Function space *)
Definition cofe_fun (A : Type) (B : cofeT) := A  B.

Section cofe_fun.
  Context {A : Type} {B : cofeT}.
  Instance cofe_fun_equiv : Equiv (cofe_fun A B) := λ f g,  x, f x  g x.
  Instance cofe_fun_dist : Dist (cofe_fun A B) := λ n f g,  x, f x {n} g x.
  Program Definition cofe_fun_chain `(c : chain (cofe_fun 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_fun_compl : Compl (cofe_fun A B) := λ c x,
    compl (cofe_fun_chain c x).
  Definition cofe_fun_cofe_mixin : CofeMixin (cofe_fun A B).
  Proof.
    split.
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
    - intros n; split.
      + by intros f x.
      + by intros f g ? x.
      + by intros f g h ?? x; trans (g x).
    - by intros n f g ? x; apply dist_S.
    - intros n c x. apply (conv_compl n (cofe_fun_chain c x)).
  Qed.
  Canonical Structure cofe_funC := CofeT (cofe_fun A B) cofe_fun_cofe_mixin.
End cofe_fun.

Arguments cofe_funC : clear implicits.
Notation "A -c> B" :=
  (cofe_funC A B) (at level 99, B at level 200, right associativity).
Instance cofe_fun_inhabited {A} {B : cofeT} `{Inhabited B} :
  Inhabited (A -c> B) := populate (λ _, inhabitant).

243 244
(** Non-expansive function space *)
Record cofe_mor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247 248
  cofe_mor_car :> A  B;
  cofe_mor_ne n : Proper (dist n ==> dist n) cofe_mor_car
}.
Arguments CofeMor {_ _} _ {_}.
249
Add Printing Constructor cofe_mor.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
Existing Instance cofe_mor_ne.

252 253 254 255
Notation "'λne' x .. y , t" :=
  (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
  (at level 200, x binder, y binder, right associativity).

256 257
Section cofe_mor.
  Context {A B : cofeT}.
258
  Global Instance cofe_mor_proper (f : cofe_mor A B) : Proper (() ==> ()) f.
259
  Proof. apply ne_proper, cofe_mor_ne. Qed.
260 261 262 263
  Instance cofe_mor_equiv : Equiv (cofe_mor A B) := λ f g,  x, f x  g x.
  Instance cofe_mor_dist : Dist (cofe_mor A B) := λ n f g,  x, f x {n} g x.
  Program Definition cofe_mor_chain `(c : chain (cofe_mor A B))
    (x : A) : chain B := {| chain_car n := c n x |}.
264
  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
265 266
  Program Instance cofe_mor_compl : Compl (cofe_mor A B) := λ c,
    {| cofe_mor_car x := compl (cofe_mor_chain c x) |}.
267
  Next Obligation.
268 269
    intros c n x y Hx. by rewrite (conv_compl n (cofe_mor_chain c x))
      (conv_compl n (cofe_mor_chain c y)) /= Hx.
270
  Qed.
271
  Definition cofe_mor_cofe_mixin : CofeMixin (cofe_mor A B).
272 273
  Proof.
    split.
274
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
Robbert Krebbers's avatar
Robbert Krebbers committed
275
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
276
    - intros n; split.
277 278
      + by intros f x.
      + by intros f g ? x.
279
      + by intros f g h ?? x; trans (g x).
280
    - by intros n f g ? x; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
    - intros n c x; simpl.
282
      by rewrite (conv_compl n (cofe_mor_chain c x)) /=.
283
  Qed.
284
  Canonical Structure cofe_morC := CofeT (cofe_mor A B) cofe_mor_cofe_mixin.
285 286 287 288 289 290

  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 _.
291
  Lemma cofe_mor_ext (f g : cofe_mor A B) : f  g   x, f x  g x.
292 293 294
  Proof. done. Qed.
End cofe_mor.

295
Arguments cofe_morC : clear implicits.
296
Notation "A -n> B" :=
297
  (cofe_morC A B) (at level 99, B at level 200, right associativity).
298 299
Instance cofe_mor_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (λne _, inhabitant).
Robbert Krebbers's avatar
Robbert Krebbers committed
300

301
(** Identity and composition and constant function *)
Robbert Krebbers's avatar
Robbert Krebbers committed
302 303
Definition cid {A} : A -n> A := CofeMor id.
Instance: Params (@cid) 1.
304 305
Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x).
Instance: Params (@cconst) 2.
306

Robbert Krebbers's avatar
Robbert Krebbers committed
307 308 309 310 311
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 :
312
  f1 {n} f2  g1 {n} g2  f1  g1 {n} f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
314

Ralf Jung's avatar
Ralf Jung committed
315
(* Function space maps *)
316
Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
Ralf Jung's avatar
Ralf Jung committed
317
  (h : A -n> B) : A' -n> B' := g  h  f.
318
Instance cofe_mor_map_ne {A A' B B'} n :
Ralf Jung's avatar
Ralf Jung committed
319
  Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B').
320
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Ralf Jung's avatar
Ralf Jung committed
321

322
Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
Ralf Jung's avatar
Ralf Jung committed
323
  (A -n> B) -n> (A' -n>  B') := CofeMor (cofe_mor_map f g).
324
Instance cofe_morC_map_ne {A A' B B'} n :
Ralf Jung's avatar
Ralf Jung committed
325 326 327
  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.
328
  by repeat apply ccompose_ne.
Ralf Jung's avatar
Ralf Jung committed
329 330
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
331
(** unit *)
332 333 334 335 336
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.
337
  Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin.
338
  Global Instance unit_discrete_cofe : Discrete unitC.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
  Proof. done. Qed.
340
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
341 342

(** Product *)
343 344 345 346 347 348 349 350 351 352 353 354 355
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.
356
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
357
      rewrite !equiv_dist; naive_solver.
358 359
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361
    - intros n c; split. apply (conv_compl n (chain_map fst c)).
      apply (conv_compl n (chain_map snd c)).
362
  Qed.
363
  Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
364 365 366
  Global Instance prod_timeless (x : A * B) :
    Timeless (x.1)  Timeless (x.2)  Timeless x.
  Proof. by intros ???[??]; split; apply (timeless _). Qed.
367 368
  Global Instance prod_discrete_cofe : Discrete A  Discrete B  Discrete prodC.
  Proof. intros ?? [??]; apply _. Qed.
369 370 371 372 373 374
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
375 376 377 378 379 380 381 382 383
  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.

384 385
(** Functors *)
Structure cFunctor := CFunctor {
386
  cFunctor_car : cofeT  cofeT  cofeT;
387 388
  cFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
389 390
  cFunctor_ne {A1 A2 B1 B2} n :
    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
391 392 393 394 395 396
  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)
}.
397
Existing Instance cFunctor_ne.
398 399
Instance: Params (@cFunctor_map) 5.

400 401 402
Delimit Scope cFunctor_scope with CF.
Bind Scope cFunctor_scope with cFunctor.

403 404 405
Class cFunctorContractive (F : cFunctor) :=
  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).

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

413
Instance constCF_contractive B : cFunctorContractive (constCF B).
414
Proof. rewrite /cFunctorContractive; apply _. Qed.
415 416 417 418 419

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

420 421 422 423 424
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)
|}.
425 426 427
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
Qed.
428 429 430 431 432 433
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.

434 435 436 437 438 439 440 441
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
442
Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
443
  cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
Ralf Jung's avatar
Ralf Jung committed
444 445 446
  cFunctor_map A1 A2 B1 B2 fg :=
    cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
|}.
447 448 449 450
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
451
Next Obligation.
452 453
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
454 455
Qed.
Next Obligation.
456 457
  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
458 459
Qed.

460 461 462 463 464 465 466 467
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550
(** Sum *)
Section sum.
  Context {A B : cofeT}.

  Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
  Global Instance inl_ne : Proper (dist n ==> dist n) (@inl A B) := _.
  Global Instance inr_ne : Proper (dist n ==> dist n) (@inr A B) := _.
  Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
  Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.

  Program Definition inl_chain (c : chain (A + B)) (a : A) : chain A :=
    {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
  Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
  Program Definition inr_chain (c : chain (A + B)) (b : B) : chain B :=
    {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
  Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.

  Instance sum_compl : Compl (A + B) := λ c,
    match c 0 with
    | inl a => inl (compl (inl_chain c a))
    | inr b => inr (compl (inr_chain c b))
    end.

  Definition sum_cofe_mixin : CofeMixin (A + B).
  Proof.
    split.
    - intros x y; split=> Hx.
      + destruct Hx=> n; constructor; by apply equiv_dist.
      + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
    - apply _.
    - destruct 1; constructor; by apply dist_S.
    - intros n c; rewrite /compl /sum_compl.
      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
      + rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
      + rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
  Qed.
  Canonical Structure sumC : cofeT := CofeT (A + B) sum_cofe_mixin.

  Global Instance inl_timeless (x : A) : Timeless x  Timeless (inl x).
  Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
  Global Instance inr_timeless (y : B) : Timeless y  Timeless (inr y).
  Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
  Global Instance sum_discrete_cofe : Discrete A  Discrete B  Discrete sumC.
  Proof. intros ?? [?|?]; apply _. Qed.
End sum.

Arguments sumC : clear implicits.
Typeclasses Opaque sum_dist.

Instance sum_map_ne {A A' B B' : cofeT} n :
  Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
           dist n ==> dist n) (@sum_map A A' B B').
Proof.
  intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg].
Qed.
Definition sumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
  sumC A B -n> sumC A' B' := CofeMor (sum_map f g).
Instance sumC_map_ne {A A' B B'} n :
  Proper (dist n ==> dist n ==> dist n) (@sumC_map A A' B B').
Proof. intros f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.

Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {|
  cFunctor_car A B := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
  cFunctor_map A1 A2 B1 B2 fg :=
    sumC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
|}.
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply sumC_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.

Instance sumCF_contractive F1 F2 :
  cFunctorContractive F1  cFunctorContractive F2 
  cFunctorContractive (sumCF F1 F2).
Proof.
  intros ?? A1 A2 B1 B2 n ???;
    by apply sumC_map_ne; apply cFunctor_contractive.
Qed.

551 552 553
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
554
  Instance discrete_dist : Dist A := λ n x y, x  y.
555
  Instance discrete_compl : Compl A := λ c, c 0.
556
  Definition discrete_cofe_mixin : CofeMixin A.
557 558
  Proof.
    split.
559 560 561
    - intros x y; split; [done|intros Hn; apply (Hn 0)].
    - done.
    - done.
562 563
    - intros n c. rewrite /compl /discrete_compl /=;
      symmetry; apply (chain_cauchy c 0 n). omega.
564 565 566
  Qed.
End discrete_cofe.

567 568 569 570 571 572 573 574
Notation discreteC A := (CofeT A discrete_cofe_mixin).
Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)).

Instance discrete_discrete_cofe `{Equiv A, @Equivalence A ()} :
  Discrete (discreteC A).
Proof. by intros x y. Qed.
Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
Proof. by intros x y. Qed.
575

Robbert Krebbers's avatar
Robbert Krebbers committed
576 577
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
578

579 580 581 582
(* Option *)
Section option.
  Context {A : cofeT}.

583
  Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
584
  Lemma dist_option_Forall2 n mx my : mx {n} my  option_Forall2 (dist n) mx my.
585
  Proof. done. Qed.
586 587

  Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
588
    {| chain_car n := from_option id x (c n) |}.
589 590 591 592 593 594 595 596 597 598
  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
  Instance option_compl : Compl (option A) := λ c,
    match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.

  Definition option_cofe_mixin : CofeMixin (option A).
  Proof.
    split.
    - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
      intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
      by intros n; feed inversion (Hxy n).
599
    - apply _.
600 601 602 603 604 605 606 607 608 609 610 611 612 613 614
    - destruct 1; constructor; by apply dist_S.
    - intros n c; rewrite /compl /option_compl.
      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
      rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
  Qed.
  Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
  Global Instance option_discrete : Discrete A  Discrete optionC.
  Proof. destruct 2; constructor; by apply (timeless _). Qed.

  Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
  Proof. by constructor. Qed.
  Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
  Proof. destruct 1; split; eauto. Qed.
  Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
  Proof. by inversion_clear 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
615 616 617
  Global Instance from_option_ne {B} (R : relation B) (f : A  B) n :
    Proper (dist n ==> R) f  Proper (R ==> dist n ==> R) (from_option f).
  Proof. destruct 3; simpl; auto. Qed.
618 619 620 621 622

  Global Instance None_timeless : Timeless (@None A).
  Proof. inversion_clear 1; constructor. Qed.
  Global Instance Some_timeless x : Timeless x  Timeless (Some x).
  Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
623 624 625 626 627 628 629 630 631 632 633 634 635

  Lemma dist_None n mx : mx {n} None  mx = None.
  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
  Lemma dist_Some_inv_l n mx my x :
    mx {n} my  mx = Some x   y, my = Some y  x {n} y.
  Proof. destruct 1; naive_solver. Qed.
  Lemma dist_Some_inv_r n mx my y :
    mx {n} my  my = Some y   x, mx = Some x  x {n} y.
  Proof. destruct 1; naive_solver. Qed.
  Lemma dist_Some_inv_l' n my x : Some x {n} my   x', Some x' = my  x {n} x'.
  Proof. intros ?%(dist_Some_inv_l _ _ _ x); naive_solver. Qed.
  Lemma dist_Some_inv_r' n mx y : mx {n} Some y   y', mx = Some y'  y {n} y'.
  Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed.
636 637
End option.

638
Typeclasses Opaque option_dist.
639 640
Arguments optionC : clear implicits.

Robbert Krebbers's avatar
Robbert Krebbers committed
641 642 643
Instance option_fmap_ne {A B : cofeT} n:
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
Proof. intros f f' Hf ?? []; constructor; auto. Qed.
644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
  CofeMor (fmap f : optionC A  optionC B).
Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.

Program Definition optionCF (F : cFunctor) : cFunctor := {|
  cFunctor_car A B := optionC (cFunctor_car F A B);
  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
|}.
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
  intros F A B x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
Qed.

Instance optionCF_contractive F :
  cFunctorContractive F  cFunctorContractive (optionCF F).
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
Qed.

671
(** Later *)
672
Inductive later (A : Type) : Type := Next { later_car : A }.
673
Add Printing Constructor later.
674
Arguments Next {_} _.
675
Arguments later_car {_} _.
676
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
677
Proof. by destruct x. Qed.
678

679
Section later.
680 681 682
  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,
683
    match n with 0 => True | S n => later_car x {n} later_car y end.
684
  Program Definition later_chain (c : chain (later A)) : chain A :=
685
    {| chain_car n := later_car (c (S n)) |}.
686
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
687
  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
688
  Definition later_cofe_mixin : CofeMixin (later A).
689 690
  Proof.
    split.
691 692
    - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
693
    - intros [|n]; [by split|split]; unfold dist, later_dist.
694 695
      + by intros [x].
      + by intros [x] [y].
696
      + by intros [x] [y] [z] ??; trans y.
697
    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
698
    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
699
  Qed.
700
  Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin.
701 702
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
703
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
704
  Proof. by intros x y. Qed.
705
End later.
706 707 708 709

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
710
  Next (f (later_car x)).
711 712 713 714 715 716 717 718 719
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.
720 721 722
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.
723 724 725
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).
726
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
727

728 729 730
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)
731
|}.
732 733 734 735
Next Obligation.
  intros F A1 A2 B1 B2 n fg fg' ?.
  by apply (contractive_ne laterC_map), cFunctor_ne.
Qed.
736
Next Obligation.
737 738 739 740 741 742 743 744
  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.

745
Instance laterCF_contractive F : cFunctorContractive (laterCF F).
746
Proof.
747
  intros A1 A2 B1 B2 n fg fg' Hfg.
748
  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
749
Qed.
750 751 752 753

(** Notation for writing functors *)
Notation "∙" := idCF : cFunctor_scope.
Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
754
Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
755
Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
756 757
Notation "▶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
Coercion constCF : cofeT >-> cFunctor.