(**************************************************************************)
(*       ___                                                              *)
(*      ||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: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
  >n_spec <w_spec % //
| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
  % //
]
qed.

definition opt_preserve : MonadFunctRel Option Option ≝
  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 ] #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 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: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
  >n_spec <w_spec % //
| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
  % //
]
qed.

definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
  λO,I.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 *
  [ #o #f | #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 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: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
  >n_spec <w_spec % //
| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
  % //
]
qed.

definition preserving ≝
  λM1,M2.λFR : MonadFunctRel M1 M2.
  λX,Y,A,B : Type[0].
  λP : X → Prop.
  λQ : A → Prop.
  λF : ∀x : X.P x → Y.
  λG : ∀a : A.Q a → B.
  λf : X → M1 A.
  λg : Y → M2 B.
  ∀x,prf.
  FR … G
    (f x) (g (F x prf)).

definition preserving1 ≝   
  λM1,M2.λFR : MonadFunctRel1 M1 M2.
  λX,Y,A,B : Type[0].
  λF : Y → X.
  λG : B → A.
  λf : X → M1 A.
  λg : Y → M2 B. 
  ∀ y.
  FR ?? G (f (F y)) (g y).

definition preserving2 ≝
  λM1,M2.λFR : MonadFunctRel M1 M2.
  λX,Y,Z,W,A,B : Type[0].
  λP : X → Prop.
  λQ : Y → Prop.
  λR : A → Prop.
  λF : ∀x : X.P x → Z.
  λG : ∀y : Y.Q y → W.
  λH : ∀a : A.R a → B.
  λf : X → Y → M1 A.
  λg : Z → W → M2 B.
  ∀x,y,prf1,prf2.
  FR … H
    (f x y) (g (F x prf1) (G y prf2)).
    
definition preserving21 ≝ 
   λM1,M2.λFR : MonadFunctRel1 M1 M2.
   λX,Y,Z,W,A,B : Type[0].
   λF : Z → X.
   λG : W → Y.
   λH : B → A.
   λf : X → Y → M1 A.
   λg : Z → W → M2 B.
   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
   
lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.

lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. 

lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
∀X,Y,P,F,v,n.
∀prf.n = return F v prf →
FR X Y P F (return v) n.
#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >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.