Changeset 1647 for src/utilities


Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (9 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
Location:
src/utilities
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/bindLists.ma

    r1636 r1647  
    7878   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
    7979
    80 notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for
     80notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    8181 ${default
    8282   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
     
    8484 }.
    8585 
    86 notation > "νν ident l : ty × n opt('with' ident EQ) 'in' f" with precedence 47 for
     86notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    8787 ${default
    8888   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
     
    9090 }.
    9191 
    92 notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     92notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    9393   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    94 notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for
     94notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for
    9595   @{ 'unews $n (λ${ident l} : $ty.$f) }.
    9696
     
    112112 
    113113 
    114 coercion blist_from_list nocomposites :
     114coercion blist_from_list :
    115115  ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.
    116116
     
    154154 
    155155definition BindList ≝
    156   λB,T.MakeMonad (mk_MonadDefinition
     156  λB,T.MakeMonadProps
    157157  (* the monad *)
    158158  (λX.bind_list B T X)
     
    161161  (* bind *)
    162162  (bbind B T)
    163   ???).
    164 [(* bind_bind *)
     163  ???.
     164[(* ret_bind *)
     165  #X#Y#x#f normalize @bappend_bnil
     166|(* bind_ret *)
     167 #X#m elim m normalize /2 by /
     168 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi
     169|(* bind_bind *)
    165170 #X#Y#Z#m#f#g elim m normalize
    166171 [//
     
    169174 |(* case bnew *)
    170175  #t #l #Hi @bnew_proper //
     176  #x#y #x_eq_y destruct(x_eq_y) @Hi
    171177 ]
    172 |(* bind_ret *)
    173  #X#m elim m normalize /2 by /
    174  #t #l' #Hi @bnew_proper normalize // #s#t#eq destruct @Hi
    175 |(* ret_bind *)
    176   #X#Y#x#f normalize @bappend_bnil
    177178]
    178179qed.
     180
     181unification hint 0 ≔ B, T, X;
     182  N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M
     183(*--------------------------------------------*) ⊢
     184  bind_list B T X ≡ monad O X.
    179185
    180186include "utilities/state.ma".
     
    195201theorem bcompile_append :
    196202  ∀E, R, T, U, fresh, bl1, bl2.
    197   bcompile E R T U fresh (bl1 @ bl2) ≅
     203  (bcompile E R T U fresh (bl1 @ bl2)) ≅
    198204  (
    199205  ! l1 ← bcompile … fresh bl1 ;
  • src/utilities/lists.ma

    r1631 r1647  
    5757] H.
    5858
     59include "utilities/monad.ma".
     60
     61definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
     62// qed.
     63
     64definition List ≝ MakeMonadProps
     65  list
     66  (λX,x.[x])
     67  (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
     68  ???. normalize
     69[ / by /
     70| #X#m elim m normalize //
     71| #X#Y#Z #m #f#g
     72  elim m normalize [//]
     73  #x#l' #Hi
     74  <(fold_sum ?? (f x) ? [ ] (Append ?))
     75  >Hi //
     76] qed.
     77
     78unification hint 0 ≔ X ;
     79N ≟ max_def List, M ≟ m_def N
     80(*---------------------------*)⊢
     81list X ≡ monad M X.
  • src/utilities/monad.ma

    r1640 r1647  
    77  monad : Type[0] → Type[0] ;
    88  m_return : ∀X. X → monad X ;
    9   m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y;
    10   m_return_bind : ∀X,Y.∀x : X.∀f : X → monad Y.
    11     m_bind ?? (m_return ? x) f = f x ;
    12   m_bind_return : ∀X.∀m : monad X.
    13     m_bind ?? m (m_return ?) = m ;
    14   m_bind_bind : ∀X,Y,Z. ∀m : monad X.∀f : X → monad Y.∀g : Y → monad Z.
    15     m_bind ?? (m_bind ?? m f) g = m_bind ?? m (λx. m_bind ?? (f x) g)
     9  m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y
    1610}.
    1711
    18 record SetoidMonadDefinition : Type[1] ≝ {
    19   std_monad : Type[0] → Setoid ;
    20   sm_return : ∀X. X → std_monad X ;
    21   sm_bind : ∀X,Y. std_monad X → (X → std_monad Y) → std_monad Y;
    22   sm_return_proper : ∀X. sm_return X ⊨ eq ? ++> std_eq …;
    23   sm_bind_proper : ∀X,Y.
    24     sm_bind X Y ⊨ std_eq … ++> (eq ? ++> std_eq …) ++> std_eq …;
    25   sm_return_bind : ∀X,Y : Setoid.∀x : X.∀f : X → std_monad Y.
    26     sm_bind ?? (sm_return ? x) f ≅ f x ;
    27   sm_bind_return : ∀X.∀m : std_monad X.
    28     sm_bind ?? m (sm_return ?) ≅ m ;
    29   sm_bind_bind : ∀X,Y,Z. ∀m : std_monad X.∀f : X → std_monad Y.∀g : Y → std_monad Z.
    30     sm_bind ?? (sm_bind ?? m f) g ≅ sm_bind ?? m (λx. sm_bind ?? (f x) g)
    31 }.
    32 
    33 notation "m »= f" with precedence 47
     12notation "m »= f" with precedence 49
    3413  for @{'m_bind $m $f) }.
    3514
     
    3716  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    3817notation > "! ident v ← e; e'"
    39   with precedence 48 for @{'m_bind' (λ${ident v}. ${e'}) ${e}}.
     18  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
    4019notation > "! ident v : ty ← e; e'"
    4120  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    42 notation < "vbox(! \nbsp ident v ← e ; break e')"
     21notation < "vbox(! \nbsp ident v ← e ; break e')"
    4322  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
    4423notation > "! ident v ← e : ty ; e'"
    4524  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
    46 notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
     25notation < "vbox(! \nbsp ident v : ty \nbsp ←  \nbsp e ; break e')"
    4726  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    4827notation > "! ident v : ty ← e : ty' ; e'"
     
    5029notation > "! 〈ident v1, ident v2〉 ← e ; e'"
    5130  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     31notation > "! 〈ident v1, ident v2〉 ← e : ty ; e'"
     32  with precedence 48 for @{'m_bind2 (${e} : $ty) (λ${ident v1}. λ${ident v2}. ${e'})}.
    5233notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
    5334  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5435notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
    5536  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
    56 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 e ; break e')"
     37notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉  \nbsp ←  \nbsp e ; break e')"
    5738  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5839notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
    5940  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
     41notation > "! 〈ident v1, ident v2, ident v3〉 ← e : ty ; e'"
     42  with precedence 48 for @{'m_bind3 (${e} : ${ty}) (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
    6043notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    6144  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    62 notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 e ; break e')"
     45notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')"
    6346  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
    64 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; break e')"
     47notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')"
    6548  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    6649
    67  
    68 (* "do" alternative notation for backward compatibility *)
     50(* dependent pair versions *)
     51notation > "! «ident v1, ident v2» ← e ; e'"
     52  with precedence 48 for
     53  @{'m_bind ${e} (λ${fresh p_sig}.
     54    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
     55notation < "vbox(! \nbsp «ident v1, ident v2» \nbsp ← \nbsp e ; break e')"
     56  with precedence 48 for
     57  @{'m_bind ${e} (λ${fresh p_sig}.
     58    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
     59   
     60notation > "! «ident v1, ident v2, ident H» ← e ; e'"
     61  with precedence 48 for
     62  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
     63notation < "vbox(! \nbsp «ident v1, ident v2, ident H» \nbsp ← \nbsp e ; e')"
     64  with precedence 48 for
     65  @{'m_sigbind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.
     66    λ${ident H} : ${ty3}. ${e'})}.
     67   
     68 
     69(*alternative do notation for backward compatibility *)
     70notation > "'do'_ e; e'"
     71  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    6972notation > "'do' ident v ← e; e'"
    7073  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
    7174notation > "'do' ident v : ty ← e; e'"
    7275  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
     76notation > "'do' ident v ← e : ty ; e'"
     77  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
     78notation > "'do' ident v : ty ← e : ty' ; e'"
     79  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
    7380notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
    7481  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     
    7986notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    8087  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    81  
     88
    8289(* dependent pair versions *)
    83 notation > "! «ident v1, ident v2» ← e ; e'"
     90notation > "'do' «ident v1, ident v2» ← e ; e'"
    8491  with precedence 48 for
    8592  @{'m_bind ${e} (λ${fresh p_sig}.
    8693    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
    8794
    88 notation > "! «ident v1, ident v2, ident H» ← e ; e'"
    89   with precedence 48 for
    90   @{'m_bind ${e} (λ${fresh p_sig}.
    91     match ${fresh p_sig} with [mk_Sig ${fresh p} ${ident H} ⇒
    92       match ${fresh p} with [mk_Prod ${ident v1} ${ident v2} ⇒ ${e'}]])}.
    93 
    94 notation > "'do' «ident v1, ident v2» ← e ; e'"
    95   with precedence 48 for
    96   @{'m_bind ${e} (λ${fresh p_sig}.
    97     match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
    98 
    9995notation > "'do' «ident v1, ident v2, ident H» ← e ; e'"
    10096  with precedence 48 for
    101   @{'m_bind ${e} (λ${fresh p_sig}.
    102     match ${fresh p_sig} with [mk_Sig ${fresh p} ${ident H} ⇒
    103       match ${fresh p} with [mk_Prod ${ident v1} ${ident v2} ⇒ ${e'}]])}.
    104 
    105 notation > "'return' t" with precedence 46 for @{'m_return $t}.
    106 notation < "'return' \nbsp t" with precedence 46 for @{'m_return $t}.
    107 
    108 interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f).
    109 interpretation "setoid monad bind'" 'm_bind' f m = (sm_bind ? ? ? m f).
    110 interpretation "setoid monad return" 'm_return x = (sm_return ? ? x).
     97  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
     98
     99notation > "'return' t" with precedence 49 for @{'m_return $t}.
     100notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}.
     101
    111102interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
    112 interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).
    113103interpretation "monad return" 'm_return x = (m_return ? ? x).
    114104
     105
    115106include "basics/lists/list.ma".
     107
    116108
    117109(* add structure and properties as needed *)
     
    124116  m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
    125117  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;
    126120  m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
    127121  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)
     
    130124interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
    131125interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
    132 
    133 (* notation breaks completely here.... *)
    134 definition mmap_sigma_helper : ∀M.∀X,Y,P.?→?→?→monad M (Σl : list Y.All ? P l) ≝
    135   λM.λX,Y:Type[0].λP.λf : X → monad M (Σy : Y.P y).
    136   λel.λmacc : monad M (Σl : list Y.All ? P l).
    137     m_bind M ?? (f el) (λp.
    138     match p with [mk_Sig r r_prf ⇒
    139     m_bind M ?? macc (λq.
    140     match q with [mk_Sig acc acc_prf ⇒
    141     return (mk_Sig … (r :: acc) ?)])]).
    142 whd %{r_prf acc_prf} qed.
    143 
    144 definition MakeMonad : MonadDefinition → Monad ≝ λM.
    145   mk_Monad M
     126interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
     127
     128check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)
     129
     130record MonadProps : Type[1] ≝
     131  { max_def :> Monad
     132  ; m_return_bind : ∀X,Y.∀x : X.∀f : X → monad max_def Y. ! y ← return x ; f y = f x
     133  ; m_bind_return : ∀X.∀m : monad max_def X.! x ← m ; return x = m
     134  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
     135      ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
     136  }.
     137
     138record SetoidMonadProps : Type[1] ≝
     139  { smax_def :> Monad
     140  ; sm_eq : ∀X.relation (monad smax_def X)
     141  ; sm_eq_refl : ∀X.reflexive ? (sm_eq X)
     142  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
     143  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
     144  ; sm_return_proper : ∀X .m_return smax_def X ⊨ eq ? ++> sm_eq ?
     145  ; sm_bind_proper : ∀X, Y.m_bind smax_def X Y ⊨ sm_eq ? ++> (eq ? ++> sm_eq ?) ++> sm_eq ?
     146  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
     147      sm_eq Y (! y ← return x ; f y) (f x)
     148  ; sm_bind_return : ∀X.∀m : monad smax_def X.sm_eq X (! x ← m ; return x) m
     149  ; sm_bind_bind : ∀X,Y,Z. ∀m : monad smax_def X.∀f : X → monad smax_def Y.
     150      ∀g : Y → monad smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)
     151  }.
     152
     153interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y).
     154
     155
     156definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind.
     157  mk_Monad (mk_MonadDefinition monad m_return m_bind)
    146158  (* map *)
    147159  (λX,Y,f,m.
     
    164176  (* join *)
    165177  (λX,m.! x ← m ; x)
     178  (* m_sigbind2 *)
     179  (λA,B,C,P,e,f.
     180    ! e_sig ← e ;
     181    match e_sig with
     182    [ mk_Sig p p_prf ⇒
     183      match p return λx.x = p → ? with
     184      [ mk_Prod a b ⇒
     185      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
     186      ](refl …)
     187    ])
    166188  (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l)
    167   (λX,Y,P,f,l.foldr … (mmap_sigma_helper M … f) (return (mk_Sig … [ ] ?)) l).
    168   % qed.
    169 
    170 
    171 (* add structure and properties as needed *)
    172 record SetoidMonad : Type[1] ≝ {
    173   sm_def :> SetoidMonadDefinition ;
    174   sm_map : ∀X, Y. (X → Y) → std_monad sm_def X → std_monad sm_def Y ;
    175   sm_map2 : ∀X, Y, Z. (X → Y → Z) →
    176     std_monad sm_def X → std_monad sm_def Y → std_monad sm_def Z;
    177   sm_bind2 : ∀X,Y,Z.std_monad sm_def (X×Y) →
    178     (X → Y → std_monad sm_def Z) → std_monad sm_def Z
    179 }.
    180 
    181 definition MakeSetoidMonad : SetoidMonadDefinition → SetoidMonad ≝ λM.
    182   mk_SetoidMonad M
    183   (* map *)
    184   (λX,Y,f,m.
    185     ! x ← m ;
    186     return f x)
    187   (* map2 *)
    188   (λX,Y,Z,f,m,n.
    189     ! x ← m ;
    190     ! y ← n ;
    191     return (f x y))
    192   (* bind2 *)
    193   (λX,Y,Z,m,f.
    194     ! p ← m ;
    195     let 〈x, y〉 ≝ p in
    196     f x y).
    197 
    198 interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f).
    199 
    200 record MonadTransformer : Type[1] ≝ {
    201   monad_trans : MonadDefinition → MonadDefinition ;
    202   m_lift : ∀M,X. monad M X → monad (monad_trans M) X ;
    203   m_lift_return : ∀M,X.∀x : X. m_lift M X (return x) = return x ;
    204   m_lift_bind : ∀M,X,Y.∀m : monad M X.∀f : X → monad M Y.
    205     m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x)
    206 }.
     189  (λX,Y,P,f,l.foldr … (λel,macc.
     190    ! «r, r_prf» ← f el ;
     191    ! «acc, acc_prf» ← macc ;
     192    return (mk_Sig ?? (r :: acc) ?))
     193    (return (mk_Sig … [ ] ?)) l).
     194  % assumption qed.
     195
     196definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3.
     197mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3.
     198
     199definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝
     200  λmonad,m_return,m_bind,sm_eq,p1,p2,p3,p4,p5,p6,p7,p8.
     201  mk_SetoidMonadProps (MakeMonad monad m_return m_bind) sm_eq p1 p2 p3 p4 p5 p6 p7 p8.
  • src/utilities/option.ma

    r1640 r1647  
    22include "basics/types.ma".
    33
    4 definition Option ≝ MakeMonad (mk_MonadDefinition
     4definition Option ≝ MakeMonadProps
    55  (* the monad *)
    66  option
     
    99  (* bind *)
    1010  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
    11   ???).
    12 // #X[#Y#Z]*normalize//qed.
     11  ???.
     12// #X[2:#Y#Z]*normalize//qed.
    1313
    1414include "hints_declaration.ma".
    1515unification hint 0 ≔ X;
    16 M ≟ m_def Option
     16N ≟ max_def Option, M ≟ m_def N
    1717(*---------------*) ⊢
    1818option X ≡ monad M X
     
    2424  | None ⇒ λeq_m.?
    2525  ] (refl …). elim (absurd … eq_m prf) qed.
    26 
    27 (* playground for notation problems *)
    28 
    29 inductive option_bis (X : Type[0]) : Type[0] ≝
    30 | Some' : X → option_bis X
    31 | None' : option_bis X.
    32 
    33 definition option_to_option' ≝ λX.λm : option X. match m with [ Some x ⇒ Some' ? x | None ⇒ None' ?].
    34 
    35 coercion o_to_o' : ∀X.∀m : option X. option_bis X ≝ option_to_option'
    36   on _m : option ? to option_bis ?.
    37  
    38 
    39 definition Option_bis ≝ MakeMonad (mk_MonadDefinition
    40   option_bis
    41   (λX.Some' X)
    42   (λX,Y,m,f.match m with [Some' x ⇒ f x | None' ⇒ None' ?])
    43   ???). //
    44 #X[#Y#Z] * normalize // qed.
    45 
    46 unification hint 0 ≔ X ;
    47 M ≟ m_def Option_bis
    48 (*---------------*) ⊢
    49 option_bis X ≡ monad M X
    50 .
    51 
    52 (* does not typecheck
    53 check (λX.λm : option_bis X.λn : option X.! x ← n ; m)
    54 *)
  • src/utilities/state.ma

    r1635 r1647  
    11include "utilities/monad.ma".
    22
    3 definition state_setoid ≝ λS,X : Type[0].
    4   mk_Setoid (S → S × X)
    5     (λf,g.∀x.f x = g x) ???.
    6 //qed.
    7 
    83definition State ≝
    9   λS : Type[0].MakeSetoidMonad (mk_SetoidMonadDefinition
     4  λS : Type[0].MakeSetoidMonadProps
    105  (* the monad *)
    11   (state_setoid S)
     6  (λX.S → S × X)
    127  (* return *)
    138  (λX,x,s.〈s,x〉)
    149  (* bind *)
    1510  (λX,Y,m,f,s. let 〈s', x〉 ≝ m s in f x s')
    16   ?????).
    17 / by /
    18 [(* bind_bind *)
    19  #X#Y#Z#m#f#g#s
    20  elim (m s) #s' #x normalize
    21  elim (f x s') #s'' #y normalize //
    22 |(* bind_ret *)
    23  #X#m#s elim (m s) #s' #x normalize //
    24 |(*bind proper*)
    25   #X#Y#m#n#eqmn#f#g#eqfg#s
    26  generalize in match (eqmn s); -eqmn
    27  elim (m s) #s' #x normalize
    28  elim (n s) #s'' #x' normalize
    29  #E destruct
    30  /2 by /
     11  (* monad eq *)
     12  (λX,c1,c2.∀s.c1 s = c2 s)
     13  ????????.
     14//
     15#X
     16[ (* bind_proper *)
     17  #Y #m#n #m_eq_n
     18  #f #g #f_eq_g
     19  #s
     20  generalize in match (m_eq_n s); -m_eq_n
     21  normalize
     22  #m_eq_n >m_eq_n -m_eq_n
     23  elim (n s) #s' #y
     24  normalize @f_eq_g //
     25| #m#s normalize
     26  elim (m s) normalize /2 by /
     27| #Y #Z #m #f #g #s normalize
     28  elim (m s) normalize
     29  #s' #x
     30  elim (f x s') normalize
     31  #s'' #y //
    3132]
    3233qed.
    3334
    34 definition state_monad ≝ λS.std_monad (State S).
     35definition state_monad ≝ λS.monad (State S).
    3536
    3637definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
     
    4041include "hints_declaration.ma".
    4142unification hint 0 ≔ S,X;
    42 M ≟ State S
     43N ≟ State S, M ≟ smax_def N, O ≟ m_def M
    4344(*---------------*) ⊢
    44 state_monad S X ≡ std_monad (sm_def M) X
     45state_monad S X ≡ monad O X
    4546.
    4647
Note: See TracChangeset for help on using the changeset viewer.