cofe_solver.v 10.9 KB
Newer Older
1
Require Export algebra.cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

3 4 5 6 7 8 9 10 11 12 13
Record solution (F : cofeT  cofeT  cofeT) := Solution {
  solution_car :> cofeT;
  solution_unfold : solution_car -n> F solution_car solution_car;
  solution_fold : F solution_car solution_car -n> solution_car;
  solution_fold_unfold X : solution_fold (solution_unfold X)  X;
  solution_unfold_fold X : solution_unfold (solution_fold X)  X
}.
Arguments solution_unfold {_} _.
Arguments solution_fold {_} _.

Module solver. Section solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Context (F : cofeT  cofeT  cofeT).
15
Context `{Finhab : Inhabited (F unitC unitC)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29
Context (map :  {A1 A2 B1 B2 : cofeT},
  ((A2 -n> A1) * (B1 -n> B2))  (F A1 B1 -n> F A2 B2)).
Arguments map {_ _ _ _} _.
Instance: Params (@map) 4.
Context (map_id :  {A B : cofeT} (x : F A B), map (cid, cid) x  x).
Context (map_comp :  {A1 A2 A3 B1 B2 B3 : cofeT}
    (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x,
  map (f  g, g'  f') x  map (g,g') (map (f,f') x)).
Context (map_contractive :  {A1 A2 B1 B2}, Contractive (@map A1 A2 B1 B2)).

Lemma map_ext {A1 A2 B1 B2 : cofeT}
  (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) x x' :
  ( x, f x  f' x)  ( y, g y  g' y)  x  x' 
  map (f,g) x  map (f',g') x'.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
31 32 33 34 35 36 37
Lemma map_ne {A1 A2 B1 B2 : cofeT}
  (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) n x :
  ( x, f x {n} f' x)  ( y, g y {n} g' y) 
  map (f,g) x {n} map (f',g') x.
Proof.
  intros. by apply map_contractive=> i ?; apply dist_le with n; last lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39

Fixpoint A (k : nat) : cofeT :=
40
  match k with 0 => unitC | S k => F (A k) (A k) end.
41 42 43 44 45 46 47 48 49 50 51
Fixpoint f (k : nat) : A k -n> A (S k) :=
  match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
  match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
Arguments A : simpl never.
Arguments f : simpl never.
Arguments g : simpl never.

Lemma gf {k} (x : A k) : g k (f k x)  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53
Proof.
  induction k as [|k IH]; simpl in *; [by destruct x|].
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Qed.
56
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Proof.
58 59 60 61 62 63
  induction k as [|k IH]; simpl.
  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
    apply map_contractive=> i ?; omega.
  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
    apply map_contractive=> i ?; apply dist_le with k; [|omega].
    split=> x' /=; apply IH.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67
Qed.

Record tower := {
  tower_car k :> A k;
68
  g_tower k : g k (tower_car (S k))  tower_car k
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70
}.
Instance tower_equiv : Equiv tower := λ X Y,  k, X k  Y k.
71
Instance tower_dist : Dist tower := λ n X Y,  k, X k {n} Y k.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77
Program Definition tower_chain (c : chain tower) (k : nat) : chain (A k) :=
  {| chain_car i := c i k |}.
Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
Program Instance tower_compl : Compl tower := λ c,
  {| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
78 79 80
  intros c k; apply equiv_dist=> n.
  by rewrite (conv_compl (tower_chain c k) n)
    (conv_compl (tower_chain c (S k)) n) /= (g_tower (c (S n)) k).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Qed.
82
Definition tower_cofe_mixin : CofeMixin tower.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88 89 90 91
Proof.
  split.
  * intros X Y; split; [by intros HXY n k; apply equiv_dist|].
    intros HXY k; apply equiv_dist; intros n; apply HXY.
  * intros k; split.
    + by intros X n.
    + by intros X Y ? n.
    + by intros X Y Z ?? n; transitivity (Y n).
  * intros k X Y HXY n; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
    by rewrite -(g_tower X) (HXY (S n)) g_tower.
  * intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95
    apply (chain_cauchy c); lia.
Qed.
96
Definition T : cofeT := CofeT tower_cofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98

Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
99
  match i with 0 => cid | S i => f (i + k)  ff i end.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
101
  match i with 0 => cid | S i => gg i  g (i + k) end.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Lemma ggff {k i} (x : A k) : gg i (ff i x)  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
104 105 106
Lemma f_tower k (X : tower) : f (S k) (X (S k)) {k} X (S (S k)).
Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
Lemma ff_tower k i (X : tower) : ff i (X (S k)) {k} X (i + S k).
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108
Proof.
  intros; induction i as [|i IH]; simpl; [done|].
109
  by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111
Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k))  X k.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115 116 117 118 119 120 121 122 123 124 125

Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k).
Proof. by intros X Y HX. Qed.
Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k).

Definition coerce {i j} (H : i = j) : A i -n> A j :=
  eq_rect _ (λ i', A i -n> A i') cid _ H.
Lemma coerce_id {i} (H : i = i) (x : A i) : coerce H x = x.
Proof. unfold coerce. by rewrite (proof_irrel H (eq_refl i)). Qed.
Lemma coerce_proper {i j} (x y : A i) (H1 H2 : i = j) :
  x = y  coerce H1 x = coerce H2 y.
Proof. by destruct H1; rewrite !coerce_id. Qed.
Lemma g_coerce {k j} (H : S k = S j) (x : A (S k)) :
126
  g j (coerce H x) = coerce (Nat.succ_inj _ _ H) (g k x).
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
129
  coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131 132 133 134 135
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
  gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof.
  assert (i = i2 + i1) by lia; simplify_equality'. revert j x H1.
  induction i2 as [|i2 IH]; intros j X H1; simplify_equality';
Robbert Krebbers's avatar
Robbert Krebbers committed
136
    [by rewrite coerce_id|by rewrite g_coerce IH].
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139 140 141 142
Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
  coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof.
  assert (i = i1 + i2) by lia; simplify_equality'.
  induction i1 as [|i1 IH]; simplify_equality';
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    [by rewrite coerce_id|by rewrite coerce_f IH].
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145
Qed.

146
Definition embed_coerce {k} (i : nat) : A k -n> A i :=
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149 150
  match le_lt_dec i k with
  | left H => gg (k-i)  coerce (eq_sym (Nat.sub_add _ _ H))
  | right H => coerce (Nat.sub_add k i (Nat.lt_le_incl _ _ H))  ff (i-k)
  end.
151 152
Lemma g_embed_coerce {k i} (x : A k) :
  g i (embed_coerce (S i) x)  embed_coerce i x.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Proof.
154
  unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157
  * symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
  * exfalso; lia.
  * assert (i = k) by lia; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
    rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
    by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
  * assert (H : 1 + ((i - k) + k) = S i) by lia.
    rewrite (ff_ff _ H) /= -{2}(gf (ff (i - k) x)) g_coerce.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163
    by erewrite coerce_proper by done.
Qed.
164 165 166 167 168
Program Definition embed (k : nat) (x : A k) : T :=
  {| tower_car n := embed_coerce n x |}.
Next Obligation. intros k x i. apply g_embed_coerce. Qed.
Instance: Params (@embed) 1.
Instance embed_ne k n : Proper (dist n ==> dist n) (embed k).
169
Proof. by intros x y Hxy i; rewrite /= Hxy. Qed.
170 171
Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
Lemma embed_f k (x : A k) : embed (S k) (f k x)  embed k x.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Proof.
173
  rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177 178 179 180
    by erewrite g_coerce, gf, coerce_proper by done.
  * assert (S k = 0 + (0 + i)) as H by lia.
    rewrite (gg_gg _ H); simplify_equality'.
    by rewrite (ff_ff _ (eq_refl (1 + (0 + k)))).
  * exfalso; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
  * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
182 183
    by erewrite coerce_proper by done.
Qed.
184
Lemma embed_tower k (X : T) : embed (S k) (X (S k)) {k} X.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
Proof.
186 187 188
  intros i; rewrite /= /embed_coerce.
  destruct (le_lt_dec i (S k)) as [H|H]; simpl.
  * rewrite -(gg_tower i (S k - i) X).
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
190
  * rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193
Qed.

Program Definition unfold_chain (X : T) : chain (F T T) :=
194
  {| chain_car n := map (project n,embed' n) (X (S n)) |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196 197
Next Obligation.
  intros X n i Hi.
  assert ( k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
198 199 200 201 202 203
  induction k as [|k IH]; simpl.
  { rewrite -f_tower f_S -map_comp.
    apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f. }
  rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
  rewrite f_S -map_comp.
  apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
Qed.
205 206
Definition unfold (X : T) : F T T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold.
207 208 209 210
Proof.
  intros n X Y HXY. by rewrite /unfold (conv_compl (unfold_chain X) n)
    (conv_compl (unfold_chain Y) n) /= (HXY (S (S n))).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
211

212
Program Definition fold (X : F T T) : T :=
213
  {| tower_car n := g n (map (embed' n,project n) X) |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Next Obligation.
215 216
  intros X k. apply (_ : Proper (() ==> ()) (g k)).
  rewrite g_S -map_comp.
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218
  apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
Qed.
219 220
Instance fold_ne : Proper (dist n ==> dist n) fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222
Theorem result : solution F.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
Proof.
224
  apply (Solution F T (CofeMor unfold) (CofeMor fold)).
225
  * move=> X /=.
226
    rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
227
    rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
228 229
    transitivity (map (ff n, gg n) (X (S (n + k)))).
    { rewrite /unfold (conv_compl (unfold_chain X) n).
230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
      rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
      rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
      rewrite f_S -!map_comp; apply map_ne; fold A=> Y.
      + rewrite /embed' /= /embed_coerce.
        destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
        by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
      + rewrite /embed' /= /embed_coerce.
        destruct (le_lt_dec _ _); simpl; [|exfalso; lia].
        by rewrite (gg_gg _ (eq_refl (0 + (S n + k)))) /= gf. }
    assert ( i k (x : A (S i + k)) (H : S i + k = i + S k),
      map (ff i, gg i) x  gg i (coerce H x)) as map_ff_gg.
    { intros i; induction i as [|i IH]; intros k' x H; simpl.
      { by rewrite coerce_id map_id. }
      rewrite map_comp g_coerce; apply IH. }
    assert (H: S n + k = n + S k) by lia.
    rewrite (map_ff_gg _ _ _ H).
246
    apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
247 248 249 250 251 252
  * intros X; rewrite equiv_dist=> n /=.
    rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
    rewrite g_S -!map_comp -{2}(map_id _ _ X); apply map_ne=> Y /=.
    + apply dist_le with n; last omega.
      rewrite f_tower. apply dist_S. by rewrite embed_tower.
    + etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Qed.
254
End solver. End solver.