[2570] | 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 | }. |
---|
[2590] | 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) |
---|
[2801] | 71 | ; mfr_bind_inversion1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n → |
---|
| 72 | ∀f,g.(∀x.m = return F x → n = return x → m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g) |
---|
[2590] | 73 | ; 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 |
---|
| 74 | }. |
---|
[2570] | 75 | |
---|
[2590] | 76 | |
---|
[2570] | 77 | definition res_preserve : MonadFunctRel Res Res ≝ |
---|
| 78 | mk_MonadFunctRel ?? |
---|
| 79 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
---|
| 80 | ???. |
---|
| 81 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
---|
| 82 | | #X #Y #Z #W #P #Q #F #G * |
---|
| 83 | [ #u | #e ] #n #H #f #g #K #x |
---|
| 84 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 85 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
---|
| 86 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
---|
| 87 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
---|
| 88 | ] |
---|
| 89 | qed. |
---|
| 90 | |
---|
[2590] | 91 | definition res_preserve1 : MonadFunctRel1 Res Res ≝ |
---|
| 92 | mk_MonadFunctRel1 ?? |
---|
| 93 | (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) |
---|
[2801] | 94 | ????. |
---|
[2590] | 95 | [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // |
---|
| 96 | | #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 97 | cases(H x (refl …)) #y * #n_spec #x_spec |
---|
| 98 | cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w} |
---|
| 99 | >n_spec <w_spec % // |
---|
[2801] | 100 | | #X #Y #Z #W #F #G * [ #x | #e ] #n #H #f #g #H1 #z |
---|
| 101 | whd in ⊢ (??%% → ?); [2: #EQ destruct(EQ)] #H2 cases(H x (refl …)) |
---|
| 102 | #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption ] #w |
---|
| 103 | * #w_spec #EQz %{w} >n_spec <w_spec % // |
---|
[2590] | 104 | | #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} |
---|
| 105 | % // |
---|
| 106 | ] |
---|
| 107 | qed. |
---|
| 108 | |
---|
[2570] | 109 | definition opt_preserve : MonadFunctRel Option Option ≝ |
---|
| 110 | mk_MonadFunctRel ?? |
---|
| 111 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
---|
| 112 | ???. |
---|
| 113 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
---|
| 114 | | #X #Y #Z #W #P #Q #F #G * |
---|
| 115 | [ | #u ] #n #H #f #g #K #x |
---|
| 116 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 117 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
---|
| 118 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
---|
| 119 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
---|
| 120 | ] |
---|
| 121 | qed. |
---|
| 122 | |
---|
[2590] | 123 | definition opt_preserve1 : MonadFunctRel1 Option Option ≝ |
---|
| 124 | mk_MonadFunctRel1 ?? |
---|
| 125 | (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) |
---|
[2801] | 126 | ????. |
---|
[2590] | 127 | [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // |
---|
| 128 | | #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 129 | cases(H x (refl …)) #y * #n_spec #x_spec |
---|
| 130 | cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w} |
---|
| 131 | >n_spec <w_spec % // |
---|
[2801] | 132 | | #X #Y #Z #W #F #G * [ | #x ] #n #H #f #g #H1 #z |
---|
| 133 | whd in ⊢ (??%% → ?); [ #EQ destruct(EQ)] #H2 cases(H x (refl …)) |
---|
| 134 | #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w |
---|
| 135 | * #w_spec #EQz %{w} >n_spec <w_spec % // |
---|
[2590] | 136 | | #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} |
---|
| 137 | % // |
---|
| 138 | ] |
---|
| 139 | qed. |
---|
| 140 | |
---|
[2570] | 141 | definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ |
---|
| 142 | λO,I.mk_MonadFunctRel ?? |
---|
| 143 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
---|
| 144 | ???. |
---|
| 145 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
---|
| 146 | | #X #Y #Z #W #P #Q #F #G * |
---|
| 147 | [ #o #f | #u | #e ] #n #H #f #g #K #x |
---|
| 148 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 149 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
---|
| 150 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
---|
| 151 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
---|
| 152 | ] |
---|
| 153 | qed. |
---|
| 154 | |
---|
[2590] | 155 | definition io_preserve1 : ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝ |
---|
| 156 | λO,I.mk_MonadFunctRel1 ?? |
---|
| 157 | (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) |
---|
[2801] | 158 | ????. |
---|
[2590] | 159 | [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // |
---|
| 160 | | #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 161 | cases(H x (refl …)) #y * #n_spec #x_spec |
---|
| 162 | cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w} |
---|
| 163 | >n_spec <w_spec % // |
---|
[2801] | 164 | | #X #Y #Z #W #F #G * [ #o #r | #x | #e ] #n #H #f #g #H1 #z |
---|
| 165 | whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(H x (refl …)) |
---|
| 166 | #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w |
---|
| 167 | * #w_spec #EQz %{w} >n_spec <w_spec % // |
---|
[2590] | 168 | | #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} |
---|
| 169 | % // |
---|
| 170 | ] |
---|
| 171 | qed. |
---|
| 172 | |
---|
[2570] | 173 | definition preserving ≝ |
---|
| 174 | λM1,M2.λFR : MonadFunctRel M1 M2. |
---|
| 175 | λX,Y,A,B : Type[0]. |
---|
| 176 | λP : X → Prop. |
---|
| 177 | λQ : A → Prop. |
---|
| 178 | λF : ∀x : X.P x → Y. |
---|
| 179 | λG : ∀a : A.Q a → B. |
---|
| 180 | λf : X → M1 A. |
---|
| 181 | λg : Y → M2 B. |
---|
| 182 | ∀x,prf. |
---|
| 183 | FR … G |
---|
| 184 | (f x) (g (F x prf)). |
---|
| 185 | |
---|
[2590] | 186 | definition preserving1 ≝ |
---|
| 187 | λM1,M2.λFR : MonadFunctRel1 M1 M2. |
---|
| 188 | λX,Y,A,B : Type[0]. |
---|
| 189 | λF : Y → X. |
---|
| 190 | λG : B → A. |
---|
| 191 | λf : X → M1 A. |
---|
| 192 | λg : Y → M2 B. |
---|
| 193 | ∀ y. |
---|
| 194 | FR ?? G (f (F y)) (g y). |
---|
| 195 | |
---|
[2570] | 196 | definition preserving2 ≝ |
---|
| 197 | λM1,M2.λFR : MonadFunctRel M1 M2. |
---|
| 198 | λX,Y,Z,W,A,B : Type[0]. |
---|
| 199 | λP : X → Prop. |
---|
| 200 | λQ : Y → Prop. |
---|
| 201 | λR : A → Prop. |
---|
| 202 | λF : ∀x : X.P x → Z. |
---|
| 203 | λG : ∀y : Y.Q y → W. |
---|
| 204 | λH : ∀a : A.R a → B. |
---|
| 205 | λf : X → Y → M1 A. |
---|
| 206 | λg : Z → W → M2 B. |
---|
| 207 | ∀x,y,prf1,prf2. |
---|
| 208 | FR … H |
---|
| 209 | (f x y) (g (F x prf1) (G y prf2)). |
---|
[2590] | 210 | |
---|
| 211 | definition preserving21 ≝ |
---|
| 212 | λM1,M2.λFR : MonadFunctRel1 M1 M2. |
---|
| 213 | λX,Y,Z,W,A,B : Type[0]. |
---|
| 214 | λF : Z → X. |
---|
| 215 | λG : W → Y. |
---|
| 216 | λH : B → A. |
---|
| 217 | λf : X → Y → M1 A. |
---|
| 218 | λg : Z → W → M2 B. |
---|
| 219 | ∀z,w. FR ?? H (f (F z) (G w)) (g z w). |
---|
| 220 | |
---|
[2570] | 221 | lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. |
---|
| 222 | #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
| 223 | |
---|
[2590] | 224 | lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n. |
---|
| 225 | #X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
| 226 | |
---|
[2570] | 227 | lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. |
---|
| 228 | ∀X,Y,P,F,v,n. |
---|
| 229 | ∀prf.n = return F v prf → |
---|
| 230 | FR X Y P F (return v) n. |
---|
| 231 | #M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed. |
---|
| 232 | |
---|
[2590] | 233 | lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2. |
---|
| 234 | ∀X,Y,F,v,n. |
---|
| 235 | n = return F v → |
---|
| 236 | FR X Y F n (return v). |
---|
| 237 | #M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1 |
---|
| 238 | qed. |
---|
| 239 | |
---|
[2570] | 240 | lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. |
---|
| 241 | #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. |
---|
| 242 | |
---|
| 243 | lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. |
---|
| 244 | #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
| 245 | |
---|
[2590] | 246 | lemma opt_preserve_none1 : ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n. |
---|
| 247 | #X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed. |
---|
| 248 | |
---|
[2570] | 249 | lemma m_list_map_All_ok : |
---|
| 250 | ∀M : MonadProps.∀X,Y,f,l. |
---|
| 251 | All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. |
---|
| 252 | #M #X #Y #f #l elim l -l |
---|
| 253 | [ * %{[ ]} % |
---|
| 254 | | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ' |
---|
| 255 | %{(y :: ys)} |
---|
| 256 | change with (! y ← ? ; ? = ?) |
---|
| 257 | >EQ >m_return_bind |
---|
| 258 | change with (! acc ← m_list_map ????? ; ? = ?) >EQ' |
---|
| 259 | @m_return_bind |
---|
| 260 | qed. |
---|
| 261 | |
---|
| 262 | lemma res_eq_from_opt : ∀A,m,a. |
---|
| 263 | res_to_opt A m = return a → m = return a. |
---|
| 264 | #A #m #a cases m #x normalize #EQ destruct(EQ) % |
---|
| 265 | qed. |
---|
| 266 | |
---|
| 267 | lemma res_to_opt_preserve : ∀X,Y,P,F,m,n. |
---|
| 268 | res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n). |
---|
| 269 | #X #Y #P #F #m #n #H #x #EQ |
---|
| 270 | cases (H x ?) |
---|
| 271 | [ #prf #EQ' %{prf} >EQ' % |
---|
| 272 | | cases m in EQ; normalize #x #EQ destruct % |
---|
| 273 | ] |
---|
| 274 | qed. |
---|
| 275 | |
---|
[2590] | 276 | lemma res_to_opt__preserve : ∀X,Y,F,m,n. |
---|
| 277 | res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n). |
---|
| 278 | #X #Y #F #m #n #H #x #EQ |
---|
| 279 | whd in H; cases (H x ?) |
---|
| 280 | [ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption] |
---|
| 281 | | cases m in EQ; normalize #x #EQ destruct % |
---|
| 282 | ] |
---|
| 283 | qed. |
---|
| 284 | |
---|
[2570] | 285 | lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. |
---|
| 286 | opt_preserve X Y P F m n → |
---|
| 287 | res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n). |
---|
| 288 | #X #Y #P #F #m #n #e1 #e2 #H #v #prf |
---|
| 289 | cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'} |
---|
| 290 | >EQ % |
---|
| 291 | qed. |
---|
| 292 | |
---|
[2590] | 293 | lemma opt_to_res_preserve1 : ∀X,Y,F,m,n,e1,e2. |
---|
| 294 | opt_preserve1 X Y F m n → |
---|
| 295 | res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n). |
---|
| 296 | #X #Y #F #m #n #e1 #e2 #H #x #EQ |
---|
| 297 | cases(H x ?) |
---|
| 298 | [ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption] |
---|
| 299 | | cases m in EQ; normalize [2: #x1] #EQ destruct % |
---|
| 300 | ] |
---|
| 301 | qed. |
---|
| 302 | |
---|
[2570] | 303 | lemma err_eq_from_io : ∀O,I,X,m,v. |
---|
| 304 | err_to_io O I X m = return v → m = return v. |
---|
| 305 | #O #I #X * #x #v normalize #EQ destruct % qed. |
---|
| 306 | |
---|
| 307 | lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n. |
---|
| 308 | res_preserve X Y P F m n → |
---|
| 309 | io_preserve O I X Y P F m n. |
---|
| 310 | #O #I #X #Y #P #F #m #n #H #v #prf |
---|
| 311 | cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'} |
---|
| 312 | >EQ % |
---|
| 313 | qed. |
---|
| 314 | |
---|
[2590] | 315 | lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n. |
---|
| 316 | res_preserve1 X Y F m n → |
---|
| 317 | io_preserve1 O I X Y F m n. |
---|
| 318 | #O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ)) |
---|
| 319 | #y * #y_spec #v_spec %{y} % // >y_spec % |
---|
[2783] | 320 | qed. |
---|
| 321 | |
---|
| 322 | lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') → |
---|
| 323 | res_preserve1 X Y F n (Error … e). |
---|
| 324 | #X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1 |
---|
| 325 | qed. |
---|