cofe_solver.v 9.85 KB
 Robbert Krebbers committed Dec 15, 2015 1 ``````Require Export modures.cofe. `````` Robbert Krebbers committed Nov 11, 2015 2 3 4 `````` Section solver. Context (F : cofeT → cofeT → cofeT). `````` Robbert Krebbers committed Nov 17, 2015 5 ``````Context `{Finhab : Inhabited (F (CofeT unit) (CofeT unit))}. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 20 ``````Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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) := `````` Robbert Krebbers committed Nov 17, 2015 25 `````` match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 33 `````` rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 39 `````` rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 59 `````` by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k). `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 71 `````` by rewrite -(g_tower X) (HXY (S n)) g_tower. `````` Robbert Krebbers committed Nov 11, 2015 72 `````` * intros X Y k; apply dist_0. `````` Robbert Krebbers committed Jan 13, 2016 73 `````` * intros c n k; rewrite /= (conv_compl (tower_chain c k) n). `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 83 ``````Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed. `````` Robbert Krebbers committed Nov 11, 2015 84 ``````Lemma f_tower {n k} (X : tower) : n ≤ k → f (X k) ={n}= X (S k). `````` Robbert Krebbers committed Jan 13, 2016 85 ``````Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 89 `````` by rewrite IH (f_tower X); last lia. `````` Robbert Krebbers committed Nov 11, 2015 90 91 ``````Qed. Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k. `````` Robbert Krebbers committed Jan 13, 2016 92 ``````Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 116 `````` [by rewrite coerce_id|by rewrite g_coerce IH]. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 123 `````` [by rewrite coerce_id|by rewrite coerce_f IH]. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 137 `````` rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf. `````` Robbert Krebbers committed Nov 11, 2015 138 `````` by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))). `````` Robbert Krebbers committed Jan 13, 2016 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 committed Nov 11, 2015 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 committed Jan 13, 2016 154 `````` * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 160 `````` * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 166 `````` * rewrite -(gg_tower i (j - i) X). `````` Robbert Krebbers committed Nov 11, 2015 167 `````` apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _). `````` Robbert Krebbers committed Jan 13, 2016 168 `````` * rewrite (ff_tower j (i-j) X); last lia. by destruct (Nat.sub_add _ _ _). `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 177 `````` rewrite Hk (f_tower X); last lia; rewrite f_S -map_comp. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 184 `````` by intros n X Y HXY; unfold unfold'; apply compl_ne; rewrite /= (HXY n). `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 192 `````` rewrite -(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g). `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 204 205 `````` { by rewrite coerce_id map_id. } rewrite map_comp g_coerce; apply IH. } `````` Robbert Krebbers committed Nov 11, 2015 206 `````` rewrite equiv_dist; intros n k; unfold unfold, fold; simpl. `````` Robbert Krebbers committed Jan 13, 2016 207 `````` rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) g). `````` Robbert Krebbers committed Nov 11, 2015 208 209 `````` transitivity (map (ff n, gg n) (X (S (n + k)))). { unfold unfold'; rewrite (conv_compl (unfold_chain X) n). `````` Robbert Krebbers committed Jan 13, 2016 210 211 `````` rewrite (chain_cauchy (unfold_chain X) n (n + k)) /=; last lia. rewrite (f_tower X); last lia; rewrite -map_comp. `````` Robbert Krebbers committed Nov 11, 2015 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 committed Jan 13, 2016 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 committed Nov 11, 2015 227 228 229 `````` apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia. Qed. End solver. `````` Robbert Krebbers committed Dec 15, 2015 230 `````` `````` Robbert Krebbers committed Jan 13, 2016 231 ``Global Opaque T fold unfold.``