cofe.v 14 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
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 {_} _ {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
132

Robbert Krebbers's avatar
Robbert Krebbers committed
133
(** Fixpoint *)
134
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A  A)
135
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Next Obligation.
137
  intros A ? f ? n; induction n as [|n IH]; intros i ?; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
  destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
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 147
  Proof.
    apply equiv_dist; intros n; unfold fixpoint.
148
    rewrite (conv_compl (fixpoint_chain f) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
149
    by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  Qed.
151 152
  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
153
  Proof.
154
    intros Hfg; unfold fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156
    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
157 158
    rewrite Hfg; apply contractive, IH; auto using dist_S.
  Qed.
159 160
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
163
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165

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

174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
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.
    * 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.
  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
216
Infix "-n>" := cofe_mor (at level 45, right associativity).
217 218
Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
219 220 221 222 223 224 225 226 227 228

(** 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
229
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
230 231

(** unit *)
232 233 234 235 236 237 238
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.
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
239 240

(** Product *)
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 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.
    * 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
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 284 285 286
(** 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.
287
  Definition discrete_cofe_mixin : CofeMixin A.
288 289 290 291 292 293 294 295
  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.
296 297
  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
  Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  Proof. by intros y. Qed.
299
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Arguments discreteC _ {_ _}.
301

Robbert Krebbers's avatar
Robbert Krebbers committed
302
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
305

306 307
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
308
Add Printing Constructor later.
309 310
Arguments Later {_} _.
Arguments later_car {_} _.
311

312
Section later.
313 314 315
  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,
316
    match n with 0 => True | S n => later_car x ={n}= later_car y end.
317
  Program Definition later_chain (c : chain (later A)) : chain A :=
318
    {| chain_car n := later_car (c (S n)) |}.
319 320 321
  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).
322 323 324 325 326 327 328 329 330 331 332 333
  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.
334 335
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
  Global Instance Later_contractive : Contractive (@Later A).
336
  Proof. by intros n ??. Qed.
337
End later.
338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355

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.