cofe.v 14.5 KB
Newer Older
1
Require Export algebra.base.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4

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

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

Record chain (A : Type) `{Dist A} := {
  chain_car :> nat  A;
  chain_cauchy n i : n  i  chain_car n ={n}= chain_car i
}.
Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
Class Compl A `{Dist A} := compl : chain A  A.

32
33
34
35
36
37
Record CofeMixin A `{Equiv A, Compl A} := {
  mixin_equiv_dist x y : x  y   n, x ={n}= y;
  mixin_dist_equivalence n : Equivalence (dist n);
  mixin_dist_S n x y : x ={S n}= y  x ={n}= y;
  mixin_dist_0 x y : x ={0}= y;
  mixin_conv_compl (c : chain A) n : compl c ={n}= c n
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40
41
42
43
44
45
46
47
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
  contractive n : Proper (dist n ==> dist (S n)) f.

(** Bundeled version *)
Structure cofeT := CofeT {
  cofe_car :> Type;
  cofe_equiv : Equiv cofe_car;
  cofe_dist : Dist cofe_car;
  cofe_compl : Compl cofe_car;
48
  cofe_mixin : CofeMixin cofe_car
Robbert Krebbers's avatar
Robbert Krebbers committed
49
}.
50
Arguments CofeT {_ _ _ _} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Add Printing Constructor cofeT.
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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.
  Lemma equiv_dist x y : x  y   n, x ={n}= y.
  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.
  Lemma dist_S n x y : x ={S n}= y  x ={n}= y.
  Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
  Lemma dist_0 x y : x ={0}= y.
  Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed.
  Lemma conv_compl (c : chain A) n : compl c ={n}= c n.
  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.

Hint Extern 0 (_ ={0}= _) => apply dist_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78

(** General properties *)
Section cofe.
79
80
  Context {A : cofeT}.
  Implicit Types x y : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
84
85
86
87
  Global Instance cofe_equivalence : Equivalence (() : relation A).
  Proof.
    split.
    * by intros x; rewrite equiv_dist.
    * by intros x y; rewrite !equiv_dist.
    * by intros x y z; rewrite !equiv_dist; intros; transitivity y.
  Qed.
88
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
    * by transitivity x1; [|transitivity y1].
    * by transitivity x2; [|transitivity y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  Qed.
94
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
99
  Qed.
  Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.
100
  Lemma dist_le (x y : A) n n' : x ={n}= y  n'  n  x ={n'}= y.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  Proof. induction 2; eauto using dist_S. Qed.
102
  Instance ne_proper {B : cofeT} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
    `{! 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.
105
  Instance ne_proper_2 {B C : cofeT} (f : A  B  C)
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
109
    `{! 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
110
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
  Qed.
  Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n  compl c1 ={n}= compl c2.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
  Lemma compl_ext (c1 c2 : chain A) : ( i, c1 i  c2 i)  compl c1  compl c2.
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
116
  Global Instance contractive_ne {B : cofeT} (f : A  B) `{!Contractive f} n :
117
118
    Proper (dist n ==> dist n) f | 100.
  Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
119
  Global Instance contractive_proper {B : cofeT} (f : A  B) `{!Contractive f} :
120
    Proper (() ==> ()) f | 100 := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
End cofe.

Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
125
126
(** 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) |}.
127
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
128

Robbert Krebbers's avatar
Robbert Krebbers committed
129
(** Timeless elements *)
130
131
Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y  x  y.
Arguments timeless {_} _ {_} _ _.
132
133
134
135
136
Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x  x  y  x ={S n}= y.
Proof.
  split; intros; [by apply equiv_dist|].
  apply (timeless _), dist_le with (S n); auto with lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
137

Robbert Krebbers's avatar
Robbert Krebbers committed
138
(** Fixpoint *)
139
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A  A)
140
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Next Obligation.
142
  intros A ? f ? n; induction n as [|n IH]; intros i ?; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Qed.
145
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A  A)
146
  `{!Contractive f} : A := compl (fixpoint_chain f).
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148

Section fixpoint.
149
  Context {A : cofeT} `{Inhabited A} (f : A  A) `{!Contractive f}.
150
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
  Proof.
    apply equiv_dist; intros n; unfold fixpoint.
153
    rewrite (conv_compl (fixpoint_chain f) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  Qed.
156
157
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
    ( z, f z ={n}= g z)  fixpoint f ={n}= fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  Proof.
159
    intros Hfg; unfold fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
    rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
    induction n as [|n IH]; simpl in *; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
    rewrite Hfg; apply contractive, IH; auto using dist_S.
  Qed.
164
165
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
168
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170

(** Function space *)
Robbert Krebbers's avatar
Robbert Krebbers committed
171
Record cofeMor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
175
176
177
178
  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.

179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
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.
  Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g,  x, f x ={n}= g x.
  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.
    intros c n x y Hx.
    rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx.
    apply (chain_cauchy c); lia.
  Qed.
  Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
  Proof.
    split.
198
199
    * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
      intros Hfg k; apply equiv_dist; intros n; apply Hfg.
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
    * intros n; split.
      + by intros f x.
      + by intros f g ? x.
      + by intros f g h ?? x; transitivity (g x).
    * by intros n f g ? x; apply dist_S.
    * by intros f g x.
    * intros c n x; simpl.
      rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
  Qed.
  Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.

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

Arguments cofe_mor : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
Infix "-n>" := cofe_mor (at level 45, right associativity).
222
223
Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
224
225
226
227
228
229
230
231
232
233

(** Identity and composition *)
Definition cid {A} : A -n> A := CofeMor id.
Instance: Params (@cid) 1.
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 :
  f1 ={n}= f2  g1 ={n}= g2  f1  g1 ={n}= f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236

(** unit *)
237
238
239
240
241
242
Section unit.
  Instance unit_dist : Dist unit := λ _ _ _, True.
  Instance unit_compl : Compl unit := λ _, ().
  Definition unit_cofe_mixin : CofeMixin unit.
  Proof. by repeat split; try exists 0. Qed.
  Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
244
  Global Instance unit_timeless (x : ()) : Timeless x.
  Proof. done. Qed.
245
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
247

(** Product *)
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
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.
    * intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
      rewrite !equiv_dist; naive_solver.
    * apply _.
    * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
    * by split.
    * intros c n; split. apply (conv_compl (chain_map fst c) n).
      apply (conv_compl (chain_map snd c) n).
  Qed.
  Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
  Global Instance pair_timeless (x : A) (y : B) :
    Timeless x  Timeless y  Timeless (x,y).
  Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
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
279
280
281
282
283
284
285
286
287
  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.

288
289
290
291
292
293
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
  Instance discrete_dist : Dist A := λ n x y,
    match n with 0 => True | S n => x  y end.
  Instance discrete_compl : Compl A := λ c, c 1.
294
  Definition discrete_cofe_mixin : CofeMixin A.
295
296
297
298
299
300
301
302
  Proof.
    split.
    * intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)].
    * intros [|n]; [done|apply _].
    * by intros [|n].
    * done.
    * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
  Qed.
