Changeset 1976 for src/utilities/monad.ma
 Timestamp:
 May 21, 2012, 7:04:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r1949 r1976 23 23 24 24 record Monad : Type[1] ≝ { 25 monad : Type[0] → Type[0] ;25 monad :1> Type[0] → Type[0] ; 26 26 m_return : ∀X. X → monad X ; 27 27 m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y … … 124 124 record MonadProps : Type[1] ≝ 125 125 { max_def :> Monad 126 ; m_return_bind : ∀X,Y.∀x : X.∀f : X → m onad max_def Y. ! y ← return x ; f y = f x127 ; m_bind_return : ∀X.∀m : m onad max_def X.! x ← m ; return x = m128 ; m_bind_bind : ∀X,Y,Z. ∀m : m onad max_def X.∀f : X → monadmax_def Y.129 ∀g : Y → m onad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y130 ; m_bind_ext_eq : ∀X,Y.∀m : m onad max_def X.∀f,g : X → monadmax_def Y.126 ; m_return_bind : ∀X,Y.∀x : X.∀f : X → max_def Y. ! y ← return x ; f y = f x 127 ; m_bind_return : ∀X.∀m : max_def X.! x ← m ; return x = m 128 ; m_bind_bind : ∀X,Y,Z. ∀m : max_def X.∀f : X → max_def Y. 129 ∀g : Y → max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y 130 ; m_bind_ext_eq : ∀X,Y.∀m : max_def X.∀f,g : X → max_def Y. 131 131 (∀x.f x = g x) → ! x ← m ; f x = ! x ← m ; g x 132 132 }. … … 134 134 record SetoidMonadProps : Type[1] ≝ 135 135 { smax_def :> Monad 136 ; sm_eq : ∀X.relation ( monadsmax_def X)136 ; sm_eq : ∀X.relation (smax_def X) 137 137 ; sm_eq_refl : ∀X.reflexive ? (sm_eq X) 138 138 ; sm_eq_trans : ∀X.transitive ? (sm_eq X) … … 140 140 ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x) 141 141 ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (x »= f) (y »= g) 142 ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monadsmax_def Y.142 ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → smax_def Y. 143 143 sm_eq Y (! y ← return x ; f y) (f x) 144 ; sm_bind_return : ∀X.∀m : monadsmax_def X.sm_eq X (! x ← m ; return x) m145 ; sm_bind_bind : ∀X,Y,Z. ∀m : monad smax_def X.∀f : X → monadsmax_def Y.146 ∀g : Y → monadsmax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)144 ; sm_bind_return : ∀X.∀m : smax_def X.sm_eq X (! x ← m ; return x) m 145 ; sm_bind_bind : ∀X,Y,Z. ∀m : smax_def X.∀f : X → smax_def Y. 146 ∀g : Y → smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y) 147 147 }. 148 148 149 149 definition setoid_of_monad : ∀M : SetoidMonadProps.∀X : Type[0]. 150 150 Setoid ≝ 151 λM,X.mk_Setoid ( monadM X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X).151 λM,X.mk_Setoid (M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X). 152 152 153 153 include "hints_declaration.ma". … … 160 160 include "basics/lists/list.ma". 161 161 162 definition m_map ≝ λM ,X,Y.λf : X → Y.λm : monadM X.162 definition m_map ≝ λM : Monad.λX,Y.λf : X → Y.λm : M X. 163 163 ! x ← m ; return f x. 164 164 165 definition m_map2 ≝ λM ,X,Y,Z.λf : X → Y → Z.λm : monad M X.λn : monadM Y.165 definition m_map2 ≝ λM : Monad.λX,Y,Z.λf : X → Y → Z.λm : M X.λn : M Y. 166 166 ! x ← m ; ! y ← n ; return f x y. 167 167 168 definition m_bind2 ≝ λM ,X,Y,Z.λm : monad M (X × Y).λf : X → Y → monadM Z.168 definition m_bind2 ≝ λM : Monad.λX,Y,Z.λm : M (X × Y).λf : X → Y → M Z. 169 169 ! p ← m ; f (\fst p) (\snd p). 170 170 … … 172 172 173 173 definition m_bind3 : 174 ∀M ,X,Y,Z,W.monad M (X×Y×Z) → (X → Y → Z → monad M W) → monadM W ≝174 ∀M : Monad.∀X,Y,Z,W.M (X×Y×Z) → (X → Y → Z → M W) → M W ≝ 175 175 λM,X,Y,Z,W,m,f. 176 176 ! p ← m ; f (\fst (\fst p)) (\snd (\fst p)) (\snd p). … … 178 178 interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f). 179 179 180 definition m_join : ∀M ,X.monad M (monad M X) → monadM X ≝180 definition m_join : ∀M : Monad.∀X.M (M X) → M X ≝ 181 181 λM,X,m.! x ← m ; x. 182 182 183 183 definition m_sigbind2 : 184 ∀M ,A,B,C.∀P:A×B → Prop. monadM (Σx:A×B.P x) →185 (∀a,b. P 〈a,b〉 → monad M C) → monadM C ≝184 ∀M : Monad.∀A,B,C.∀P:A×B → Prop. M (Σx:A×B.P x) → 185 (∀a,b. P 〈a,b〉 → M C) → M C ≝ 186 186 λM,A,B,C,P,e,f. 187 187 ! e_sig ← e ; … … 197 197 198 198 definition m_list_map : 199 ∀M ,X,Y.(X → monad M Y) → list X → monadM (list Y) ≝199 ∀M : Monad.∀X,Y.(X → M Y) → list X → M (list Y) ≝ 200 200 λM,X,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l. 201 201 202 202 definition m_list_map_sigma : 203 ∀M ,X,Y,P.(X → monad M (Σy : Y.P y)) → list X → monadM (Σl : list Y.All ? P l) ≝203 ∀M : Monad.∀X,Y,P.(X → M (Σy : Y.P y)) → list X → M (Σl : list Y.All ? P l) ≝ 204 204 λM,X,Y,P,f,l.foldr … (λel,macc. 205 205 ! «r, r_prf» ← f el ; … … 209 209 210 210 definition m_bin_op : 211 ∀M ,X,Y,Z.(X → Y → Z) → monad M X → monad M Y → monadM Z ≝211 ∀M : Monad.∀X,Y,Z.(X → Y → Z) → M X → M Y → M Z ≝ 212 212 λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y. 213 213 214 unification hint 0 ≔ M, X, Y, Z, m, f ⊢ 215 m_bind M (X×Y) Z m (λp.f (\fst p) (\snd p)) ≡ m_bind2 M X Y Z m f. 216 217 unification hint 0 ≔ M, X, Y, Z, W, m, f ⊢ 218 m_bind M (X×Y×Z) W m (λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p)) ≡ 219 m_bind3 M X Y Z W m f. 214 unification hint 0 ≔ M, X, Y, Z, m, f ; 215 P ≟ Prod X Y, F ≟ λp.f (\fst p) (\snd p) ⊢ 216 m_bind M P Z m F ≡ m_bind2 M X Y Z m f. 217 218 unification hint 0 ≔ M, X, Y, Z, W, m, f ; 219 P' ≟ Prod X Y, P ≟ Prod P' Z, F ≟ λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p) ⊢ 220 m_bind M P W m F ≡ m_bind3 M X Y Z W m f. 220 221 221 222 definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind. … … 229 230 230 231 record MonadPred (M : Monad) : Type[1] ≝ 231 { m_pred :> ∀X.pred_transformer X (monad M X) 232 ; mp_inject : ∀X,P.(Σm.m_pred X P m) → monad M (Σx.P x) 232 { m_pred :2> ∀X.(X → Prop) → (M X → Prop) 233 233 ; mp_return : ∀X,P,x.P x → m_pred X P (return x) 234 234 ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m → … … 236 236 m_pred ? Pout (m_bind … m f) 237 237 ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X) 238 }. 239 240 record InjMonadPred (M : Monad) : Type[1] ≝ 241 { im_pred :> MonadPred M 242 ; mp_inject : ∀X.∀P : X → Prop.(Σm.im_pred P m) → M (Σx.P x) 238 243 ; mp_inject_eq : ∀X,P,m.pi1 ?? m = ! x ← mp_inject X P m ; return pi1 … x 239 244 }. 240 245 241 coercion coerc_mp_inject : ∀M.∀MP: MonadPred M.242 ∀X ,P.∀m : Σm.m_pred ? MP X P m.monadM (Σx.P x) ≝243 mp_inject on _m : Sig (monad ??) (λm. m_pred ???? m) to monad ? (Sig ? (λx.? x)).244 245 lemma mp_inject_bind : ∀M : MonadProps.∀MP,X,P,Y.∀m.∀f : X → monadM Y.246 coercion coerc_mp_inject : ∀M.∀MP:InjMonadPred M. 247 ∀X.∀P : X → Prop.∀m : Σm.MP P m.M (Σx.P x) ≝ 248 mp_inject on _m : Sig (monad ??) (λm.im_pred ??? m) to monad ? (Sig ? (λx.? x)). 249 250 lemma mp_inject_bind : ∀M : MonadProps.∀MP,X,P,Y.∀m.∀f : X → M Y. 246 251 ! x ← mp_inject M MP X P m ; f (pi1 … x) = ! x ← pi1 … m ; f x. 247 252 #M#MP#X#P#Y#m#f >mp_inject_eq >m_bind_bind @m_bind_ext_eq #x >m_return_bind % qed. 248 253 249 254 record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ 250 { m_rel : > ∀X,Y.rel_transformer X Y (monad M1 X) (monad M2 Y)255 { m_rel :3> ∀X,Y.(X → Y → Prop) → (M1 X → M2 Y → Prop) 251 256 ; mr_return : ∀X,Y,rel,x,y.rel x y → m_rel X Y rel (return x) (return y) 252 257 ; mr_bind : ∀X,Y,Z,W,relin,relout,m,n.m_rel X Y relin m n → ∀f,g.(∀x,y.relin x y → m_rel Z W relout (f x) (g y)) → … … 254 259 ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y) 255 260 }. 256 257
Note: See TracChangeset
for help on using the changeset viewer.