1 | include "utilities/monad.ma". |
---|

2 | |
---|

3 | definition state_monad ≝ |
---|

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

15 | #X |
---|

16 | [ (* bind_proper *) |
---|

17 | #Y #m #n #f #g #H #G #s >H elim (n s) #s' #x normalize @G |
---|

18 | | #m#s @pair_elim // |
---|

19 | | #Y#Z #m #f #g #s elim (m s) // |
---|

20 | ] |
---|

21 | qed. |
---|

22 | |
---|

23 | definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉. |
---|

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

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

26 | definition state_update : ∀S.(S → S) → state_monad S unit ≝ λS,f,s.〈f s, it〉. |
---|

27 | |
---|

28 | definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S) |
---|

29 | (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???. |
---|

30 | [ normalize /2 by conj/ |
---|

31 | | normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps) |
---|

32 | elim (m s) #s' #x normalize * /2/ |
---|

33 | | #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/ |
---|

34 | ] |
---|

35 | qed. |
---|

36 | |
---|

37 | definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T) |
---|

38 | (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in |
---|

39 | Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???. |
---|

40 | [ normalize /2/ |
---|

41 | | normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps) |
---|

42 | * elim (m s) elim (n t) /2/ |
---|

43 | | #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/ |
---|

44 | ] |
---|

45 | qed. |
---|

46 | |
---|