source: src/utilities/state.ma @ 1636

Last change on this file since 1636 was 1635, checked in by tranquil, 9 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 1.1 KB
Line 
1include "utilities/monad.ma".
2
3definition state_setoid ≝ λS,X : Type[0].
4  mk_Setoid (S → S × X)
5    (λf,g.∀x.f x = g x) ???.
6//qed.
7
8definition State ≝
9  λS : Type[0].MakeSetoidMonad (mk_SetoidMonadDefinition
10  (* the monad *)
11  (state_setoid S)
12  (* return *)
13  (λX,x,s.〈s,x〉)
14  (* bind *)
15  (λ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 /
31]
32qed.
33
34definition state_monad ≝ λS.std_monad (State S).
35
36definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
37definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
38definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
39
40include "hints_declaration.ma".
41unification hint 0 ≔ S,X;
42M ≟ State S
43(*---------------*) ⊢
44state_monad S X ≡ std_monad (sm_def M) X
45.
46
Note: See TracBrowser for help on using the repository browser.