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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.