cofe.v 14.3 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.
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 {_} ?y) => 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

Ralf Jung's avatar
Ralf Jung committed
24
Tactic Notation "solve_ne" := intros; solve_proper.
25

Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
Record chain (A : Type) `{Dist A} := {
  chain_car :> nat  A;
28
  chain_cauchy n i : n < i  chain_car i {n} chain_car (S n)
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
}.
Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
Class Compl A `{Dist A} := compl : chain A  A.

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
125
(** Timeless elements *)
126
Class Timeless {A : cofeT} (x : A) := timeless y : x {0} y  x  y.
127
Arguments timeless {_} _ {_} _ _.
128
Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x  x  y  x {n} y.
129
130
Proof.
  split; intros; [by apply equiv_dist|].
131
  apply (timeless _), dist_le with n; auto with lia.
132
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
133

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

Section fixpoint.
146
  Context {A : cofeT} `{Inhabited A} (f : A  A) `{!Contractive f}.
147
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
148
  Proof.
149
150
    apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
    induction n as [|n IH]; simpl; eauto using contractive, dist_le with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  Qed.
152
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
153
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  Proof.
155
156
157
158
    intros Hfg. rewrite /fixpoint
      (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=.
    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
159
  Qed.
160
161
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
164
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166

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

175
176
177
178
179
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.
180
  Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g,  x, f x {n} g x.
181
182
183
184
185
186
  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.
187
188
    intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n)
      (conv_compl (fun_chain c y) n) /= Hx.
189
190
191
192
  Qed.
  Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
  Proof.
    split.
193
194
    * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
      intros Hfg k; apply equiv_dist; intros n; apply Hfg.
195
196
197
198
199
200
    * 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.
    * intros c n x; simpl.
201
      by rewrite (conv_compl (fun_chain c x) n) /=.
202
203
204
205
206
207
208
209
210
211
212
213
214
  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
215
Infix "-n>" := cofe_mor (at level 45, right associativity).
216
217
Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
220
221
222
223
224
225
226

(** 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 :
227
  f1 {n} f2  g1 {n} g2  f1  g1 {n} f2  g2.
Robbert Krebbers's avatar
Robbert Krebbers committed
228
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230

(** unit *)
231
232
233
234
235
236
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
237
238
  Global Instance unit_timeless (x : ()) : Timeless x.
  Proof. done. Qed.
239
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
241

(** Product *)
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
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.
    * 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
272
273
274
275
276
277
278
279
280
  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.

281
282
283
(** Discrete cofe *)
Section discrete_cofe.
  Context `{Equiv A, @Equivalence A ()}.
284
  Instance discrete_dist : Dist A := λ n x y, x  y.
285
  Instance discrete_compl : Compl A := λ c, c 1.
286
  Definition discrete_cofe_mixin : CofeMixin A.
287
288
  Proof.
    split.
289
290
    * intros x y; split; [done|intros Hn; apply (Hn 0)].
    * done.
291
    * done.
292
293
    * intros c n. rewrite /compl /discrete_compl /=.
      symmetry; apply (chain_cauchy c 0 (S n)); omega.
294
  Qed.
295
296
  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
  Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Proof. by intros y. Qed.
298
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Arguments discreteC _ {_ _}.
300

Robbert Krebbers's avatar
Robbert Krebbers committed
301
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
302
303
304
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
305
306
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
307

308
(** Later *)
309
Inductive later (A : Type) : Type := Next { later_car : A }.
310
Add Printing Constructor later.
311
Arguments Next {_} _.
312
Arguments later_car {_} _.
313
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Proof. by destruct x. Qed.
315

316
Section later.
317
318
319
  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,
320
    match n with 0 => True | S n => later_car x {n} later_car y end.
321
  Program Definition later_chain (c : chain (later A)) : chain A :=
322
    {| chain_car n := later_car (c (S n)) |}.
323
  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
324
  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
325
  Definition later_cofe_mixin : CofeMixin (later A).
326
327
328
329
330
331
332
333
334
335
336
  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.
    * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
  Qed.
337
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
338
339
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
340
  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  Proof. by intros x y. Qed.
342
End later.
343
344
345
346

Arguments laterC : clear implicits.

Definition later_map {A B} (f : A  B) (x : later A) : later B :=
347
  Next (f (later_car x)).
348
349
350
351
352
353
354
355
356
357
358
359
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).
360
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.