Ignore:
Timestamp:
Apr 1, 2013, 5:18:05 PM (7 years ago)
Author:
piccolo
Message:

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraMonads.ma

    r2801 r3050  
    7474}.
    7575
     76record MonadGenRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
     77{ m_gen_rel :5> ∀X,Y.(X → Y → Prop) → (M1 X → M2 Y → Prop)
     78; m_gen_return : ∀X,Y,R,x,y.R x y → m_gen_rel X Y R (return x) (return y)
     79; m_gen_bind : ∀X,Y,Z,W,R1,R2,m,n.m_gen_rel X Y R1 m n →
     80           ∀f,g.(∀x,y.R1 x y → m_gen_rel Z W R2 (f x) (g y)) → m_gen_rel ?? R2 (m_bind … m f) (m_bind … n g)
     81; m_gen_bind_inversion  : ∀X,Y,Z,W,R1,R2,m,n.m_gen_rel X Y R1 m n →
     82         ∀f,g.(∀x,y.m = return x → n = return y → R1 x y → m_gen_rel Z W R2 (f x) (g y))
     83         → m_gen_rel ?? R2 (m_bind … m f) (m_bind … n g)
     84; m_gen_rel_ext : ∀X,Y,R1,R2.(∀x,y.R1 x y → R2 x y) → ∀u,v.m_gen_rel X Y R1 u v → m_gen_rel X Y R2 u v
     85}.
    7686
    7787definition res_preserve : MonadFunctRel Res Res ≝
     
    107117qed.
    108118
     119definition gen_res_preserve : MonadGenRel Res Res ≝
     120mk_MonadGenRel ??
     121(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
     122????.
     123[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
     124| #X #Y #Z #W #R1 #R2 * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     125  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     126  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
     127  %{(refl …)} assumption
     128| #X #Y #Z #W #R1 #R2 * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     129  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
     130  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
     131  normalize %{EQw} assumption
     132| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
     133  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     134  #Rxy %{y} %{(refl …)} @H assumption
     135]
     136qed.
     137
    109138definition opt_preserve : MonadFunctRel Option Option ≝
    110139  mk_MonadFunctRel ??
     
    139168qed.
    140169
     170definition gen_opt_preserve : MonadGenRel Option Option ≝
     171mk_MonadGenRel ??
     172(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
     173????.
     174[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
     175| #X #Y #Z #W #R1 #R2 * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     176  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     177  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
     178  %{(refl …)} assumption
     179| #X #Y #Z #W #R1 #R2 * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     180  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
     181  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
     182  normalize %{EQw} assumption
     183| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
     184  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     185  #Rxy %{y} %{(refl …)} @H assumption
     186]
     187qed.
     188
     189
    141190definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    142191  λO,I.mk_MonadFunctRel ??
     
    168217| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    169218  % //
     219]
     220qed.
     221
     222definition gen_io_preserve : ∀O,I.MonadGenRel (IOMonad O I)(IOMonad O I) ≝
     223λO,I.mk_MonadGenRel ??
     224(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
     225????.
     226[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
     227| #X #Y #Z #W #R1 #R2 * [#o #r | #x | #e ] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     228  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     229  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
     230  %{(refl …)} assumption
     231| #X #Y #Z #W #R1 #R2 * [#o #r | #x | #e ] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     232  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
     233  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
     234  normalize %{EQw} assumption
     235| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
     236  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     237  #Rxy %{y} %{(refl …)} @H assumption
    170238]
    171239qed.
     
    193261  ∀ y.
    194262  FR ?? G (f (F y)) (g y).
     263 
     264definition gen_preserving ≝
     265λM1,M2.λFR : MonadGenRel M1 M2.
     266 λX,Y,A,B : Type[0].
     267 λR1 : X → Y → Prop.
     268 λR2 : A → B → Prop.
     269 λf : X → M1 A.
     270 λg : Y → M2 B.
     271 ∀x,y. R1 x y →
     272 FR ?? R2 (f x) (g y).
    195273
    196274definition preserving2 ≝
     
    219297   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
    220298   
     299definition gen_preserving2 ≝
     300λM1,M2.λFR : MonadGenRel M1 M2.
     301  λX,Y,Z,W,A,B : Type[0].
     302  λR1 : X → Y → Prop.
     303  λR2 : Z → W → Prop.
     304  λR3 : A → B → Prop.
     305  λf : X → Z → M1 A.
     306  λg : Y → W → M2 B.
     307  ∀x,y,z,w. R1 x y → R2 z w →
     308  FR ?? R3 (f x z) (g y w). 
     309
    221310lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
    222311#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
    223312
    224313lemma 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.
     314#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     315
     316lemma res_preserve_error_gen : ∀X,Y,R,e,n.gen_res_preserve X Y R (Error … e) n.
     317#X #Y #R #e #n whd #x whd in ⊢ (???% → ?); #EQ destruct qed.
    226318
    227319lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
     
    238330qed.
    239331
     332lemma gen_mfr_return_eq : ∀M1,M2.∀FR : MonadGenRel M1 M2.
     333∀X,Y,R,x,y,n.R x y →
     334n = return x → FR X Y R n (return y).
     335#M1 #M2 #FR #X #Y #R #x #y #n #H #EQ destruct @m_gen_return assumption
     336qed.
     337
    240338lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
    241339#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
     
    246344lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
    247345#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
     346
     347lemma opt_preserve_none_gen : ∀X,Y,R,n.gen_opt_preserve X Y R (None ?) n.
     348#X #Y #R #n whd #x whd in ⊢ (???% → ?); #EQ destruct qed.
    248349
    249350lemma m_list_map_All_ok :
     
    283384qed.
    284385
     386lemma res_to_opt_gen_preserve : ∀X,Y,R,m,n.
     387gen_res_preserve X Y R m n → gen_opt_preserve X Y R (res_to_opt … m) (res_to_opt … n).
     388#X #Y #R #m #n #H #x #EQ whd in H; cases(H x ?)
     389[ #y * #y_spec #Rxy %{y} >y_spec %{(refl …)} assumption
     390| cases m in EQ; normalize #x #EQ destruct %
     391]
     392qed.
     393
    285394lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
    286395       opt_preserve X Y P F m n →
     
    301410qed.
    302411
     412lemma opt_to_res_gen_preserve :  ∀X,Y,R,m,n,e1,e2.
     413gen_opt_preserve X Y R m n →
     414gen_res_preserve X Y R (opt_to_res … e1 m) (opt_to_res … e2 n).
     415#X #Y #R #m #n #e1 #e2 #H #x #EQ whd in H; cases(H x ?)
     416[ #y * #y_spec #Rxy %{y} >y_spec %{(refl …)} assumption
     417| cases m in EQ; normalize [2: #x] #EQ destruct %
     418]
     419qed.
     420
    303421lemma err_eq_from_io : ∀O,I,X,m,v.
    304422  err_to_io O I X m = return v → m = return v.
Note: See TracChangeset for help on using the changeset viewer.