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 24 25

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
132
(** Fixpoint *)
133
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A  A)
134
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Next Obligation.
136 137 138
  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
139
Qed.
140
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A  A)
141
  `{!Contractive f} : A := compl (fixpoint_chain f).
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143

Section fixpoint.
144
  Context {A : cofeT} `{Inhabited A} (f : A  A) `{!Contractive f}.
145
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  Proof.
147 148
    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
149
  Qed.
150
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
151
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  Proof.
153 154 155 156
    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
157
  Qed.
158 159
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
162
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164

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

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

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

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

(** Product *)
240 241 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
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
270 271 272 273 274 275 276 277 278
  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.

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

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

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

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

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

Arguments laterC : clear implicits.

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