Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (7 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/monad.ma

    r1648 r1882  
    22include "basics/relations.ma".
    33include "utilities/setoids.ma".
    4 include "utilities/proper.ma".
     4
     5definition pred_transformer ≝ λA,B : Type[0].(A → Prop) → B → Prop.
     6
     7definition 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 
     10lemma 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
     14definition rel_transformer ≝ λA,B,C,D : Type[0].
     15  (A → B → Prop) → C → D → Prop.
     16 
     17definition 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 
     20lemma 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.
    523 
    6 record MonadDefinition : Type[1] ≝ {
     24record Monad : Type[1] ≝ {
    725  monad : Type[0] → Type[0] ;
    826  m_return : ∀X. X → monad X ;
     
    1129
    1230notation "m »= f" with precedence 49
    13   for @{'m_bind $m $f) }.
     31  for @{'m_bind $m $f }.
    1432
    1533notation > "!_ e; e'"
     
    104122
    105123
    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 
    132124record MonadProps : Type[1] ≝
    133125  { max_def :> Monad
     
    136128  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
    137129      ∀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
    138132  }.
    139133
     
    144138  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
    145139  ; 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)
    148142  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
    149143      sm_eq Y (! y ← return x ; f y) (f x)
     
    153147  }.
    154148
    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.
     149definition 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
     153include "hints_declaration.ma".
     154
     155unification hint 0 ≔ M, X;
     156M' ≟ smax_def M, S ≟ setoid_of_monad M X
     157(*-----------------------------*)⊢
     158monad M' X ≡ std_supp S.
     159
     160include "basics/lists/list.ma".
     161
     162definition m_map ≝ λM,X,Y.λf : X → Y.λm : monad M X.
     163  ! x ← m ; return f x.
     164
     165definition 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 
     168definition 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
     171interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
     172
     173definition 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
     178interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
     179
     180definition m_join : ∀M,X.monad M (monad M X) → monad M X ≝
     181  λM,X,m.! x ← m ; x.
     182
     183definition 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.
    182187    ! e_sig ← e ;
    183188    match e_sig with
     
    187192      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
    188193      ](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
     196interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
     197
     198definition 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
     202definition 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.
    192205    ! «r, r_prf» ← f el ;
    193206    ! «acc, acc_prf» ← macc ;
    194207    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
     210definition 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
     214unification hint 0 ≔ M, X, Y, Z, m, f ⊢
     215m_bind M (X×Y) Z m (λp.f (\fst p) (\snd p)) ≡ m_bind2 M X Y Z m f.
     216
     217unification hint 0 ≔ M, X, Y, Z, W, m, f ⊢
     218m_bind M (X×Y×Z) W m (λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p)) ≡
     219m_bind3 M X Y Z W m f.
     220
     221definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind.
     222mk_MonadProps (mk_Monad monad m_return m_bind).
    200223
    201224definition 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 
     228record 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
     237record 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.