Changeset 1882 for src/utilities/monad.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r1648 r1882 2 2 include "basics/relations.ma". 3 3 include "utilities/setoids.ma". 4 include "utilities/proper.ma". 4 5 definition pred_transformer ≝ λA,B : Type[0].(A → Prop) → B → Prop. 6 7 definition modus_ponens ≝ λA,B.λPT : pred_transformer A B. 8 ∀P,Q.(∀x.P x → Q x) → ∀y.PT P y → PT Q y. 9 10 lemma mp_transitive : 11 ∀A,B,C,PT1,PT2.modus_ponens A B PT1 → modus_ponens B C PT2 → 12 modus_ponens A C (PT2 ∘ PT1). /4/ qed. 13 14 definition rel_transformer ≝ λA,B,C,D : Type[0]. 15 (A → B → Prop) → C → D → Prop. 16 17 definition rel_modus_ponens ≝ λA,B,C,D.λRT : rel_transformer A B C D. 18 ∀P,Q.(∀x,y.P x y → Q x y) → ∀z,w.RT P z w → RT Q z w. 19 20 lemma rel_mp_transitive : 21 ∀A,B,C,D,E,F,RT1,RT2.rel_modus_ponens A B C D RT1 → rel_modus_ponens C D E F RT2 → 22 rel_modus_ponens … (RT2 ∘ RT1). /4/ qed. 5 23 6 record Monad Definition: Type[1] ≝ {24 record Monad : Type[1] ≝ { 7 25 monad : Type[0] → Type[0] ; 8 26 m_return : ∀X. X → monad X ; … … 11 29 12 30 notation "m »= f" with precedence 49 13 for @{'m_bind $m $f )}.31 for @{'m_bind $m $f }. 14 32 15 33 notation > "!_ e; e'" … … 104 122 105 123 106 include "basics/lists/list.ma".107 108 109 (* add structure and properties as needed *)110 record Monad : Type[1] ≝ {111 m_def :> MonadDefinition ;112 m_map : ∀X, Y. (X → Y) → monad m_def X → monad m_def Y ;113 m_map2 : ∀X, Y, Z. (X → Y → Z) →114 monad m_def X → monad m_def Y → monad m_def Z;115 m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z;116 m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;117 m_join : ∀X.monad m_def (monad m_def X) → monad m_def X;118 m_sigbind2 : ∀A,B,C.∀P:A×B → Prop. monad m_def (Σx:A×B.P x) →119 (∀a,b. P 〈a,b〉 → monad m_def C) → monad m_def C;120 m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);121 m_mmap_sigma : ∀X,Y,P.(X → monad m_def (Σy : Y.P y)) → list X → monad m_def (Σl : list Y.All ? P l)122 }.123 124 interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).125 interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).126 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).127 128 (*129 check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)130 *)131 132 124 record MonadProps : Type[1] ≝ 133 125 { max_def :> Monad … … 136 128 ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y. 137 129 ∀g : Y → monad 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 : monad max_def X.∀f,g : X → monad max_def Y. 131 (∀x.f x = g x) → ! x ← m ; f x = ! x ← m ; g x 138 132 }. 139 133 … … 144 138 ; sm_eq_trans : ∀X.transitive ? (sm_eq X) 145 139 ; sm_eq_sym : ∀X.symmetric ? (sm_eq X) 146 ; sm_return_proper : ∀X .m_return smax_def X ⊨ eq ? ++> sm_eq ?147 ; sm_bind_proper : ∀X, Y.m_bind smax_def X Y ⊨ sm_eq ? ++> (eq ? ++> sm_eq ?) ++> sm_eq ?140 ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x) 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) 148 142 ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y. 149 143 sm_eq Y (! y ← return x ; f y) (f x) … … 153 147 }. 154 148 155 interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y). 156 157 158 definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind. 159 mk_Monad (mk_MonadDefinition monad m_return m_bind) 160 (* map *) 161 (λX,Y,f,m. 162 ! x ← m ; 163 return f x) 164 (* map2 *) 165 (λX,Y,Z,f,m,n. 166 ! x ← m ; 167 ! y ← n ; 168 return (f x y)) 169 (* bind2 *) 170 (λX,Y,Z,m,f. 171 ! p ← m ; 172 let 〈x, y〉 ≝ p in 173 f x y) 174 (λX,Y,Z,W,m,f. 175 ! p ← m ; 176 let 〈x, y, z〉 ≝ p in 177 f x y z) 178 (* join *) 179 (λX,m.! x ← m ; x) 180 (* m_sigbind2 *) 181 (λA,B,C,P,e,f. 149 definition setoid_of_monad : ∀M : SetoidMonadProps.∀X : Type[0]. 150 Setoid ≝ 151 λM,X.mk_Setoid (monad M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X). 152 153 include "hints_declaration.ma". 154 155 unification hint 0 ≔ M, X; 156 M' ≟ smax_def M, S ≟ setoid_of_monad M X 157 (**)⊢ 158 monad M' X ≡ std_supp S. 159 160 include "basics/lists/list.ma". 161 162 definition m_map ≝ λM,X,Y.λf : X → Y.λm : monad M X. 163 ! x ← m ; return f x. 164 165 definition m_map2 ≝ λM,X,Y,Z.λf : X → Y → Z.λm : monad M X.λn : monad M Y. 166 ! x ← m ; ! y ← n ; return f x y. 167 168 definition m_bind2 ≝ λM,X,Y,Z.λm : monad M (X × Y).λf : X → Y → monad M Z. 169 ! p ← m ; f (\fst p) (\snd p). 170 171 interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f). 172 173 definition m_bind3 : 174 ∀M,X,Y,Z,W.monad M (X×Y×Z) → (X → Y → Z → monad M W) → monad M W ≝ 175 λM,X,Y,Z,W,m,f. 176 ! p ← m ; f (\fst (\fst p)) (\snd (\fst p)) (\snd p). 177 178 interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f). 179 180 definition m_join : ∀M,X.monad M (monad M X) → monad M X ≝ 181 λM,X,m.! x ← m ; x. 182 183 definition m_sigbind2 : 184 ∀M,A,B,C.∀P:A×B → Prop. monad M (Σx:A×B.P x) → 185 (∀a,b. P 〈a,b〉 → monad M C) → monad M C ≝ 186 λM,A,B,C,P,e,f. 182 187 ! e_sig ← e ; 183 188 match e_sig with … … 187 192 λeq_p. f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p) 188 193 ](refl …) 189 ]) 190 (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l) 191 (λX,Y,P,f,l.foldr … (λel,macc. 194 ]. 195 196 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f). 197 198 definition m_list_map : 199 ∀M,X,Y.(X → monad M Y) → list X → monad M (list Y) ≝ 200 λM,X,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l. 201 202 definition m_list_map_sigma : 203 ∀M,X,Y,P.(X → monad M (Σy : Y.P y)) → list X → monad M (Σl : list Y.All ? P l) ≝ 204 λM,X,Y,P,f,l.foldr … (λel,macc. 192 205 ! «r, r_prf» ← f el ; 193 206 ! «acc, acc_prf» ← macc ; 194 207 return (mk_Sig ?? (r :: acc) ?)) 195 (return (mk_Sig … [ ] ?)) l). 196 % assumption qed. 197 198 definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3. 199 mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3. 208 (return (mk_Sig … [ ] ?)) l. % assumption qed. 209 210 definition m_bin_op : 211 ∀M,X,Y,Z.(X → Y → Z) → monad M X → monad M Y → monad M Z ≝ 212 λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y. 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. 220 221 definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind. 222 mk_MonadProps (mk_Monad monad m_return m_bind). 200 223 201 224 definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝ 202 λmonad,m_return,m_bind,sm_eq,p1,p2,p3,p4,p5,p6,p7,p8. 203 mk_SetoidMonadProps (MakeMonad monad m_return m_bind) sm_eq p1 p2 p3 p4 p5 p6 p7 p8. 225 λmonad,m_return,m_bind. 226 mk_SetoidMonadProps (mk_Monad monad m_return m_bind). 227 228 record MonadPred (M : Monad) : Type[1] ≝ 229 { m_pred :> ∀X.pred_transformer X (monad M X) 230 ; mp_return : ∀X,P,x.P x → m_pred X P (return x) 231 ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m → 232 ∀f.(∀x.Pin x → m_pred Y Pout (f x)) → 233 m_pred ? Pout (m_bind … m f) 234 ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X) 235 }. 236 237 record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ 238 { m_rel :> ∀X,Y.rel_transformer X Y (monad M1 X) (monad M2 Y) 239 ; mr_return : ∀X,Y,rel,x,y.rel x y → m_rel X Y rel (return x) (return y) 240 ; 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)) → 241 m_rel ?? relout (m_bind … m f) (m_bind … n g) 242 ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y) 243 }.
Note: See TracChangeset
for help on using the changeset viewer.