include "utilities/monad.ma".

definition State ≝
  λ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)
  ????????.
//
#X
[ (* bind_proper *)
  #Y #m#n #m_eq_n
  #f #g #f_eq_g
  #s
  generalize in match (m_eq_n s); -m_eq_n
  normalize
  #m_eq_n >m_eq_n -m_eq_n
  elim (n s) #s' #y
  normalize @f_eq_g //
| #m#s normalize
  elim (m s) normalize /2 by /
| #Y #Z #m #f #g #s normalize
  elim (m s) normalize
  #s' #x
  elim (f x s') normalize
  #s'' #y //
]
qed.

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

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).

include "hints_declaration.ma".
unification hint 0 ≔ S,X;
N ≟ State S, M ≟ smax_def N, O ≟ m_def M
(*---------------*) ⊢
state_monad S X ≡ monad O X
.