ofe.v 31.7 KB
Newer Older
1
From iris.algebra Require Export base.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

3
(** This files defines (a shallow embedding of) the category of OFEs:
4
5
6
7
8
9
10
11
    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.
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
(** Unbundeled version *)
Class Dist A := dist : nat  relation A.
14
Instance: Params (@dist) 3.
15
16
Notation "x ≡{ n }≡ y" := (dist n x y)
  (at level 70, n at next level, format "x  ≡{ n }≡  y").
17
Hint Extern 0 (_ {_} _) => reflexivity.
18
Hint Extern 0 (_ {_} _) => symmetry; assumption.
19
20
21

Tactic Notation "cofe_subst" ident(x) :=
  repeat match goal with
22
  | _ => progress simplify_eq/=
23
24
25
26
  | 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" :=
27
  repeat match goal with
28
  | _ => progress simplify_eq/=
29
30
  | 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
31
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

33
Record OfeMixin A `{Equiv A, Dist A} := {
34
  mixin_equiv_dist x y : x  y   n, x {n} y;
35
  mixin_dist_equivalence n : Equivalence (dist n);
36
  mixin_dist_S n x y : x {S n} y  x {n} y
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
39
}.

(** Bundeled version *)
40
41
42
43
44
Structure ofeT := OfeT' {
  ofe_car :> Type;
  ofe_equiv : Equiv ofe_car;
  ofe_dist : Dist ofe_car;
  ofe_mixin : OfeMixin ofe_car;
45
  _ : Type
Robbert Krebbers's avatar
Robbert Krebbers committed
46
}.
47
48
49
50
51
52
53
54
55
Arguments OfeT' _ {_ _} _ _.
Notation OfeT A m := (OfeT' A m A).
Add Printing Constructor ofeT.
Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
Arguments ofe_car : simpl never.
Arguments ofe_equiv : simpl never.
Arguments ofe_dist : simpl never.
Arguments ofe_mixin : simpl never.
56
57

(** Lifting properties from the mixin *)
58
59
Section ofe_mixin.
  Context {A : ofeT}.
60
  Implicit Types x y : A.
61
  Lemma equiv_dist x y : x  y   n, x {n} y.
62
  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
63
  Global Instance dist_equivalence n : Equivalence (@dist A _ n).
64
  Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
65
  Lemma dist_S n x y : x {S n} y  x {n} y.
66
67
  Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
End ofe_mixin.
68

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

71
(** Discrete COFEs and Timeless elements *)
Ralf Jung's avatar
Ralf Jung committed
72
(* TODO: On paper, We called these "discrete elements". I think that makes
Ralf Jung's avatar
Ralf Jung committed
73
   more sense. *)
74
75
Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x {0} y  x  y.
Arguments timeless {_ _ _} _ {_} _ _.
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.

(** OFEs with a completion *)
Record chain (A : ofeT) := {
  chain_car :> nat  A;
  chain_cauchy n i : n  i  chain_car i {n} chain_car n
}.
Arguments chain_car {_} _ _.
Arguments chain_cauchy {_} _ _ _ _.

Notation Compl A := (chain A%type  A).
Class Cofe (A : ofeT) := {
  compl : Compl A;
  conv_compl n c : compl c {n} c n;
}.
Arguments compl : simpl never.
92

Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
(** General properties *)
Section cofe.
95
  Context {A : ofeT}.
96
  Implicit Types x y : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
99
  Global Instance cofe_equivalence : Equivalence (() : relation A).
  Proof.
    split.
100
101
    - by intros x; rewrite equiv_dist.
    - by intros x y; rewrite !equiv_dist.
102
    - by intros x y z; rewrite !equiv_dist; intros; trans y.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  Qed.
104
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
107
108
    - by trans x1; [|trans y1].
    - by trans x2; [|trans y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  Qed.
110
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
115
  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
116
  Lemma dist_le n n' x y : x {n} y  n'  n  x {n'} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  Proof. induction 2; eauto using dist_S. Qed.
118
119
  Lemma dist_le' n n' x y : n'  n  x {n} y  x {n'} y.
  Proof. intros; eauto using dist_le. Qed.
120
  Instance ne_proper {B : ofeT} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
    `{! 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.
123
  Instance ne_proper_2 {B C : ofeT} (f : A  B  C)
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
127
    `{! 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
128
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Qed.
130

131
  Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c {n} c (S n).
132
133
134
135
  Proof.
    transitivity (c n); first by apply conv_compl. symmetry.
    apply chain_cauchy. omega.
  Qed.
136
137
  Lemma timeless_iff n (x : A) `{!Timeless x} y : x  y  x {n} y.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
    split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
139
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
End cofe.

142
143
144
145
(** Contractive functions *)
Class Contractive {A B : ofeT} (f : A  B) :=
  contractive n x y : ( i, i < n  x {i} y)  f x {n} f y.

146
Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
147
148
Proof. by intros n y1 y2. Qed.

149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
Section contractive.
  Context {A B : ofeT} (f : A  B) `{!Contractive f}.
  Implicit Types x y : A.

  Lemma contractive_0 x y : f x {0} f y.
  Proof. eauto using contractive with omega. Qed.
  Lemma contractive_S n x y : x {n} y  f x {S n} f y.
  Proof. eauto using contractive, dist_le with omega. Qed.

  Global Instance contractive_ne n : Proper (dist n ==> dist n) f | 100.
  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
  Global Instance contractive_proper : Proper (() ==> ()) f | 100.
  Proof. apply (ne_proper _). Qed.
End contractive.

Robbert Krebbers's avatar
Robbert Krebbers committed
164
(** Mapping a chain *)
165
Program Definition chain_map {A B : ofeT} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
    `{! n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
  {| chain_car n := f (c n) |}.
168
Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
169

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

180
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A  A)
181
  `{!Contractive f} : A := compl (fixpoint_chain f).
182
Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
183
Definition fixpoint {A AC AiH} f {Hf} := proj1_sig fixpoint_aux A AC AiH f Hf.
184
Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186

Section fixpoint.
187
  Context `{Cofe A, Inhabited A} (f : A  A) `{!Contractive f}.
188

189
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  Proof.
191
192
    apply equiv_dist=>n.
    rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
193
    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
  Qed.
195
196
197

  Lemma fixpoint_unique (x : A) : x  f x  x  fixpoint f.
  Proof.
198
199
200
    rewrite !equiv_dist=> Hx n. induction n as [|n IH]; simpl in *.
    - rewrite Hx fixpoint_unfold; eauto using contractive_0.
    - rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
201
202
  Qed.

203
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
204
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
  Proof.
206
    intros Hfg. rewrite fixpoint_eq /fixpoint_def
Robbert Krebbers's avatar
Robbert Krebbers committed
207
      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
208
209
    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
210
  Qed.
211
212
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.

216
(** Function space *)
217
(* We make [ofe_fun] a definition so that we can register it as a canonical
218
structure. *)
219
Definition ofe_fun (A : Type) (B : ofeT) := A  B.
220

221
222
223
224
225
Section ofe_fun.
  Context {A : Type} {B : ofeT}.
  Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g,  x, f x  g x.
  Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g,  x, f x {n} g x.
  Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
226
227
228
229
230
231
232
233
234
235
  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.
  Qed.
236
  Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
237

238
239
240
241
242
243
244
245
246
  Program Definition ofe_fun_chain `(c : chain ofe_funC)
    (x : A) : chain B := {| chain_car n := c n x |}.
  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
  Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
    { compl c x := compl (ofe_fun_chain c x) }.
  Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
End ofe_fun.

Arguments ofe_funC : clear implicits.
247
Notation "A -c> B" :=
248
249
  (ofe_funC A B) (at level 99, B at level 200, right associativity).
Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
250
251
  Inhabited (A -c> B) := populate (λ _, inhabitant).

252
(** Non-expansive function space *)
253
254
255
Record ofe_mor (A B : ofeT) : Type := CofeMor {
  ofe_mor_car :> A  B;
  ofe_mor_ne n : Proper (dist n ==> dist n) ofe_mor_car
Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
}.
Arguments CofeMor {_ _} _ {_}.
258
259
Add Printing Constructor ofe_mor.
Existing Instance ofe_mor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
260

261
262
263
264
Notation "'λne' x .. y , t" :=
  (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
  (at level 200, x binder, y binder, right associativity).

265
266
267
268
269
270
271
Section ofe_mor.
  Context {A B : ofeT}.
  Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper (() ==> ()) f.
  Proof. apply ne_proper, ofe_mor_ne. Qed.
  Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g,  x, f x  g x.
  Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g,  x, f x {n} g x.
  Definition ofe_mor_ofe_mixin : OfeMixin (ofe_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.
281
  Qed.
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
  Canonical Structure ofe_morC := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.

  Program Definition ofe_mor_chain (c : chain ofe_morC)
    (x : A) : chain B := {| chain_car n := c n x |}.
  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
  Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morC := λ c,
    {| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
  Next Obligation.
    intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
      (conv_compl n (ofe_mor_chain c y)) /= Hx.
  Qed.
  Global Program Instance ofe_more_cofe `{Cofe B} : Cofe ofe_morC :=
    {| compl := ofe_mor_compl |}.
  Next Obligation.
    intros ? n c x; simpl.
    by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
  Qed.
299

300
301
  Global Instance ofe_mor_car_ne n :
    Proper (dist n ==> dist n ==> dist n) (@ofe_mor_car A B).
302
  Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
303
304
305
  Global Instance ofe_mor_car_proper :
    Proper (() ==> () ==> ()) (@ofe_mor_car A B) := ne_proper_2 _.
  Lemma ofe_mor_ext (f g : ofe_mor A B) : f  g   x, f x  g x.
306
  Proof. done. Qed.
307
End ofe_mor.
308

309
Arguments ofe_morC : clear implicits.
310
Notation "A -n> B" :=
311
312
  (ofe_morC A B) (at level 99, B at level 200, right associativity).
Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
313
  Inhabited (A -n> B) := populate (λne _, inhabitant).
Robbert Krebbers's avatar
Robbert Krebbers committed
314

315
(** Identity and composition and constant function *)
Robbert Krebbers's avatar
Robbert Krebbers committed
316
317
Definition cid {A} : A -n> A := CofeMor id.
Instance: Params (@cid) 1.
318
Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x).
319
Instance: Params (@cconst) 2.
320

Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
323
324
325
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 :
326
  f1 {n} f2  g1 {n} g2  f1  g1 {n} f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328

Ralf Jung's avatar
Ralf Jung committed
329
(* Function space maps *)
330
Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
Ralf Jung's avatar
Ralf Jung committed
331
  (h : A -n> B) : A' -n> B' := g  h  f.
332
333
Instance ofe_mor_map_ne {A A' B B'} n :
  Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B').
334
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Ralf Jung's avatar
Ralf Jung committed
335

336
337
338
339
Definition ofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
  (A -n> B) -n> (A' -n>  B') := CofeMor (ofe_mor_map f g).
Instance ofe_morC_map_ne {A A' B B'} n :
  Proper (dist n ==> dist n ==> dist n) (@ofe_morC_map A A' B B').
Ralf Jung's avatar
Ralf Jung committed
340
Proof.
341
  intros f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
342
  by repeat apply ccompose_ne.
Ralf Jung's avatar
Ralf Jung committed
343
344
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
345
(** unit *)
346
347
Section unit.
  Instance unit_dist : Dist unit := λ _ _ _, True.
348
  Definition unit_ofe_mixin : OfeMixin unit.
349
  Proof. by repeat split; try exists 0. Qed.
350
  Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
351

352
353
  Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
  Next Obligation. by repeat split; try exists 0. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
355

  Global Instance unit_discrete_cofe : Discrete unitC.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
  Proof. done. Qed.
357
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359

(** Product *)
360
Section product.
361
  Context {A B : ofeT}.
362
363
364
365
366
367

  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) := _.
368
  Definition prod_ofe_mixin : OfeMixin (A * B).
369
370
  Proof.
    split.
371
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
372
      rewrite !equiv_dist; naive_solver.
373
374
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
375
  Qed.
376
377
378
379
380
381
382
383
384
  Canonical Structure prodC : ofeT := OfeT (A * B) prod_ofe_mixin.

  Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodC :=
    { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
  Next Obligation.
    intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
    apply (conv_compl n (chain_map snd c)).
  Qed.

385
386
387
  Global Instance prod_timeless (x : A * B) :
    Timeless (x.1)  Timeless (x.2)  Timeless x.
  Proof. by intros ???[??]; split; apply (timeless _). Qed.
388
389
  Global Instance prod_discrete_cofe : Discrete A  Discrete B  Discrete prodC.
  Proof. intros ?? [??]; apply _. Qed.
390
391
392
393
394
End product.

Arguments prodC : clear implicits.
Typeclasses Opaque prod_dist.

395
Instance prod_map_ne {A A' B B' : ofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
396
397
398
399
400
401
402
403
404
  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.

405
406
(** Functors *)
Structure cFunctor := CFunctor {
407
  cFunctor_car : ofeT  ofeT  ofeT;
408
409
  cFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
410
411
  cFunctor_ne {A1 A2 B1 B2} n :
    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
412
  cFunctor_id {A B : ofeT} (x : cFunctor_car A B) :
413
414
415
416
417
    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)
}.
418
Existing Instance cFunctor_ne.
419
420
Instance: Params (@cFunctor_map) 5.

421
422
423
Delimit Scope cFunctor_scope with CF.
Bind Scope cFunctor_scope with cFunctor.

424
425
426
Class cFunctorContractive (F : cFunctor) :=
  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).

427
Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
428
429
Coercion cFunctor_diag : cFunctor >-> Funclass.

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

434
Instance constCF_contractive B : cFunctorContractive (constCF B).
435
Proof. rewrite /cFunctorContractive; apply _. Qed.
436
437
438
439
440

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

441
442
443
444
445
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)
|}.
446
447
448
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
Qed.
449
450
451
452
453
454
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.

455
456
457
458
459
460
461
462
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.

463
Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') n :
464
465
466
  Proper (dist n ==> dist n) (compose f : (A -c> B)  A -c> B').
Proof. intros g g' Hf x; simpl. by rewrite (Hf x). Qed.

467
Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
468
  @CofeMor (_ -c> _) (_ -c> _) (compose f) _.
469
470
Instance ofe_funC_map_ne {A B B'} n :
  Proper (dist n ==> dist n) (@ofe_funC_map A B B').
471
472
Proof. intros f f' Hf g x. apply Hf. Qed.

473
474
475
Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
  cFunctor_car A B := ofe_funC T (cFunctor_car F A B);
  cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (cFunctor_map F fg)
476
477
|}.
Next Obligation.
478
  intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne.
479
480
481
482
483
484
485
Qed.
Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed.
Next Obligation.
  intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
  by rewrite !cFunctor_compose.
Qed.

486
487
Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
  cFunctorContractive F  cFunctorContractive (ofe_funCF T F).
488
489
Proof.
  intros ?? A1 A2 B1 B2 n ???;
490
    by apply ofe_funC_map_ne; apply cFunctor_contractive.
491
492
Qed.

493
Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
494
  cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
Ralf Jung's avatar
Ralf Jung committed
495
  cFunctor_map A1 A2 B1 B2 fg :=
496
    ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
Ralf Jung's avatar
Ralf Jung committed
497
|}.
498
499
Next Obligation.
  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
500
  apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
501
Qed.
Ralf Jung's avatar
Ralf Jung committed
502
Next Obligation.
503
504
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
505
506
Qed.
Next Obligation.
507
508
  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
509
510
Qed.

511
Instance ofe_morCF_contractive F1 F2 :
512
  cFunctorContractive F1  cFunctorContractive F2 
513
  cFunctorContractive (ofe_morCF F1 F2).
514
515
Proof.
  intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
516
  apply ofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
517
518
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
519
520
(** Sum *)
Section sum.
521
  Context {A B : ofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
524
525
526
527
528

  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) := _.

529
530
531
532
533
534
535
536
537
538
539
540
  Definition sum_ofe_mixin : OfeMixin (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.
  Qed.
  Canonical Structure sumC : ofeT := OfeT (A + B) sum_ofe_mixin.

  Program Definition inl_chain (c : chain sumC) (a : A) : chain A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
    {| 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.
543
  Program Definition inr_chain (c : chain sumC) (b : B) : chain B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
544
545
546
    {| 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.

547
  Definition sum_compl `{Cofe A, Cofe B} : Compl sumC := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
548
549
550
551
    match c 0 with
    | inl a => inl (compl (inl_chain c a))
    | inr b => inr (compl (inr_chain c b))
    end.
552
553
554
555
556
557
558
  Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumC :=
    { compl := sum_compl }.
  Next Obligation.
    intros ?? n c; rewrite /compl /sum_compl.
    feed inversion (chain_cauchy c 0 n); first by 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
560
561
562
563
564
565
566
567
568
569
570
571
  Qed.

  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.

572
Instance sum_map_ne {A A' B B' : ofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
  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.

606
607
608
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
609
  Instance discrete_dist : Dist A := λ n x y, x  y.
610
  Definition discrete_ofe_mixin : OfeMixin A.
611
612
  Proof.
    split.
613
614
615
    - intros x y; split; [done|intros Hn; apply (Hn 0)].
    - done.
    - done.
616
617
618
619
620
621
622
  Qed.
  
  Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
    { compl c := c 0 }.
  Next Obligation.
    intros n c. rewrite /compl /=;
    symmetry; apply (chain_cauchy c 0 n). omega.
623
624
625
  Qed.
End discrete_cofe.

626
627
Notation discreteC A := (OfeT A discrete_ofe_mixin).
Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
628
629
630
631
632
633

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.
634

Robbert Krebbers's avatar
Robbert Krebbers committed
635
636
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
637

638
639
(* Option *)
Section option.
640
  Context {A : ofeT}.
641

642
  Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
643
  Lemma dist_option_Forall2 n mx my : mx {n} my  option_Forall2 (dist n) mx my.
644
  Proof. done. Qed.
645

646
  Definition option_ofe_mixin : OfeMixin (option A).
647
648
649
650
651
  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).
652
    - apply _.
653
654
    - destruct 1; constructor; by apply dist_S.
  Qed.
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
  Canonical Structure optionC := OfeT (option A) option_ofe_mixin.

  Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
    {| chain_car n := from_option id x (c n) |}.
  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
  Definition option_compl `{Cofe A} : Compl optionC := λ c,
    match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
  Global Program Instance option_cofe `{Cofe A} : Cofe optionC :=
    { compl := option_compl }.
  Next Obligation.
    intros ? n c; rewrite /compl /option_compl.
    feed inversion (chain_cauchy c 0 n); auto with lia; [].
    constructor. rewrite (conv_compl n (option_chain c _)) /=.
    destruct (c n); naive_solver.
  Qed.

671
672
673
674
675
676
677
678
679
  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
680
681
682
  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.
683
684
685
686
687

  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.
688
689
690
691
692
693
694
695
696
697
698
699
700

  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.
701
702
End option.

703
Typeclasses Opaque option_dist.
704
705
Arguments optionC : clear implicits.

706
Instance option_fmap_ne {A B : ofeT} n:
Robbert Krebbers's avatar
Robbert Krebbers committed
707
708
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
Proof. intros f f' Hf ?? []; constructor; auto. Qed.
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
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.

736
(** Later *)
737
Inductive later (A : Type) : Type := Next { later_car : A }.
738
Add Printing Constructor later.
739
Arguments Next {_} _.
740
Arguments later_car {_} _.
741

742
Section later.
743
  Context {A : ofeT}.
744
745
  Instance later_equiv : Equiv (later A) := λ x y, later_car x  later_car y.
  Instance later_dist : Dist (later A) := λ n x y,
746
    match n with 0 => True | S n => later_car x {n} later_car y end.
747
  Definition later_ofe_mixin : OfeMixin (later A).
748
749
  Proof.
    split.
750
751
    - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
752
    - intros [|n]; [by split|split]; unfold dist, later_dist.
753
754
      + by intros [x].
      + by intros [x] [y].
755
      + by intros [x] [y] [z] ??; trans y.
756
    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
757
  Qed.
758
759
760
761
762
763
764
765
766
767
768
  Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.

  Program Definition later_chain (c : chain laterC) : chain A :=
    {| chain_car n := later_car (c (S n)) |}.
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
  Global Program Instance later_cofe `{Cofe A} : Cofe laterC := 
    { compl c := Next (compl (later_chain c)) }.
  Next Obligation.
    intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))].
  Qed.

769
770
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
771
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
772
  Proof. by intros x y. Qed.
773
End later.
774
775
776
777

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
778
  Next (f (later_car x)).
779
Instance later_map_ne {A B : ofeT} (f : A  B) n :
780
781
782
783
784
785
786
787
  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.
788
Lemma later_map_ext {A B : ofeT} (f g : A  B) x :
789
790
  ( x, f x  g x)  later_map f x  later_map g x.
Proof. destruct x; intros Hf; apply Hf. Qed.
791
792
Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
  CofeMor (later_map f).
793
Instance laterC_map_contractive (A B : ofeT) : Contractive (@laterC_map A B).
794
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
795

Ralf Jung's avatar