cofe.v 13.2 KB
Newer Older
1
Require Export prelude.prelude.
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
Ltac cofe_subst :=
  repeat match goal with
  | _ => progress simplify_equality'
13 14
  | 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
15
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46

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.
47 48 49 50 51
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
52 53 54 55 56 57 58 59 60 61 62 63 64 65

(** 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
66 67
    * by transitivity x1; [|transitivity y1].
    * by transitivity x2; [|transitivity y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71 72 73 74 75 76 77
  Qed.
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (dist n).
  Proof.
    intros x1 x2 Hx y1 y2 Hy.
    by rewrite equiv_dist in Hx, Hy; rewrite (Hx n), (Hy n).
  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.
78
  Instance ne_proper `{Cofe B} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80
    `{! 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.
81
  Instance ne_proper_2 `{Cofe B, Cofe C} (f : A  B  C)
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85
    `{! 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
86
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n), (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90 91
  Qed.
  Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n  compl c1 ={n}= compl c2.
  Proof. intros. by rewrite (conv_compl c1 n), (conv_compl c2 n). Qed.
  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.
92 93 94 95 96
  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
97 98
End cofe.

Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101 102 103 104
(** 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
105 106 107 108
(** 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
109
(** Fixpoint *)
110 111
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
112 113 114 115
Next Obligation.
  intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
  destruct i as [|i]; simpl; try lia; apply contractive, IH; auto with lia.
Qed.
116 117
Program Definition fixpoint `{Cofe A, Inhabited A} (f : A  A)
  `{!Contractive f} : A := compl (fixpoint_chain f).
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119

Section fixpoint.
120 121
  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
122 123
  Proof.
    apply equiv_dist; intros n; unfold fixpoint.
124 125
    rewrite (conv_compl (fixpoint_chain f) n).
    by rewrite (chain_cauchy (fixpoint_chain f) n (S n)) at 1 by lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  Qed.
127 128
  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
129
  Proof.
130 131
    intros Hfg; unfold fixpoint.
    rewrite (conv_compl (fixpoint_chain f) n),(conv_compl (fixpoint_chain g) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133 134
    induction n as [|n IH]; simpl in *; [done|].
    rewrite Hfg; apply contractive, IH; auto using dist_S.
  Qed.
135 136
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
139
Global Opaque fixpoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141

(** Function space *)
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Record cofeMor (A B : cofeT) : Type := CofeMor {
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
  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.
  rewrite (conv_compl (fun_chain c x) n), (conv_compl (fun_chain c y) n).
  simpl; rewrite Hxy; apply (chain_cauchy c); lia.
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.
179 180 181 182 183
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
184 185 186 187
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).
188 189
Instance cofe_more_inhabited (A B : cofeT)
  `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
Robbert Krebbers's avatar
Robbert Krebbers committed
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 216 217 218 219

(** 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.
Proof. by intros Hf Hg x; simpl; rewrite (Hg x), (Hf (g2 x)). Qed.

(** 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
220 221 222 223
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
224
Instance prod_compl `{Compl A, Compl B} : Compl (A * B) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  (compl (chain_map fst c), compl (chain_map snd c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229 230 231 232 233
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
234 235
  * 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
236
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239
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
240
Canonical Structure prodC (A B : cofeT) : cofeT := CofeT (A * B).
241
Instance prod_map_ne `{Dist A, Dist A', Dist B, Dist B'} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
242 243 244 245 246 247 248 249 250 251
  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.
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267

(** 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
268 269
  Global Instance discrete_timeless (x : A) : Timeless x.
  Proof. by intros y. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
  Definition discreteC : cofeT := CofeT A.
271
End discrete_cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
Arguments discreteC _ {_ _}.
273

Robbert Krebbers's avatar
Robbert Krebbers committed
274
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
Robbert Krebbers's avatar
Robbert Krebbers committed
275 276
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
277

278 279
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
280
Add Printing Constructor later.
281 282
Arguments Later {_} _.
Arguments later_car {_} _.
283

284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
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).

309 310
  Global Instance Later_contractive `{Dist A} : Contractive (@Later A).
  Proof. by intros n ??. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
311 312
  Definition later_map {A B} (f : A  B) (x : later A) : later B :=
    Later (f (later_car x)).
313 314 315 316
  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
317
  Lemma later_fmap_id {A} (x : later A) : later_map id x = x.
318 319
  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
320
    later_map (g  f) x = later_map g (later_map f x).
321 322
  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
323
    CofeMor (later_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
324
  Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
325 326
  Proof. intros n f g Hf n'; apply Hf. Qed.
End later.