| 1 | (**************************************************************************) |
|---|
| 2 | (* ___ *) |
|---|
| 3 | (* ||M|| *) |
|---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
|---|
| 5 | (* ||T|| *) |
|---|
| 6 | (* ||I|| Developers: *) |
|---|
| 7 | (* ||T|| The HELM team. *) |
|---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
|---|
| 9 | (* \ / *) |
|---|
| 10 | (* \ / This file is distributed under the terms of the *) |
|---|
| 11 | (* v GNU General Public License Version 2 *) |
|---|
| 12 | (* *) |
|---|
| 13 | (**************************************************************************) |
|---|
| 14 | |
|---|
| 15 | include "common/Errors.ma". |
|---|
| 16 | include "common/IOMonad.ma". |
|---|
| 17 | |
|---|
| 18 | lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r. |
|---|
| 19 | ! x ← m ; f x = return r → |
|---|
| 20 | ∃x.m = return x ∧ f x = return r. |
|---|
| 21 | #A #B * normalize [2:#x] #f #r #EQ destruct |
|---|
| 22 | %{x} %{EQ} % |
|---|
| 23 | qed. |
|---|
| 24 | |
|---|
| 25 | lemma bind_option_inversion_star: |
|---|
| 26 | ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. |
|---|
| 27 | (∀x.f = Some … x → g x = Some … y → P) → |
|---|
| 28 | (! x ← f ; g x = Some … y) → P. |
|---|
| 29 | #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed. |
|---|
| 30 | |
|---|
| 31 | interpretation "option bind inversion" 'bind_inversion = |
|---|
| 32 | (bind_option_inversion_star ???????). |
|---|
| 33 | |
|---|
| 34 | lemma bind_inversion_star : ∀X,Y.∀P : Prop. |
|---|
| 35 | ∀m : res X.∀f : X → res Y.∀v : Y. |
|---|
| 36 | (∀x. m = return x → f x = return v → P) → |
|---|
| 37 | ! x ← m ; f x = return v → P. |
|---|
| 38 | #X #Y #P #m #f #v #H #G |
|---|
| 39 | elim (bind_inversion ????? G) #x * @H qed. |
|---|
| 40 | |
|---|
| 41 | interpretation "res bind inversion" 'bind_inversion = |
|---|
| 42 | (bind_inversion_star ???????). |
|---|
| 43 | |
|---|
| 44 | lemma IO_bind_inversion: |
|---|
| 45 | ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. |
|---|
| 46 | (∀x.f = return x → g x = return y → P) → |
|---|
| 47 | (! x ← f ; g x = return y) → P. |
|---|
| 48 | #O #I #A #B #P #f #g #y cases f normalize |
|---|
| 49 | [ #o #f #_ #H destruct |
|---|
| 50 | | #a #G #H @(G ? (refl …) H) |
|---|
| 51 | | #e #_ #H destruct |
|---|
| 52 | ] qed. |
|---|
| 53 | |
|---|
| 54 | interpretation "IO bind inversion" 'bind_inversion = |
|---|
| 55 | (IO_bind_inversion ?????????). |
|---|
| 56 | |
|---|
| 57 | record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ |
|---|
| 58 | { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop) |
|---|
| 59 | ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf)) |
|---|
| 60 | ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n. |
|---|
| 61 | m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) → |
|---|
| 62 | m_frel ?? Q G (m_bind … m f) (m_bind … n g) |
|---|
| 63 | ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v |
|---|
| 64 | }. |
|---|
| 65 | |
|---|
| 66 | record MonadFunctRel1 (M1 : Monad) (M2 : Monad) : Type[1] ≝ |
|---|
| 67 | { m_frel1 :5> ∀X,Y.(Y → X) → (M1 X → M2 Y → Prop) |
|---|
| 68 | ; mfr_return1 : ∀X,Y,F,y.m_frel1 X Y F (return (F y)) (return y) |
|---|
| 69 | ; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n → |
|---|
| 70 | ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g) |
|---|
| 71 | ; m_frel_ext1 : ∀X,Y,F,G.(∀x.F x = G x) → ∀ u,v.m_frel1 X Y F u v → m_frel1 X Y G u v |
|---|
| 72 | }. |
|---|
| 73 | |
|---|
| 74 | |
|---|
| 75 | definition res_preserve : MonadFunctRel Res Res ≝ |
|---|
| 76 | mk_MonadFunctRel ?? |
|---|
| 77 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
|---|
| 78 | ???. |
|---|
| 79 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
|---|
| 80 | | #X #Y #Z #W #P #Q #F #G * |
|---|
| 81 | [ #u | #e ] #n #H #f #g #K #x |
|---|
| 82 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
|---|
| 83 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
|---|
| 84 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
|---|
| 85 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
|---|
| 86 | ] |
|---|
| 87 | qed. |
|---|
| 88 | |
|---|
| 89 | definition res_preserve1 : MonadFunctRel1 Res Res ≝ |
|---|
| 90 | mk_MonadFunctRel1 ?? |
|---|
| 91 | (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) |
|---|
| 92 | ???. |
|---|
| 93 | [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // |
|---|
| 94 | | #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct |
|---|
| 95 | cases(H x (refl …)) #y * #n_spec #x_spec |
|---|
| 96 | cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w} |
|---|
| 97 | >n_spec <w_spec % // |
|---|
| 98 | | #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} |
|---|
| 99 | % // |
|---|
| 100 | ] |
|---|
| 101 | qed. |
|---|
| 102 | |
|---|
| 103 | definition opt_preserve : MonadFunctRel Option Option ≝ |
|---|
| 104 | mk_MonadFunctRel ?? |
|---|
| 105 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
|---|
| 106 | ???. |
|---|
| 107 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
|---|
| 108 | | #X #Y #Z #W #P #Q #F #G * |
|---|
| 109 | [ | #u ] #n #H #f #g #K #x |
|---|
| 110 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
|---|
| 111 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
|---|
| 112 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
|---|
| 113 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
|---|
| 114 | ] |
|---|
| 115 | qed. |
|---|
| 116 | |
|---|
| 117 | definition opt_preserve1 : MonadFunctRel1 Option Option ≝ |
|---|
| 118 | mk_MonadFunctRel1 ?? |
|---|
| 119 | (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) |
|---|
| 120 | ???. |
|---|
| 121 | [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // |
|---|
| 122 | | #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct |
|---|
| 123 | cases(H x (refl …)) #y * #n_spec #x_spec |
|---|
| 124 | cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w} |
|---|
| 125 | >n_spec <w_spec % // |
|---|
| 126 | | #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} |
|---|
| 127 | % // |
|---|
| 128 | ] |
|---|
| 129 | qed. |
|---|
| 130 | |
|---|
| 131 | definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ |
|---|
| 132 | λO,I.mk_MonadFunctRel ?? |
|---|
| 133 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
|---|
| 134 | ???. |
|---|
| 135 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
|---|
| 136 | | #X #Y #Z #W #P #Q #F #G * |
|---|
| 137 | [ #o #f | #u | #e ] #n #H #f #g #K #x |
|---|
| 138 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
|---|
| 139 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
|---|
| 140 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
|---|
| 141 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
|---|
| 142 | ] |
|---|
| 143 | qed. |
|---|
| 144 | |
|---|
| 145 | definition io_preserve1 : ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝ |
|---|
| 146 | λO,I.mk_MonadFunctRel1 ?? |
|---|
| 147 | (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) |
|---|
| 148 | ???. |
|---|
| 149 | [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // |
|---|
| 150 | | #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct |
|---|
| 151 | cases(H x (refl …)) #y * #n_spec #x_spec |
|---|
| 152 | cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w} |
|---|
| 153 | >n_spec <w_spec % // |
|---|
| 154 | | #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} |
|---|
| 155 | % // |
|---|
| 156 | ] |
|---|
| 157 | qed. |
|---|
| 158 | |
|---|
| 159 | definition preserving ≝ |
|---|
| 160 | λM1,M2.λFR : MonadFunctRel M1 M2. |
|---|
| 161 | λX,Y,A,B : Type[0]. |
|---|
| 162 | λP : X → Prop. |
|---|
| 163 | λQ : A → Prop. |
|---|
| 164 | λF : ∀x : X.P x → Y. |
|---|
| 165 | λG : ∀a : A.Q a → B. |
|---|
| 166 | λf : X → M1 A. |
|---|
| 167 | λg : Y → M2 B. |
|---|
| 168 | ∀x,prf. |
|---|
| 169 | FR … G |
|---|
| 170 | (f x) (g (F x prf)). |
|---|
| 171 | |
|---|
| 172 | definition preserving1 ≝ |
|---|
| 173 | λM1,M2.λFR : MonadFunctRel1 M1 M2. |
|---|
| 174 | λX,Y,A,B : Type[0]. |
|---|
| 175 | λF : Y → X. |
|---|
| 176 | λG : B → A. |
|---|
| 177 | λf : X → M1 A. |
|---|
| 178 | λg : Y → M2 B. |
|---|
| 179 | ∀ y. |
|---|
| 180 | FR ?? G (f (F y)) (g y). |
|---|
| 181 | |
|---|
| 182 | definition preserving2 ≝ |
|---|
| 183 | λM1,M2.λFR : MonadFunctRel M1 M2. |
|---|
| 184 | λX,Y,Z,W,A,B : Type[0]. |
|---|
| 185 | λP : X → Prop. |
|---|
| 186 | λQ : Y → Prop. |
|---|
| 187 | λR : A → Prop. |
|---|
| 188 | λF : ∀x : X.P x → Z. |
|---|
| 189 | λG : ∀y : Y.Q y → W. |
|---|
| 190 | λH : ∀a : A.R a → B. |
|---|
| 191 | λf : X → Y → M1 A. |
|---|
| 192 | λg : Z → W → M2 B. |
|---|
| 193 | ∀x,y,prf1,prf2. |
|---|
| 194 | FR … H |
|---|
| 195 | (f x y) (g (F x prf1) (G y prf2)). |
|---|
| 196 | |
|---|
| 197 | definition preserving21 ≝ |
|---|
| 198 | λM1,M2.λFR : MonadFunctRel1 M1 M2. |
|---|
| 199 | λX,Y,Z,W,A,B : Type[0]. |
|---|
| 200 | λF : Z → X. |
|---|
| 201 | λG : W → Y. |
|---|
| 202 | λH : B → A. |
|---|
| 203 | λf : X → Y → M1 A. |
|---|
| 204 | λg : Z → W → M2 B. |
|---|
| 205 | ∀z,w. FR ?? H (f (F z) (G w)) (g z w). |
|---|
| 206 | |
|---|
| 207 | lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. |
|---|
| 208 | #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
|---|
| 209 | |
|---|
| 210 | lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n. |
|---|
| 211 | #X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
|---|
| 212 | |
|---|
| 213 | lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. |
|---|
| 214 | ∀X,Y,P,F,v,n. |
|---|
| 215 | ∀prf.n = return F v prf → |
|---|
| 216 | FR X Y P F (return v) n. |
|---|
| 217 | #M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed. |
|---|
| 218 | |
|---|
| 219 | lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2. |
|---|
| 220 | ∀X,Y,F,v,n. |
|---|
| 221 | n = return F v → |
|---|
| 222 | FR X Y F n (return v). |
|---|
| 223 | #M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1 |
|---|
| 224 | qed. |
|---|
| 225 | |
|---|
| 226 | lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. |
|---|
| 227 | #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. |
|---|
| 228 | |
|---|
| 229 | lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. |
|---|
| 230 | #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
|---|
| 231 | |
|---|
| 232 | lemma opt_preserve_none1 : ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n. |
|---|
| 233 | #X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed. |
|---|
| 234 | |
|---|
| 235 | lemma m_list_map_All_ok : |
|---|
| 236 | ∀M : MonadProps.∀X,Y,f,l. |
|---|
| 237 | All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. |
|---|
| 238 | #M #X #Y #f #l elim l -l |
|---|
| 239 | [ * %{[ ]} % |
|---|
| 240 | | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ' |
|---|
| 241 | %{(y :: ys)} |
|---|
| 242 | change with (! y ← ? ; ? = ?) |
|---|
| 243 | >EQ >m_return_bind |
|---|
| 244 | change with (! acc ← m_list_map ????? ; ? = ?) >EQ' |
|---|
| 245 | @m_return_bind |
|---|
| 246 | qed. |
|---|
| 247 | |
|---|
| 248 | lemma res_eq_from_opt : ∀A,m,a. |
|---|
| 249 | res_to_opt A m = return a → m = return a. |
|---|
| 250 | #A #m #a cases m #x normalize #EQ destruct(EQ) % |
|---|
| 251 | qed. |
|---|
| 252 | |
|---|
| 253 | lemma res_to_opt_preserve : ∀X,Y,P,F,m,n. |
|---|
| 254 | res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n). |
|---|
| 255 | #X #Y #P #F #m #n #H #x #EQ |
|---|
| 256 | cases (H x ?) |
|---|
| 257 | [ #prf #EQ' %{prf} >EQ' % |
|---|
| 258 | | cases m in EQ; normalize #x #EQ destruct % |
|---|
| 259 | ] |
|---|
| 260 | qed. |
|---|
| 261 | |
|---|
| 262 | lemma res_to_opt__preserve : ∀X,Y,F,m,n. |
|---|
| 263 | res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n). |
|---|
| 264 | #X #Y #F #m #n #H #x #EQ |
|---|
| 265 | whd in H; cases (H x ?) |
|---|
| 266 | [ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption] |
|---|
| 267 | | cases m in EQ; normalize #x #EQ destruct % |
|---|
| 268 | ] |
|---|
| 269 | qed. |
|---|
| 270 | |
|---|
| 271 | lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. |
|---|
| 272 | opt_preserve X Y P F m n → |
|---|
| 273 | res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n). |
|---|
| 274 | #X #Y #P #F #m #n #e1 #e2 #H #v #prf |
|---|
| 275 | cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'} |
|---|
| 276 | >EQ % |
|---|
| 277 | qed. |
|---|
| 278 | |
|---|
| 279 | lemma opt_to_res_preserve1 : ∀X,Y,F,m,n,e1,e2. |
|---|
| 280 | opt_preserve1 X Y F m n → |
|---|
| 281 | res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n). |
|---|
| 282 | #X #Y #F #m #n #e1 #e2 #H #x #EQ |
|---|
| 283 | cases(H x ?) |
|---|
| 284 | [ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption] |
|---|
| 285 | | cases m in EQ; normalize [2: #x1] #EQ destruct % |
|---|
| 286 | ] |
|---|
| 287 | qed. |
|---|
| 288 | |
|---|
| 289 | lemma err_eq_from_io : ∀O,I,X,m,v. |
|---|
| 290 | err_to_io O I X m = return v → m = return v. |
|---|
| 291 | #O #I #X * #x #v normalize #EQ destruct % qed. |
|---|
| 292 | |
|---|
| 293 | lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n. |
|---|
| 294 | res_preserve X Y P F m n → |
|---|
| 295 | io_preserve O I X Y P F m n. |
|---|
| 296 | #O #I #X #Y #P #F #m #n #H #v #prf |
|---|
| 297 | cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'} |
|---|
| 298 | >EQ % |
|---|
| 299 | qed. |
|---|
| 300 | |
|---|
| 301 | lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n. |
|---|
| 302 | res_preserve1 X Y F m n → |
|---|
| 303 | io_preserve1 O I X Y F m n. |
|---|
| 304 | #O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ)) |
|---|
| 305 | #y * #y_spec #v_spec %{y} % // >y_spec % |
|---|
| 306 | qed. |
|---|
