Last change
on this file since 1651 was
1647,
checked in by tranquil, 8 years ago

 corrected some notation problems
 adapted Cligth with slight modifications to new monad framework

File size:
1.1 KB

Line  

1  include "utilities/monad.ma". 

2  

3  definition State ≝ 

4  λS : Type[0].MakeSetoidMonadProps 

5  (* the monad *) 

6  (λX.S → S × X) 

7  (* return *) 

8  (λX,x,s.〈s,x〉) 

9  (* bind *) 

10  (λX,Y,m,f,s. let 〈s', x〉 ≝ m s in f x s') 

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 // 

32  ] 

33  qed. 

34  

35  definition state_monad ≝ λS.monad (State S). 

36  

37  definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉. 

38  definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉. 

39  definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s). 

40  

41  include "hints_declaration.ma". 

42  unification hint 0 ≔ S,X; 

43  N ≟ State S, M ≟ smax_def N, O ≟ m_def M 

44  (**) ⊢ 

45  state_monad S X ≡ monad O X 

46  . 

47  

Note: See
TracBrowser
for help on using the repository browser.