include "utilities/monad.ma".

definition state_monad ≝
  λS : Type[0].MakeSetoidMonadProps
  (* the monad *)
  (λX.S → S × X)
  (* return *)
  (λX,x,s.〈s,x〉)
  (* bind *)
  (λX,Y,m,f,s. let 〈s', x〉 ≝ m s in f x s')
  (* monad eq *)
  (λX,c1,c2.∀s.c1 s = c2 s)
  ????????.
// normalize
#X
[ (* bind_proper *)
  #Y #m #n #f #g #H #G #s >H elim (n s) #s' #x normalize @G
| #m#s @pair_elim //
| #Y#Z #m #f #g #s elim (m s) //
]
qed.

definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).

definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
[ normalize /2 by conj/
| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
  elim (m s) #s' #x normalize * /2/
| #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/
]
qed.

definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T)
  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
[ normalize /2/
| normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps)
  * elim (m s) elim (n t) /2/
| #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/
]
qed.