303
304
  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
  Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
Robbert Krebbers's avatar
Robbert Krebbers committed
305
  Proof. by intros y. Qed.
306
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
Arguments discreteC _ {_ _}.
308

Robbert Krebbers's avatar
Robbert Krebbers committed
309
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
310
311
312
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
315

316
317
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
318
Add Printing Constructor later.
319
320
Arguments Later {_} _.
Arguments later_car {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
Lemma later_eta {A} (x : later A) : Later (later_car x) = x.
Proof. by destruct x. Qed.
323

324
Section later.
325
326
327
  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,
328
    match n with 0 => True | S n => later_car x ={n}= later_car y end.
329
  Program Definition later_chain (c : chain (later A)) : chain A :=
330
    {| chain_car n := later_car (c (S n)) |}.
331
332
333
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
  Instance later_compl : Compl (later A) := λ c, Later (compl (later_chain c)).
  Definition later_cofe_mixin : CofeMixin (later A).
334
335
336
337
338
339
340
341
342
343
344
345
  Proof.
    split.
    * intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
    * intros [|n]; [by split|split]; unfold dist, later_dist.
      + by intros [x].
      + by intros [x] [y].
      + by intros [x] [y] [z] ??; transitivity y.
    * intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
    * done.
    * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
  Qed.
346
347
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
  Global Instance Later_contractive : Contractive (@Later A).
348
  Proof. by intros n ??. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
350
  Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A).
  Proof. by intros x y. Qed.
351
End later.
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
  Later (f (later_car x)).
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.
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).
Proof. intros n f g Hf n'; apply Hf. Qed.