cofe_solver.v 10.1 KB
 Ralf Jung committed Nov 22, 2016 1 ``````From iris.algebra Require Export ofe. `````` 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Nov 11, 2015 3 `````` `````` Robbert Krebbers committed Jun 16, 2019 4 ``````Record solution (F : oFunctor) := Solution { `````` Ralf Jung committed Nov 22, 2016 5 6 `````` solution_car :> ofeT; solution_cofe : Cofe solution_car; `````` Robbert Krebbers committed Apr 01, 2020 7 `````` solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car; `````` Robbert Krebbers committed Jan 14, 2016 8 ``````}. `````` Ralf Jung committed Nov 22, 2016 9 ``````Existing Instance solution_cofe. `````` Robbert Krebbers committed Jan 14, 2016 10 11 `````` Module solver. Section solver. `````` Robbert Krebbers committed Jun 16, 2019 12 ``````Context (F : oFunctor) `{Fcontr : oFunctorContractive F}. `````` Robbert Krebbers committed Apr 01, 2020 13 14 ``````Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (oFunctor_apply F T)}. Context `{Finh : Inhabited (oFunctor_apply F unitO)}. `````` Robbert Krebbers committed Jun 16, 2019 15 ``````Notation map := (oFunctor_map F). `````` Robbert Krebbers committed Nov 11, 2015 16 `````` `````` Robbert Krebbers committed Jun 04, 2019 17 18 ``````Fixpoint A' (k : nat) : { C : ofeT & Cofe C } := match k with `````` Robbert Krebbers committed Jun 16, 2019 19 `````` | 0 => existT (P:=Cofe) unitO _ `````` Robbert Krebbers committed Apr 01, 2020 20 `````` | S k => existT (P:=Cofe) (@oFunctor_apply F (projT1 (A' k)) (projT2 (A' k))) _ `````` Robbert Krebbers committed Jun 04, 2019 21 22 23 24 `````` end. Notation A k := (projT1 (A' k)). Local Instance A_cofe k : Cofe (A k) := projT2 (A' k). `````` Robbert Krebbers committed Feb 10, 2016 25 ``````Fixpoint f (k : nat) : A k -n> A (S k) := `````` Robbert Krebbers committed Jun 16, 2019 26 `````` match k with 0 => OfeMor (λ _, inhabitant) | S k => map (g k,f k) end `````` Robbert Krebbers committed Feb 10, 2016 27 ``````with g (k : nat) : A (S k) -n> A k := `````` Robbert Krebbers committed Jun 16, 2019 28 `````` match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end. `````` Robbert Krebbers committed Feb 10, 2016 29 30 31 32 33 34 ``````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 f : simpl never. Arguments g : simpl never. Lemma gf {k} (x : A k) : g k (f k x) ≡ x. `````` 35 ``````Proof using Fcontr. `````` Robbert Krebbers committed Nov 11, 2015 36 `````` induction k as [|k IH]; simpl in *; [by destruct x|]. `````` Robbert Krebbers committed Apr 02, 2020 37 38 `````` rewrite -oFunctor_map_compose -{2}[x]oFunctor_map_id. by apply (contractive_proper map). `````` Robbert Krebbers committed Nov 11, 2015 39 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 40 ``````Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x. `````` 41 ``````Proof using Fcontr. `````` Robbert Krebbers committed Feb 10, 2016 42 `````` induction k as [|k IH]; simpl. `````` Robbert Krebbers committed Apr 02, 2020 43 `````` - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose. `````` Robbert Krebbers committed Mar 02, 2016 44 `````` apply (contractive_0 map). `````` Robbert Krebbers committed Apr 02, 2020 45 `````` - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose. `````` Robbert Krebbers committed Mar 02, 2016 46 `````` by apply (contractive_S map). `````` Robbert Krebbers committed Nov 11, 2015 47 48 49 50 ``````Qed. Record tower := { tower_car k :> A k; `````` Robbert Krebbers committed Feb 10, 2016 51 `````` g_tower k : g k (tower_car (S k)) ≡ tower_car k `````` Robbert Krebbers committed Nov 11, 2015 52 53 ``````}. Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k. `````` Ralf Jung committed Feb 10, 2016 54 ``````Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k. `````` Ralf Jung committed Nov 22, 2016 55 ``````Definition tower_ofe_mixin : OfeMixin tower. `````` Robbert Krebbers committed Nov 11, 2015 56 57 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 58 `````` - intros X Y; split; [by intros HXY n k; apply equiv_dist|]. `````` Robbert Krebbers committed Nov 11, 2015 59 `````` intros HXY k; apply equiv_dist; intros n; apply HXY. `````` Robbert Krebbers committed Feb 17, 2016 60 `````` - intros k; split. `````` Robbert Krebbers committed Nov 11, 2015 61 62 `````` + by intros X n. + by intros X Y ? n. `````` Ralf Jung committed Feb 20, 2016 63 `````` + by intros X Y Z ?? n; trans (Y n). `````` Robbert Krebbers committed Feb 17, 2016 64 `````` - intros k X Y HXY n; apply dist_S. `````` Robbert Krebbers committed Jan 13, 2016 65 `````` by rewrite -(g_tower X) (HXY (S n)) g_tower. `````` Robbert Krebbers committed Nov 11, 2015 66 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 ``````Definition T : ofeT := OfeT tower tower_ofe_mixin. Program Definition tower_chain (c : chain T) (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 Definition tower_compl : Compl T := λ c, {| tower_car n := compl (tower_chain c n) |}. Next Obligation. intros c k; apply equiv_dist=> n. by rewrite (conv_compl n (tower_chain c k)) (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k). Qed. Global Program Instance tower_cofe : Cofe T := { compl := tower_compl }. Next Obligation. intros n c k; rewrite /= (conv_compl n (tower_chain c k)). apply (chain_cauchy c); lia. Qed. `````` Robbert Krebbers committed Nov 11, 2015 84 85 `````` Fixpoint ff {k} (i : nat) : A k -n> A (i + k) := `````` Robbert Krebbers committed Feb 10, 2016 86 `````` match i with 0 => cid | S i => f (i + k) ◎ ff i end. `````` Robbert Krebbers committed Nov 11, 2015 87 ``````Fixpoint gg {k} (i : nat) : A (i + k) -n> A k := `````` Robbert Krebbers committed Feb 10, 2016 88 `````` match i with 0 => cid | S i => gg i ◎ g (i + k) end. `````` Robbert Krebbers committed Nov 11, 2015 89 ``````Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x. `````` 90 ``````Proof using Fcontr. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed. `````` Robbert Krebbers committed Feb 10, 2016 91 ``````Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)). `````` 92 ``````Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed. `````` Robbert Krebbers committed Feb 10, 2016 93 ``````Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k). `````` 94 ``````Proof using Fcontr. `````` Robbert Krebbers committed Nov 11, 2015 95 `````` intros; induction i as [|i IH]; simpl; [done|]. `````` Ralf Jung committed Jun 20, 2018 96 `````` by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last lia. `````` Robbert Krebbers committed Nov 11, 2015 97 98 ``````Qed. Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k. `````` Robbert Krebbers committed Jan 13, 2016 99 ``````Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed. `````` Robbert Krebbers committed Nov 11, 2015 100 `````` `````` Ralf Jung committed Jan 27, 2017 101 ``````Instance tower_car_ne k : NonExpansive (λ X, tower_car X k). `````` Robbert Krebbers committed Nov 11, 2015 102 ``````Proof. by intros X Y HX. Qed. `````` Robbert Krebbers committed Jun 16, 2019 103 ``````Definition project (k : nat) : T -n> A k := OfeMor (λ X : T, tower_car X k). `````` Robbert Krebbers committed Nov 11, 2015 104 105 106 107 108 109 110 111 112 `````` 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)) : `````` Robbert Krebbers committed Feb 10, 2016 113 `````` g j (coerce H x) = coerce (Nat.succ_inj _ _ H) (g k x). `````` Robbert Krebbers committed Nov 11, 2015 114 115 ``````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) : `````` Robbert Krebbers committed Feb 10, 2016 116 `````` coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x). `````` Robbert Krebbers committed Nov 11, 2015 117 ``````Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. `````` Robbert Krebbers committed Aug 08, 2016 118 ``````Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k), `````` Robbert Krebbers committed Nov 11, 2015 119 120 `````` gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)). Proof. `````` Robbert Krebbers committed Aug 08, 2016 121 `````` intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1. `````` Robbert Krebbers committed Feb 17, 2016 122 `````` induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=; `````` Robbert Krebbers committed Jan 13, 2016 123 `````` [by rewrite coerce_id|by rewrite g_coerce IH]. `````` Robbert Krebbers committed Nov 11, 2015 124 ``````Qed. `````` Robbert Krebbers committed Aug 08, 2016 125 ``````Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k), `````` Robbert Krebbers committed Nov 11, 2015 126 127 `````` coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)). Proof. `````` Robbert Krebbers committed Aug 08, 2016 128 `````` intros ? <- x. assert (i = i1 + i2) as -> by lia. `````` Robbert Krebbers committed Feb 17, 2016 129 `````` induction i1 as [|i1 IH]; simplify_eq/=; `````` Robbert Krebbers committed Jan 13, 2016 130 `````` [by rewrite coerce_id|by rewrite coerce_f IH]. `````` Robbert Krebbers committed Nov 11, 2015 131 132 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 133 ``````Definition embed_coerce {k} (i : nat) : A k -n> A i := `````` Robbert Krebbers committed Nov 11, 2015 134 135 136 137 `````` 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. `````` Robbert Krebbers committed Feb 10, 2016 138 139 ``````Lemma g_embed_coerce {k i} (x : A k) : g i (embed_coerce (S i) x) ≡ embed_coerce i x. `````` 140 ``````Proof using Fcontr. `````` Robbert Krebbers committed Feb 10, 2016 141 `````` unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl. `````` Robbert Krebbers committed Feb 17, 2016 142 143 144 `````` - symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl. - exfalso; lia. - assert (i = k) by lia; subst. `````` Robbert Krebbers committed Jan 13, 2016 145 `````` rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf. `````` Robbert Krebbers committed Nov 11, 2015 146 `````` by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))). `````` Robbert Krebbers committed Feb 17, 2016 147 `````` - assert (H : 1 + ((i - k) + k) = S i) by lia. `````` Robbert Krebbers committed Jan 13, 2016 148 `````` rewrite (ff_ff _ H) /= -{2}(gf (ff (i - k) x)) g_coerce. `````` Robbert Krebbers committed Nov 11, 2015 149 150 `````` by erewrite coerce_proper by done. Qed. `````` Robbert Krebbers committed Feb 10, 2016 151 152 153 ``````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. `````` Maxime Dénès committed Jan 24, 2019 154 ``````Instance: Params (@embed) 1 := {}. `````` Ralf Jung committed Jan 27, 2017 155 156 ``````Instance embed_ne k : NonExpansive (embed k). Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed. `````` Robbert Krebbers committed Jun 16, 2019 157 ``````Definition embed' (k : nat) : A k -n> T := OfeMor (embed k). `````` Robbert Krebbers committed Feb 10, 2016 158 ``````Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x. `````` Robbert Krebbers committed Nov 11, 2015 159 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 160 `````` rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce. `````` Robbert Krebbers committed Nov 11, 2015 161 `````` destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl. `````` Robbert Krebbers committed Feb 17, 2016 162 `````` - assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=. `````` Robbert Krebbers committed Nov 11, 2015 163 `````` by erewrite g_coerce, gf, coerce_proper by done. `````` Robbert Krebbers committed Feb 17, 2016 164 `````` - assert (S k = 0 + (0 + i)) as H by lia. `````` Robbert Krebbers committed Feb 17, 2016 165 `````` rewrite (gg_gg _ H); simplify_eq/=. `````` Robbert Krebbers committed Nov 11, 2015 166 `````` by rewrite (ff_ff _ (eq_refl (1 + (0 + k)))). `````` Robbert Krebbers committed Feb 17, 2016 167 168 `````` - exfalso; lia. - assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=. `````` Robbert Krebbers committed Nov 11, 2015 169 170 `````` by erewrite coerce_proper by done. Qed. `````` Robbert Krebbers committed Feb 10, 2016 171 ``````Lemma embed_tower k (X : T) : embed (S k) (X (S k)) ≡{k}≡ X. `````` Robbert Krebbers committed Nov 11, 2015 172 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 173 174 `````` intros i; rewrite /= /embed_coerce. destruct (le_lt_dec i (S k)) as [H|H]; simpl. `````` Robbert Krebbers committed Feb 17, 2016 175 `````` - rewrite -(gg_tower i (S k - i) X). `````` Robbert Krebbers committed Nov 11, 2015 176 `````` apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _). `````` Robbert Krebbers committed Feb 17, 2016 177 `````` - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _). `````` Robbert Krebbers committed Nov 11, 2015 178 179 ``````Qed. `````` Robbert Krebbers committed Apr 01, 2020 180 ``````Program Definition unfold_chain (X : T) : chain (oFunctor_apply F T) := `````` Robbert Krebbers committed Feb 10, 2016 181 `````` {| chain_car n := map (project n,embed' n) (X (S n)) |}. `````` Robbert Krebbers committed Nov 11, 2015 182 183 184 ``````Next Obligation. intros X n i Hi. assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi. `````` Ralf Jung committed Feb 29, 2016 185 `````` induction k as [|k IH]; simpl; first done. `````` Robbert Krebbers committed Feb 10, 2016 186 `````` rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia. `````` Robbert Krebbers committed Apr 02, 2020 187 `````` rewrite f_S -oFunctor_map_compose. `````` Robbert Krebbers committed Feb 12, 2016 188 `````` by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f. `````` Robbert Krebbers committed Nov 11, 2015 189 ``````Qed. `````` Robbert Krebbers committed Apr 01, 2020 190 ``````Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X). `````` Ralf Jung committed Jan 27, 2017 191 ``````Instance unfold_ne : NonExpansive unfold. `````` Robbert Krebbers committed Feb 10, 2016 192 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 193 `````` intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X)) `````` Ralf Jung committed Feb 29, 2016 194 `````` (conv_compl n (unfold_chain Y)) /= (HXY (S n)). `````` Robbert Krebbers committed Feb 10, 2016 195 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 196 `````` `````` Robbert Krebbers committed Apr 01, 2020 197 ``````Program Definition fold (X : oFunctor_apply F T) : T := `````` Robbert Krebbers committed Feb 10, 2016 198 `````` {| tower_car n := g n (map (embed' n,project n) X) |}. `````` Robbert Krebbers committed Nov 11, 2015 199 ``````Next Obligation. `````` Robbert Krebbers committed Feb 10, 2016 200 `````` intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)). `````` Robbert Krebbers committed Apr 02, 2020 201 `````` rewrite g_S -oFunctor_map_compose. `````` Robbert Krebbers committed Feb 12, 2016 202 `````` apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower]. `````` Robbert Krebbers committed Nov 11, 2015 203 ``````Qed. `````` Ralf Jung committed Jan 27, 2017 204 ``````Instance fold_ne : NonExpansive fold. `````` Robbert Krebbers committed Jan 14, 2016 205 ``````Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed. `````` Robbert Krebbers committed Nov 11, 2015 206 `````` `````` Robbert Krebbers committed Jan 14, 2016 207 ``````Theorem result : solution F. `````` Ralf Jung committed Jan 05, 2017 208 ``````Proof using Type*. `````` Robbert Krebbers committed Apr 01, 2020 209 `````` refine (Solution F T _ (OfeIso (OfeMor fold) (OfeMor unfold) _ _)). `````` Robbert Krebbers committed Mar 02, 2016 210 `````` - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=. `````` Robbert Krebbers committed Feb 10, 2016 211 `````` rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)). `````` Ralf Jung committed Feb 20, 2016 212 `````` trans (map (ff n, gg n) (X (S (n + k)))). `````` Robbert Krebbers committed Feb 18, 2016 213 `````` { rewrite /unfold (conv_compl n (unfold_chain X)). `````` Robbert Krebbers committed Feb 10, 2016 214 215 `````` rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia. rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia. `````` Robbert Krebbers committed Apr 02, 2020 216 `````` rewrite f_S -!oFunctor_map_compose; apply (contractive_ne map); split=> Y. `````` Robbert Krebbers committed Feb 10, 2016 217 218 219 220 221 222 223 224 225 `````` + 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. `````` Robbert Krebbers committed Apr 02, 2020 226 227 `````` { by rewrite coerce_id oFunctor_map_id. } rewrite oFunctor_map_compose g_coerce; apply IH. } `````` Robbert Krebbers committed Feb 10, 2016 228 229 `````` assert (H: S n + k = n + S k) by lia. rewrite (map_ff_gg _ _ _ H). `````` Robbert Krebbers committed Jan 14, 2016 230 `````` apply (_ : Proper (_ ==> _) (gg _)); by destruct H. `````` Robbert Krebbers committed Feb 17, 2016 231 `````` - intros X; rewrite equiv_dist=> n /=. `````` Ralf Jung committed Feb 29, 2016 232 `````` rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=. `````` Robbert Krebbers committed Apr 02, 2020 233 `````` rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id. `````` Robbert Krebbers committed Feb 12, 2016 234 `````` apply (contractive_ne map); split => Y /=. `````` Ralf Jung committed Feb 29, 2016 235 `````` + rewrite f_tower. apply dist_S. by rewrite embed_tower. `````` Ralf Jung committed Feb 20, 2016 236 `````` + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower]. `````` Robbert Krebbers committed Nov 11, 2015 237 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 238 ``End solver. End solver.``