(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "common/Errors.ma". include "common/IOMonad.ma". lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r. ! x ← m ; f x = return r → ∃x.m = return x ∧ f x = return r. #A #B * normalize [2:#x] #f #r #EQ destruct %{x} %{EQ} % qed. lemma bind_option_inversion_star: ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. (∀x.f = Some … x → g x = Some … y → P) → (! x ← f ; g x = Some … y) → P. #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed. interpretation "option bind inversion" 'bind_inversion = (bind_option_inversion_star ???????). lemma bind_inversion_star : ∀X,Y.∀P : Prop. ∀m : res X.∀f : X → res Y.∀v : Y. (∀x. m = return x → f x = return v → P) → ! x ← m ; f x = return v → P. #X #Y #P #m #f #v #H #G elim (bind_inversion ????? G) #x * @H qed. interpretation "res bind inversion" 'bind_inversion = (bind_inversion_star ???????). lemma IO_bind_inversion: ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. (∀x.f = return x → g x = return y → P) → (! x ← f ; g x = return y) → P. #O #I #A #B #P #f #g #y cases f normalize [ #o #f #_ #H destruct | #a #G #H @(G ? (refl …) H) | #e #_ #H destruct ] qed. interpretation "IO bind inversion" 'bind_inversion = (IO_bind_inversion ?????????). record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop) ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf)) ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n. m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) → m_frel ?? Q G (m_bind … m f) (m_bind … n g) ; 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 }. record MonadFunctRel1 (M1 : Monad) (M2 : Monad) : Type[1] ≝ { m_frel1 :5> ∀X,Y.(Y → X) → (M1 X → M2 Y → Prop) ; mfr_return1 : ∀X,Y,F,y.m_frel1 X Y F (return (F y)) (return y) ; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n → ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g) ; 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 }. definition res_preserve : MonadFunctRel Res Res ≝ mk_MonadFunctRel ?? (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) ???. [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % | #X #Y #Z #W #P #Q #F #G * [ #u | #e ] #n #H #f #g #K #x whd in ⊢ (??%%→?); #EQ destruct(EQ) cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) | #X #Y #P #F #G #H #u #v #K #x #EQ cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % ] qed. definition res_preserve1 : MonadFunctRel1 Res Res ≝ mk_MonadFunctRel1 ?? (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) ???. [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // | #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct cases(H x (refl …)) #y * #n_spec #x_spec cases(H1 y z ?) [2: n_spec L @(K ? prf ? EQ) | #X #Y #P #F #G #H #u #v #K #x #EQ cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % ] qed. definition opt_preserve1 : MonadFunctRel1 Option Option ≝ mk_MonadFunctRel1 ?? (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) ???. [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // | #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct cases(H x (refl …)) #y * #n_spec #x_spec cases(H1 y z ?) [2: n_spec L @(K ? prf ? EQ) | #X #Y #P #F #G #H #u #v #K #x #EQ cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % ] qed. definition io_preserve1 : ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝ λO,I.mk_MonadFunctRel1 ?? (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x) ???. [ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % // | #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct cases(H x (refl …)) #y * #n_spec #x_spec cases(H1 y z ?) [2: n_spec EQ @mfr_return qed. lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2. ∀X,Y,F,v,n. n = return F v → FR X Y F n (return v). #M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1 qed. lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. lemma opt_preserve_none1 : ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n. #X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed. lemma m_list_map_All_ok : ∀M : MonadProps.∀X,Y,f,l. All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. #M #X #Y #f #l elim l -l [ * %{[ ]} % | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ' %{(y :: ys)} change with (! y ← ? ; ? = ?) >EQ >m_return_bind change with (! acc ← m_list_map ????? ; ? = ?) >EQ' @m_return_bind qed. lemma res_eq_from_opt : ∀A,m,a. res_to_opt A m = return a → m = return a. #A #m #a cases m #x normalize #EQ destruct(EQ) % qed. lemma res_to_opt_preserve : ∀X,Y,P,F,m,n. res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n). #X #Y #P #F #m #n #H #x #EQ cases (H x ?) [ #prf #EQ' %{prf} >EQ' % | cases m in EQ; normalize #x #EQ destruct % ] qed. lemma res_to_opt__preserve : ∀X,Y,F,m,n. res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n). #X #Y #F #m #n #H #x #EQ whd in H; cases (H x ?) [ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption] | cases m in EQ; normalize #x #EQ destruct % ] qed. lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. opt_preserve X Y P F m n → res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n). #X #Y #P #F #m #n #e1 #e2 #H #v #prf cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'} >EQ % qed. lemma opt_to_res_preserve1 : ∀X,Y,F,m,n,e1,e2. opt_preserve1 X Y F m n → res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n). #X #Y #F #m #n #e1 #e2 #H #x #EQ cases(H x ?) [ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption] | cases m in EQ; normalize [2: #x1] #EQ destruct % ] qed. lemma err_eq_from_io : ∀O,I,X,m,v. err_to_io O I X m = return v → m = return v. #O #I #X * #x #v normalize #EQ destruct % qed. lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n. res_preserve X Y P F m n → io_preserve O I X Y P F m n. #O #I #X #Y #P #F #m #n #H #v #prf cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'} >EQ % qed. lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n. res_preserve1 X Y F m n → io_preserve1 O I X Y F m n. #O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ)) #y * #y_spec #v_spec %{y} % // >y_spec % qed.