Laws for Monads with State

This file defines a typeclass for MonadStateOf with compatible get and set operations.

Note that we use MonadStateOf over MonadState as the first induces the second, but we phrase things using MonadStateOf.set and MonadState.get as those are the versions that are available at the top level namespace.

@[simp]

theorem monadStateOf_get_eq_get {σ : Type u_1} {m : Type u_1 → Type u_2} [MonadStateOf σ m] : MonadStateOf.get = get

The namespaced MonadStateOf.get is equal to the MonadState provided get.

@[simp]

theorem monadStateOf_modifyGet_eq_modifyGet {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [MonadStateOf σ m] (f : σ → α × σ) : MonadStateOf.modifyGet f = modifyGet f

The namespaced MonadStateOf.modifyGet is equal to the MonadState provided modifyGet.

@[simp]

theorem liftM_get {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadStateOf σ m] [MonadLift m n] : liftM get = get

@[simp]

theorem liftM_set {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadStateOf σ m] [MonadLift m n] (s : σ) : liftM (set s) = set s

@[simp]

theorem liftM_modify {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadStateOf σ m] [MonadLift m n] (f : σ → σ) : liftM (modify f) = modify f

@[simp]

theorem liftM_modifyGet {σ α : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadStateOf σ m] [MonadLift m n] (f : σ → α × σ) : liftM (modifyGet f) = modifyGet f

@[simp]

theorem liftM_getModify {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadStateOf σ m] [MonadLift m n] (f : σ → σ) : liftM (getModify f) = getModify f

class LawfulMonadStateOf (σ : semiOutParam (Type u_1)) (m : Type u_1 → Type u_2) [Monad m] [MonadStateOf σ m] extends LawfulMonad m : Prop

Class for well behaved state monads, extending the base MonadState type. Requires that modifyGet is equal to the same definition with only get and set, that get is idempotent if the result isn't used, and that get after set returns exactly the value that was previously set.

• map_const {α β : Type u_1} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u_1} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u_1} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u_1} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u_1} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u_1} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u_1} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u_1} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u_1} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type u_1} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type u_1} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type u_1} (x : α) (f : α → m β) : pure x >>= f = f x
• bind_assoc {α β γ : Type u_1} (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• modifyGet_eq {α : Type u_1} (f : σ → α × σ) : modifyGet f = do let z ← f <$> get set z.snd pure z.fst

  modifyGet f is equal to getting the state, modifying it, and returning a result.

• get_bind_const {α : Type u_1} (mx : m α) : (do let __discr ← get let x : σ := __discr mx) = mx

  Discarding the result of get is the same as never getting the state.

• get_bind_get_bind {α : Type u_1} (mx : σ → σ → m α) : (do let s ← get let s' ← get mx s s') = do let s ← get mx s s

  Calling get twice is the same as just using the first retreived state value.

• get_bind_set_bind {α : Type u_1} (mx : σ → PUnit → m α) : (do let s ← get let u ← set s mx s u) = do let s ← get mx s PUnit.unit

  Setting the monad state to its current value has no effect.

• set_bind_get (s : σ) : (do set s get) = do set s pure s

  Setting and then returning the monad state is the same as returning the set value.

• set_bind_set (s s' : σ) : (do set s set s') = set s'

  Setting the monad twice is the same as just setting to the final state.

@[simp]

theorem LawfulMonadStateOf.get_seqRight {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (mx : m α) : get *> mx = mx

@[simp]

theorem LawfulMonadStateOf.seqLeft_get {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (mx : m α) : mx <* get = mx

@[simp]

theorem LawfulMonadStateOf.get_map_const {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (x : α) : (fun (x_1 : σ) => x) <$> get = pure x

theorem LawfulMonadStateOf.get_bind_get {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : (do let __discr ← get have x : σ := __discr get) = get

@[simp]

theorem LawfulMonadStateOf.get_bind_set {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : (do let s ← get set s) = pure PUnit.unit

@[simp]

theorem LawfulMonadStateOf.get_bind_map_set {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (f : σ → PUnit → α) : (do let s ← get f s <$> set s) = do let __do_lift ← get pure (f __do_lift PUnit.unit)

@[simp]

theorem LawfulMonadStateOf.set_bind_get_bind {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (s : σ) (f : σ → m α) : (do set s let s' ← get f s') = do set s f s

@[simp]

theorem LawfulMonadStateOf.set_bind_map_get {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (f : σ → α) (s : σ) : (do set s f <$> get) = do set s pure (f s)

@[simp]

theorem LawfulMonadStateOf.set_bind_set_bind {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (s s' : σ) (mx : m α) : (do set s set s' mx) = do set s' mx

@[simp]

theorem LawfulMonadStateOf.set_bind_map_set {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (s s' : σ) (f : PUnit → α) : (do set s f <$> set s') = f <$> set s'

theorem LawfulMonadStateOf.modifyGetThe_eq {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (f : σ → α × σ) : modifyGetThe σ f = do let z ← f <$> get set z.snd pure z.fst

theorem LawfulMonadStateOf.modify_eq {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (f : σ → σ) : modify f = do let __do_lift ← get set (f __do_lift)

theorem LawfulMonadStateOf.modifyThe_eq {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (f : σ → σ) : modifyThe σ f = do let __do_lift ← get set (f __do_lift)

theorem LawfulMonadStateOf.getModify_eq {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (f : σ → σ) : getModify f = do let s ← get set (f s) pure s

theorem LawfulMonadStateOf.modifyGet_eq' {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (f : σ → α × σ) : modifyGet f = do let s ← get modify (Prod.snd ∘ f) pure (f s).fst

Version of modifyGet_eq that preserves an call to modify.

@[simp]

theorem LawfulMonadStateOf.modify_id {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : modify id = pure PUnit.unit

@[simp]

theorem LawfulMonadStateOf.getModify_id {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : getModify id = get

@[simp]

theorem LawfulMonadStateOf.set_bind_modify {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (s : σ) (f : σ → σ) : (do set s modify f) = set (f s)

@[simp]

theorem LawfulMonadStateOf.set_bind_modify_bind {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (s : σ) (f : σ → σ) (mx : PUnit → m α) : (do set s let u ← modify f mx u) = do set (f s) mx PUnit.unit

@[simp]

theorem LawfulMonadStateOf.set_bind_modifyGet {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (s : σ) (f : σ → α × σ) : (do set s modifyGet f) = do set (f s).snd pure (f s).fst

@[simp]

theorem LawfulMonadStateOf.set_bind_modifyGet_bind {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α β : Type u_1} (s : σ) (f : σ → α × σ) (mx : α → m β) : (do set s let x ← modifyGet f mx x) = do set (f s).snd mx (f s).fst

@[simp]

theorem LawfulMonadStateOf.set_bind_getModify {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (s : σ) (f : σ → σ) : (do set s getModify f) = do set (f s) pure s

@[simp]

theorem LawfulMonadStateOf.set_bind_getModify_bind {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (s : σ) (f : σ → σ) (mx : σ → m α) : (do set s let x ← getModify f mx x) = do set (f s) mx s

@[simp]

theorem LawfulMonadStateOf.modify_bind_modify {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (f g : σ → σ) : (do modify f modify g) = modify (g ∘ f)

@[simp]

theorem LawfulMonadStateOf.modify_bind_modifyGet {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {α : Type u_1} (f : σ → σ) (g : σ → α × σ) : (do modify f modifyGet g) = modifyGet (g ∘ f)

@[simp]

theorem LawfulMonadStateOf.getModify_bind_modify {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (f : σ → σ) (g : σ → σ → σ) : (do let s ← getModify f modify (g s)) = do let s ← get modify (g s ∘ f)

theorem LawfulMonadStateOf.modify_comm_of_comp_comm {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] {f g : σ → σ} (h : f ∘ g = g ∘ f) : (do modify f modify g) = do modify g modify f

theorem LawfulMonadStateOf.modify_bind_get {σ : Type u_2} {m : Type u_2 → Type u_1} [Monad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] (f : σ → σ) : (do modify f get) = do let s ← get modify f pure (f s)

instance LawfulMonadStateOf.instStateTOfLawfulMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonadStateOf σ (StateT σ m)

StateT has lawful state operations if the underlying monad is lawful. This is applied for StateM as well due to the reducibility of that definition.

instance LawfulMonadStateOf.instStateCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} : LawfulMonadStateOf σ (StateCpsT σ m)

The continuation passing state monad variant StateCpsT always has lawful state instance.

instance LawfulMonadStateOf.instEStateM {σ ε : Type u_1} : LawfulMonadStateOf σ (EStateM ε σ)

The EStateM monad always has a lawful state instance.

instance LawfulMonadStateOf.instReaderTOfLawfulMonad {m : Type u_1 → Type u_2} {σ ρ : Type u_1} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : LawfulMonadStateOf σ (ReaderT ρ m)

If the underlying monad m has a lawful state instance, then the induced state instance on ReaderT ρ m will also be lawful.

instance LawfulMonadStateOf.instStateRefT'OfLawfulMonad {m : Type → Type} {ω σ : Type} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : LawfulMonadStateOf σ (StateRefT' ω σ m)