Documentation

ToMathlib.Control.StateT

Lemmas about StateT #

source
@[implicit_reducible]
instance StateT.instMonadLift_toMathlib {m : Type u → Type v} {m' : Type u → Type w} {σ : Type u} [MonadLift m m'] :
MonadLift (StateT σ m) (StateT σ m')
source
@[simp]
theorem StateT.liftM_of_liftM_eq {m : Type u → Type v} {m' : Type u → Type w} {σ α : Type u} [MonadLift m m'] (x : StateT σ m α) :
liftM x = mk fun (s : σ) => liftM (x.run s)
source
theorem StateT.liftM_def {m : Type u → Type v} {σ α : Type u} [Monad m] (x : m α) :
liftM x = StateT.lift x
source
@[simp]
theorem StateT.run_liftM {m : Type u → Type v} {σ α : Type u} [Monad m] (x : m α) (s : σ) :
(liftM x).run s = do let a ← x pure (a, s)
source
theorem StateT.monad_pure_def {m : Type u → Type v} {σ α : Type u} [Monad m] (x : α) :
pure x = StateT.pure x
source
theorem StateT.monad_bind_def {m : Type u → Type v} {σ α β : Type u} [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) :
x >>= f = x.bind f
source
theorem StateT.monad_failure_eq {m : Type u → Type v} {σ α : Type u} [AlternativeMonad m] :
failure = StateT.failure
source
@[simp]
theorem StateT.run_failure' {m : Type u → Type v} {σ α : Type u} [AlternativeMonad m] :
failure.run = fun (x : σ) => failure
source
@[simp]
theorem StateT.mk_pure_eq_pure {m : Type u → Type v} {σ α : Type u} [Monad m] (x : α) :
(mk fun (s : σ) => pure (x, s)) = pure x

StateT.run' lemmas #

source
@[simp]
theorem StateT.run'_pure' {m : Type u → Type v} {σ α : Type u} [Monad m] [LawfulMonad m] (x : α) (s : σ) :
(pure x).run' s = pure x
source
@[simp]
theorem StateT.run'_bind' {m : Type u → Type v} {σ α β : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ) :
(x >>= f).run' s = do let x ← x.run s match x with | (a, s') => (f a).run' s'
source
@[simp]
theorem StateT.run'_map' {m : Type u → Type v} {σ α β : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (f : α → β) (s : σ) :
(f <$> x).run' s = f <$> x.run' s
source
@[simp]
theorem StateT.run'_lift' {m : Type u → Type v} {σ α : Type u} [Monad m] [LawfulMonad m] (x : m α) (s : σ) :
(StateT.lift x).run' s = x
source
theorem StateT.map_run'_eq_of_map_eq {m : Type u → Type v} {σ α β : Type u} [Monad m] [LawfulMonad m] {γ : Type u} {f : α → γ} {g : β → γ} {mx : StateT σ m α} {my : StateT σ m β} (s : σ) (h : f <$> mx = g <$> my) :
f <$> mx.run' s = g <$> my.run' s

If two StateT computations agree after mapping into a common result type, then they still agree after projecting away the final state with run' from any initial state.