cofe.v 13.5 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
Require Export modures.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
8
9
Notation "x ={ n }= y" := (dist n x y)
  (at level 70, n at next level, format "x  ={ n }=  y").
Hint Extern 0 (?x ={_}= ?x) => reflexivity.
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

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.

Class Cofe A `{Equiv A, Compl A} := {
  equiv_dist x y : x  y   n, x ={n}= y;
  dist_equivalence n :> Equivalence (dist n);
  dist_S n x y : x ={S n}= y  x ={n}= y;
  dist_0 x y : x ={0}= y;
  conv_compl (c : chain A) n : compl c ={n}= c n
}.
Hint Extern 0 (_ ={0}= _) => apply dist_0.
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;
  cofe_cofe : Cofe cofe_car
}.
Arguments CofeT _ {_ _ _ _}.
Add Printing Constructor cofeT.
Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe.
54
55
56
57
58
Arguments cofe_car _ : simpl never.
Arguments cofe_equiv _ _ _ : simpl never.
Arguments cofe_dist _ _ _ _ : simpl never.
Arguments cofe_compl _ _ : simpl never.
Arguments cofe_cofe _ : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
62
63
64
65
66
67
68
69
70
71
72

(** General properties *)
Section cofe.
  Context `{Cofe A}.
  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.
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (dist n).
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
    * by transitivity x1; [|transitivity y1].
    * by transitivity x2; [|transitivity y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
  Qed.
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (dist n).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81
82
83
  Qed.
  Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.
  Lemma dist_le x y n n' : x ={n}= y  n'  n  x ={n'}= y.
  Proof. induction 2; eauto using dist_S. Qed.
84
  Instance ne_proper `{Cofe B} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
    `{! 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.
87
  Instance ne_proper_2 `{Cofe B, Cofe C} (f : A  B  C)
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
91
    `{! 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
92
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
  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
95
  Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
  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.
98
99
100
101
102
  Global Instance contractive_ne `{Cofe B} (f : A  B) `{!Contractive f} n :
    Proper (dist n ==> dist n) f | 100.
  Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
  Global Instance contractive_proper `{Cofe B} (f : A  B) `{!Contractive f} :
    Proper (() ==> ()) f | 100 := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
End cofe.

Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
108
109
110
(** 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) |}.
Next Obligation. by intros A ? B ? f Hf c n i ?; apply Hf, chain_cauchy. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
(** Timeless elements *)
Class Timeless `{Dist A, Equiv A} (x : A) := timeless y : x ={1}= y  x  y.
Arguments timeless {_ _ _} _ {_} _ _.

Robbert Krebbers's avatar
Robbert Krebbers committed
115
(** Fixpoint *)
116
117
Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A  A)
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
Next Obligation.
  intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Qed.
122
123
Program Definition fixpoint `{Cofe A, Inhabited A} (f : A  A)
  `{!Contractive f} : A := compl (fixpoint_chain f).
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125

Section fixpoint.
126
127
  Context `{Cofe A, Inhabited A} (f : A  A) `{!Contractive f}.
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
  Proof.
    apply equiv_dist; intros n; unfold fixpoint.
130
    rewrite (conv_compl (fixpoint_chain f) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Qed.
133
134
  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
135
  Proof.
136
    intros Hfg; unfold fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
    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
139
140
    rewrite Hfg; apply contractive, IH; auto using dist_S.
  Qed.
141
142
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
145
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147

(** Function space *)
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Record cofeMor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  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.

Instance cofe_mor_proper `(f : cofeMor A B) : Proper (() ==> ()) f := _.
Instance cofe_mor_equiv {A B : cofeT} : Equiv (cofeMor A B) := λ f g,
   x, f x  g x.
Instance cofe_mor_dist (A B : cofeT) : 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 A B c x n i ?. by apply (chain_cauchy c). Qed.
Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c,
  {| cofe_mor_car x := compl (fun_chain c x) |}.
Next Obligation.
  intros A B c n x y Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
  rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hxy.
  apply (chain_cauchy c); lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
Qed.
Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B).
Proof.
  split.
  * intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|].
    intros HXY k; apply equiv_dist; intros n; apply HXY.
  * 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.
185
186
187
188
189
Instance cofe_mor_car_ne A B 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.
Instance cofe_mor_car_proper A B :
  Proper (() ==> () ==> ()) (@cofe_mor_car A B) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
192
193
Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f  g   x, f x  g x.
Proof. done. Qed.
Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B).
Infix "-n>" := cofe_mor (at level 45, right associativity).
194
195
Instance cofe_more_inhabited (A B : cofeT)
  `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
199
200
201
202
203
204
205

(** 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
206
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225

(** Pre-composition as a functor *)
Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n :
  Proper (dist n ==> dist n) (λ g : A -n> C, g  f).
Proof. by intros g1 g2 ?; apply ccompose_ne. Qed.
Definition ccompose_l {A B C} (f : B -n> A) : (A -n> C) -n> (B -n> C) :=
  CofeMor (λ g : A -n> C, g  f).
Instance ccompose_l_ne {A B C} : Proper (dist n ==> dist n) (@ccompose_l A B C).
Proof. by intros n f1 f2 Hf g x; apply ccompose_ne. Qed.

(** unit *)
Instance unit_dist : Dist unit := λ _ _ _, True.
Instance unit_compl : Compl unit := λ _, ().
Instance unit_cofe : Cofe unit.
Proof. by repeat split; try exists 0. Qed.

(** Product *)
Instance prod_dist `{Dist A, Dist B} : Dist (A * B) := λ n,
  prod_relation (dist n) (dist n).
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
228
229
Instance pair_ne `{Dist A, Dist B} :
  Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
Instance fst_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@fst A B) := _.
Instance snd_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@snd A B) := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Instance prod_compl `{Compl A, Compl B} : Compl (A * B) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
231
  (compl (chain_map fst c), compl (chain_map snd c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
234
235
236
237
238
239
Instance prod_cofe `{Cofe A, Cofe B} : Cofe (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
241
  * intros c n; split. apply (conv_compl (chain_map fst c) n).
    apply (conv_compl (chain_map snd c) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
242
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
244
245
Instance pair_timeless `{Dist A, Equiv A, Dist B, Equiv B} (x : A) (y : B) :
  Timeless x  Timeless y  Timeless (x,y).
Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Canonical Structure prodC (A B : cofeT) : cofeT := CofeT (A * B).
247
Instance prod_map_ne `{Dist A, Dist A', Dist B, Dist B'} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
250
251
252
253
254
255
256
257
  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.

Typeclasses Opaque prod_dist.
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273

(** 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.
  Instance discrete_cofe : Cofe A.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
  Global Instance discrete_timeless (x : A) : Timeless x.
  Proof. by intros y. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
276
  Definition discreteC : cofeT := CofeT A.
277
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
Arguments discreteC _ {_ _}.
279

Robbert Krebbers's avatar
Robbert Krebbers committed
280
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
282
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
283

284
285
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
286
Add Printing Constructor later.
287
288
Arguments Later {_} _.
Arguments later_car {_} _.
289

290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
Section later.
  Instance later_equiv `{Equiv A} : Equiv (later A) := λ x y,
    later_car x  later_car y.
  Instance later_dist `{Dist A} : Dist (later A) := λ n x y,
    match n with 0 => True | S n => later_car x ={n}= later_car y end.
  Program Definition later_chain `{Dist A} (c : chain (later A)) : chain A :=
    {| chain_car n := later_car (c (S n)) |}.
  Next Obligation. intros A ? c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
  Instance later_compl `{Compl A} : Compl (later A) := λ c,
    Later (compl (later_chain c)).
  Instance later_cofe `{Cofe A} : Cofe (later A).
  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.
  Canonical Structure laterC (A : cofeT) : cofeT := CofeT (later A).

315
316
  Global Instance Later_contractive `{Dist A} : Contractive (@Later A).
  Proof. by intros n ??. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
318
  Definition later_map {A B} (f : A  B) (x : later A) : later B :=
    Later (f (later_car x)).
319
320
321
322
  Global Instance later_map_ne `{Cofe A, Cofe B} (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  Lemma later_fmap_id {A} (x : later A) : later_map id x = x.
324
325
  Proof. by destruct x. Qed.
  Lemma later_fmap_compose {A B C} (f : A  B) (g : B  C) (x : later A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
326
    later_map (g  f) x = later_map g (later_map f x).
327
328
  Proof. by destruct x. Qed.
  Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
329
    CofeMor (later_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
330
  Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
331
332
  Proof. intros n f g Hf n'; apply Hf. Qed.
End later.