Changeset 2590 for src/common/ExtraMonads.ma
 Timestamp:
 Jan 24, 2013, 7:52:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ExtraMonads.ma
r2570 r2590 63 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 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 65 74 66 75 definition res_preserve : MonadFunctRel Res Res ≝ … … 78 87 qed. 79 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 80 103 definition opt_preserve : MonadFunctRel Option Option ≝ 81 104 mk_MonadFunctRel ?? … … 92 115 qed. 93 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 94 131 definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ 95 132 λO,I.mk_MonadFunctRel ?? … … 103 140  #X #Y #P #F #G #H #u #v #K #x #EQ 104 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 % // 105 156 ] 106 157 qed. … … 118 169 FR … G 119 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). 120 181 121 182 definition preserving2 ≝ … … 133 194 FR … H 134 195 (f x y) (g (F x prf1) (G y prf2)). 135 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 136 207 lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. 137 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. 138 212 139 213 lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. … … 143 217 #M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed. 144 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 145 226 lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. 146 227 #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. … … 148 229 lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. 149 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. 150 234 151 235 lemma m_list_map_All_ok : … … 176 260 qed. 177 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 178 271 lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. 179 272 opt_preserve X Y P F m n → … … 184 277 qed. 185 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 186 289 lemma err_eq_from_io : ∀O,I,X,m,v. 187 290 err_to_io O I X m = return v → m = return v. … … 196 299 qed. 197 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.
Note: See TracChangeset
for help on using the changeset viewer.