source: src/utilities/state.ma @ 1651

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 
1include "utilities/monad.ma".
2
3definition 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]
33qed.
34
35definition state_monad ≝ λS.monad (State S).
36
37definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
38definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
39definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
40
41include "hints_declaration.ma".
42unification hint 0 ≔ S,X;
43N ≟ State S, M ≟ smax_def N, O ≟ m_def M
44(*---------------*) ⊢
45state_monad S X ≡ monad O X
46.
47
Note: See TracBrowser for help on using the repository browser.