cofe.v 14.4 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
  Lemma contractive_S {B : cofeT} (f : A  B) `{!Contractive f} n x y :
110 111
    x {n} y  f x {S n} f y.
  Proof. eauto using contractive, dist_le with omega. Qed.
112 113 114
  Lemma contractive_0 {B : cofeT} (f : A  B) `{!Contractive f} x y :
    f x {0} f y.
  Proof. eauto using contractive with omega. Qed.
115
  Global Instance contractive_ne {B : cofeT} (f : A  B) `{!Contractive f} n :
116
    Proper (dist n ==> dist n) f | 100.
117
  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
118
  Global Instance contractive_proper {B : cofeT} (f : A  B) `{!Contractive f} :
119
    Proper (() ==> ()) f | 100 := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121
End cofe.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
137
(** Fixpoint *)
138
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A  A)
139
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Next Obligation.
141
  intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
142 143
  * apply (contractive_0 f).
  * apply (contractive_S f), IH; auto with omega.
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
  Proof.
152
    apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
153
    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  Qed.
155
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
156
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  Proof.
158 159 160 161
    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
162
  Qed.
163 164
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
165 166
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
167
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169

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

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

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

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

(** Product *)
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 272 273 274
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
275 276 277 278 279 280 281 282 283
  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.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
308 309
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
310

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

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

Arguments laterC : clear implicits.

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