Changeset 3050 for src/common/ExtraMonads.ma
 Timestamp:
 Apr 1, 2013, 5:18:05 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ExtraMonads.ma
r2801 r3050 74 74 }. 75 75 76 record 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 }. 76 86 77 87 definition res_preserve : MonadFunctRel Res Res ≝ … … 107 117 qed. 108 118 119 definition gen_res_preserve : MonadGenRel Res Res ≝ 120 mk_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 ] 136 qed. 137 109 138 definition opt_preserve : MonadFunctRel Option Option ≝ 110 139 mk_MonadFunctRel ?? … … 139 168 qed. 140 169 170 definition gen_opt_preserve : MonadGenRel Option Option ≝ 171 mk_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 ] 187 qed. 188 189 141 190 definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ 142 191 λO,I.mk_MonadFunctRel ?? … … 168 217  #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y} 169 218 % // 219 ] 220 qed. 221 222 definition 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 170 238 ] 171 239 qed. … … 193 261 ∀ y. 194 262 FR ?? G (f (F y)) (g y). 263 264 definition 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). 195 273 196 274 definition preserving2 ≝ … … 219 297 ∀z,w. FR ?? H (f (F z) (G w)) (g z w). 220 298 299 definition 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 221 310 lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. 222 311 #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. 223 312 224 313 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. 314 #X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. 315 316 lemma 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. 226 318 227 319 lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. … … 238 330 qed. 239 331 332 lemma gen_mfr_return_eq : ∀M1,M2.∀FR : MonadGenRel M1 M2. 333 ∀X,Y,R,x,y,n.R x y → 334 n = 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 336 qed. 337 240 338 lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. 241 339 #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. … … 246 344 lemma opt_preserve_none1 : ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n. 247 345 #X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed. 346 347 lemma 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. 248 349 249 350 lemma m_list_map_All_ok : … … 283 384 qed. 284 385 386 lemma res_to_opt_gen_preserve : ∀X,Y,R,m,n. 387 gen_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 ] 392 qed. 393 285 394 lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. 286 395 opt_preserve X Y P F m n → … … 301 410 qed. 302 411 412 lemma opt_to_res_gen_preserve : ∀X,Y,R,m,n,e1,e2. 413 gen_opt_preserve X Y R m n → 414 gen_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 ] 419 qed. 420 303 421 lemma err_eq_from_io : ∀O,I,X,m,v. 304 422 err_to_io O I X m = return v → m = return v.
Note: See TracChangeset
for help on using the changeset viewer.