cofe_solver.v 9.85 KB
Newer Older
1
Require Export modures.cofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4

Section solver.
Context (F : cofeT  cofeT  cofeT).
5
Context `{Finhab : Inhabited (F (CofeT unit) (CofeT unit))}.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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
20
Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24

Fixpoint A (k : nat) : cofeT :=
  match k with 0 => CofeT unit | S k => F (A k) (A k) end.
Fixpoint f {k} : A k -n> A (S k) :=
25
  match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
with g {k} : A (S k) -n> A k :=
  match k with 0 => CofeMor (λ _, () : CofeT ()) | S k => map (f,g) end.
Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
Lemma gf {k} (x : A k) : g (f x)  x.
Proof.
  induction k as [|k IH]; simpl in *; [by destruct x|].
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
Qed.
Lemma fg {n k} (x : A (S k)) : n  k  f (g x) ={n}= x.
Proof.
  intros Hnk; apply dist_le with k; auto; clear Hnk.
  induction k as [|k IH]; simpl; [apply dist_0|].
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
Qed.
Arguments A _ : simpl never.
Arguments f {_} : simpl never.
Arguments g {_} : simpl never.

Record tower := {
  tower_car k :> A k;
  g_tower k : g (tower_car (S k))  tower_car k
}.
Instance tower_equiv : Equiv tower := λ X Y,  k, X k  Y k.
Instance tower_dist : Dist tower := λ n X Y,  k, X k ={n}= Y k.
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.
  intros c k; apply equiv_dist; intros n.
  rewrite (conv_compl (tower_chain c k) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
62
63
64
65
66
67
68
69
70
Qed.
Instance tower_cofe : Cofe tower.
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
71
    by rewrite -(g_tower X) (HXY (S n)) g_tower.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  * intros X Y k; apply dist_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  * intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
77
78
79
80
81
82
    apply (chain_cauchy c); lia.
Qed.
Definition T : cofeT := CofeT tower.

Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
  match i with 0 => cid | S i => f  ff i end.
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
  match i with 0 => cid | S i => gg i  g end.
Lemma ggff {k i} (x : A k) : gg i (ff i x)  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Lemma f_tower {n k} (X : tower) : n  k  f (X k) ={n}= X (S k).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
Lemma ff_tower {n} k i (X : tower) : n  k  ff i (X k) ={n}= X (i + k).
Proof.
  intros; induction i as [|i IH]; simpl; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  by rewrite IH (f_tower X); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k))  X k.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

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)) :
  g (coerce H x) = coerce (Nat.succ_inj _ _ H) (g x).
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) :
  coerce H (f x) = f (coerce (Nat.succ_inj _ _ H) x).
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
116
    [by rewrite coerce_id|by rewrite g_coerce IH].
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
121
122
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
123
    [by rewrite coerce_id|by rewrite coerce_f IH].
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
127
128
129
130
131
132
133
134
135
136
Qed.

Definition embed' {k} (i : nat) : A k -n> A i :=
  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.
Lemma g_embed' {k i} (x : A k) : g (embed' (S i) x)  embed' i x.
Proof.
  unfold embed'; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
  * 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
137
    rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
    by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
  * 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
141
142
143
144
145
146
147
148
149
150
151
152
153
    by erewrite coerce_proper by done.
Qed.
Program Definition embed_inf (k : nat) (x : A k) : T :=
  {| tower_car n := embed' n x |}.
Next Obligation. intros k x i. apply g_embed'. Qed.
Instance embed_inf_ne k n : Proper (dist n ==> dist n) (embed_inf k).
Proof. by intros x y Hxy i; simpl; rewrite Hxy. Qed.
Definition embed (k : nat) : A k -n> T := CofeMor (embed_inf k).
Lemma embed_f k (x : A k) : embed (S k) (f x)  embed k x.
Proof.
  rewrite equiv_dist; intros n i.
  unfold embed_inf, embed; simpl; unfold embed'.
  destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
158
159
    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
160
  * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
164
165
    by erewrite coerce_proper by done.
Qed.
Lemma embed_tower j n (X : T) : n  j  embed j (X j) ={n}= X.
Proof.
  intros Hn i; simpl; unfold embed'; destruct (le_lt_dec i j) as [H|H]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  * rewrite -(gg_tower i (j - i) X).
Robbert Krebbers's avatar
Robbert Krebbers committed
167
    apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  * rewrite (ff_tower j (i-j) X); last lia. by destruct (Nat.sub_add _ _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
172
173
174
175
176
Qed.

Program Definition unfold_chain (X : T) : chain (F T T) :=
  {| chain_car n := map (project n,embed n) (f (X n)) |}.
Next Obligation.
  intros X n i Hi.
  assert ( k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
  induction k as [|k Hk]; simpl; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  rewrite Hk (f_tower X); last lia; rewrite f_S -map_comp.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
181
182
183
  apply dist_S, map_contractive.
  split; intros Y; symmetry; apply equiv_dist; [apply g_tower|apply embed_f].
Qed.
Definition unfold' (X : T) : F T T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold'.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  by intros n X Y HXY; unfold unfold'; apply compl_ne; rewrite /= (HXY n).
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
187
188
189
190
191
Qed.
Definition unfold : T -n> F T T := CofeMor unfold'.

Program Definition fold' (X : F T T) : T :=
  {| tower_car n := g (map (embed n,project n) X) |}.
Next Obligation.
  intros X k; apply (_ : Proper (() ==> ()) g).
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  rewrite -(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g).
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
196
197
198
199
200
201
202
203
  apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
Qed.
Instance fold_ne : Proper (dist n ==> dist n) fold'.
Proof. by intros n X Y HXY k; simpl; unfold fold'; simpl; rewrite HXY. Qed.
Definition fold : F T T -n> T := CofeMor fold'.

Definition fold_unfold X : fold (unfold X)  X.
Proof.
  assert (map_ff_gg :  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)).
  { intros i; induction i as [|i IH]; intros k x H; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
    { by rewrite coerce_id map_id. }
    rewrite map_comp g_coerce; apply IH. }
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) g).
Robbert Krebbers's avatar
Robbert Krebbers committed
208
209
  transitivity (map (ff n, gg n) (X (S (n + k)))).
  { unfold unfold'; rewrite (conv_compl (unfold_chain X) n).
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
    rewrite (chain_cauchy (unfold_chain X) n (n + k)) /=; last lia.
    rewrite (f_tower X); last lia; rewrite -map_comp.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
214
215
216
217
218
219
220
221
222
    apply dist_S. apply map_contractive; split; intros x; simpl; unfold embed'.
    * destruct (le_lt_dec _ _); simpl.
      { assert (n = 0) by lia; subst. apply dist_0. }
      by rewrite (ff_ff _ (eq_refl (n + (0 + k)))).
    * destruct (le_lt_dec _ _); [|exfalso; lia]; simpl.
      by rewrite (gg_gg _ (eq_refl (0 + (n + k)))). }
  assert (H: S n + k = n + S k) by lia; rewrite (map_ff_gg _ _ _ H).
  apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
Qed.
Definition unfold_fold X : unfold (fold X)  X.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
225
226
  rewrite equiv_dist; intros n.
  rewrite /(unfold) /= /(unfold') (conv_compl (unfold_chain (fold X)) n) /=.
  rewrite (fg (map (embed _,project n) X)); last lia.
  rewrite -map_comp -{2}(map_id _ _ X).
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
  apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia.
Qed.
End solver.
230

Robbert Krebbers's avatar
Robbert Krebbers committed
231
Global Opaque T fold unfold.