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

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

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

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

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

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

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

Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A  A)
180
  `{!Contractive f} : A := compl (fixpoint_chain f).
181 182 183
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
184 185

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

(** Function space *)
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Record cofeMor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210 211 212 213 214
  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.

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

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

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

259
(** Identity and composition and constant function *)
Robbert Krebbers's avatar
Robbert Krebbers committed
260 261
Definition cid {A} : A -n> A := CofeMor id.
Instance: Params (@cid) 1.
262 263
Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x).
Instance: Params (@cconst) 2.
264

Robbert Krebbers's avatar
Robbert Krebbers committed
265 266 267 268 269
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 :
270
  f1 {n} f2  g1 {n} g2  f1  g1 {n} f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
272

Ralf Jung's avatar
Ralf Jung committed
273
(* Function space maps *)
274
Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
Ralf Jung's avatar
Ralf Jung committed
275
  (h : A -n> B) : A' -n> B' := g  h  f.
276
Instance cofe_mor_map_ne {A A' B B'} n :
Ralf Jung's avatar
Ralf Jung committed
277
  Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B').
278
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Ralf Jung's avatar
Ralf Jung committed
279

280
Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
Ralf Jung's avatar
Ralf Jung committed
281
  (A -n> B) -n> (A' -n>  B') := CofeMor (cofe_mor_map f g).
282
Instance cofe_morC_map_ne {A A' B B'} n :
Ralf Jung's avatar
Ralf Jung committed
283 284 285
  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.
286
  by repeat apply ccompose_ne.
Ralf Jung's avatar
Ralf Jung committed
287 288
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
289
(** unit *)
290 291 292 293 294
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.
295
  Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin.
296
  Global Instance unit_discrete_cofe : Discrete unitC.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Proof. done. Qed.
298
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
299 300

(** Product *)
301 302 303 304 305 306 307 308 309 310 311 312 313
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.
314
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
315
      rewrite !equiv_dist; naive_solver.
316 317
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
318 319
    - intros n c; split. apply (conv_compl n (chain_map fst c)).
      apply (conv_compl n (chain_map snd c)).
320
  Qed.
321
  Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
322 323 324
  Global Instance pair_timeless (x : A) (y : B) :
    Timeless x  Timeless y  Timeless (x,y).
  Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
325 326
  Global Instance prod_discrete_cofe : Discrete A  Discrete B  Discrete prodC.
  Proof. intros ?? [??]; apply _. Qed.
327 328 329 330 331 332
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
333 334 335 336 337 338 339 340 341
  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.

342 343
(** Functors *)
Structure cFunctor := CFunctor {
344
  cFunctor_car : cofeT  cofeT  cofeT;
345 346
  cFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
347 348
  cFunctor_ne {A1 A2 B1 B2} n :
    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
349 350 351 352 353 354
  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)
}.
355
Existing Instance cFunctor_ne.
356 357
Instance: Params (@cFunctor_map) 5.

358 359 360
Delimit Scope cFunctor_scope with CF.
Bind Scope cFunctor_scope with cFunctor.

361 362 363
Class cFunctorContractive (F : cFunctor) :=
  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).

364 365 366 367 368 369 370
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.

371
Instance constCF_contractive B : cFunctorContractive (constCF B).
372
Proof. rewrite /cFunctorContractive; apply _. Qed.
373 374 375 376 377

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

378 379 380 381 382
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)
|}.
383 384 385
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
Qed.
386 387 388 389 390 391
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.

392 393 394 395 396 397 398 399
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
400 401 402 403 404
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)
|}.
405 406 407 408
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
409
Next Obligation.
410 411
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
412 413
Qed.
Next Obligation.
414 415
  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
416 417
Qed.

418 419 420 421 422 423 424 425
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
426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 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
(** 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.

509 510 511
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
512
  Instance discrete_dist : Dist A := λ n x y, x  y.
513
  Instance discrete_compl : Compl A := λ c, c 0.
514
  Definition discrete_cofe_mixin : CofeMixin A.
515 516
  Proof.
    split.
517 518 519
    - intros x y; split; [done|intros Hn; apply (Hn 0)].
    - done.
    - done.
520 521
    - intros n c. rewrite /compl /discrete_compl /=;
      symmetry; apply (chain_cauchy c 0 n). omega.
522 523 524
  Qed.
End discrete_cofe.

525 526 527 528 529 530 531 532
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.
533

Robbert Krebbers's avatar
Robbert Krebbers committed
534 535
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
536

537 538 539 540
(* Option *)
Section option.
  Context {A : cofeT}.

541
  Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
542
  Lemma dist_option_Forall2 n mx my : mx {n} my  option_Forall2 (dist n) mx my.
543
  Proof. done. Qed.
544 545

  Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
546
    {| chain_car n := from_option id x (c n) |}.
547 548 549 550 551 552 553 554 555 556
  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).
557
    - apply _.
558 559 560 561 562 563 564 565 566 567 568 569 570 571 572
    - 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
573 574 575
  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.
576 577 578 579 580

  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.
581 582 583 584 585 586 587 588 589 590 591 592 593

  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.
594 595
End option.

596
Typeclasses Opaque option_dist.
597 598
Arguments optionC : clear implicits.

Robbert Krebbers's avatar
Robbert Krebbers committed
599 600 601
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.
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
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.

629
(** Later *)
630
Inductive later (A : Type) : Type := Next { later_car : A }.
631
Add Printing Constructor later.
632
Arguments Next {_} _.
633
Arguments later_car {_} _.
634
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
Proof. by destruct x. Qed.
636

637
Section later.
638 639 640
  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,
641
    match n with 0 => True | S n => later_car x {n} later_car y end.
642
  Program Definition later_chain (c : chain (later A)) : chain A :=
643
    {| chain_car n := later_car (c (S n)) |}.
644
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
645
  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
646
  Definition later_cofe_mixin : CofeMixin (later A).
647 648
  Proof.
    split.
649 650
    - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
651
    - intros [|n]; [by split|split]; unfold dist, later_dist.
652 653
      + by intros [x].
      + by intros [x] [y].
654
      + by intros [x] [y] [z] ??; trans y.
655
    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
656
    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
657
  Qed.
658
  Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin.
659 660
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
661
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
662
  Proof. by intros x y. Qed.
663
End later.
664 665 666 667

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
668
  Next (f (later_car x)).
669 670 671 672 673 674 675 676 677
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.
678 679 680
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.
681 682 683
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).
684
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
685

686 687 688
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)
689
|}.
690 691 692 693
Next Obligation.
  intros F A1 A2 B1 B2 n fg fg' ?.
  by apply (contractive_ne laterC_map), cFunctor_ne.
Qed.
694
Next Obligation.
695 696 697 698 699 700 701 702
  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.

703
Instance laterCF_contractive F : cFunctorContractive (laterCF F).
704
Proof.
705
  intros A1 A2 B1 B2 n fg fg' Hfg.
706
  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
707
Qed.
708 709 710 711

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