chore: add ReaderT.mk and StateT.mk (#11470)

These complement the existing `ExceptT.mk` and `OptionT.mk`, and provide
a symbol to key `simp` lemmas on, to prevent getting stuck on
`StateT.run (fun s => f s) s`.

A future PR could insert these new `mk`s into the implementation of many
definitions, such that unfolding the definitions leaves appropriate
casts behind; but this is invasive, and by itself having `mk` provides
value.

Author: eric-wieser

src/Init/Control/Lawful/Instances.lean

@@ -234,6 +234,9 @@ namespace ReaderT
   simp [run] at h
   exact funext h
 
+@[simp, grind =] theorem run_mk (x : ρ → m α) (ctx : ρ) : run (.mk x : ReaderT ρ m α) ctx = x ctx :=
+  rfl
+
 @[simp, grind =] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
 
 @[simp, grind =] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
@@ -295,6 +298,9 @@ namespace StateT
 @[ext, grind ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   funext h
 
+@[simp, grind =] theorem run_mk [Monad m] (x : σ → m (α × σ)) (s : σ) : run (.mk x) s = x s :=
+  rfl
+
 @[simp, grind =] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
   rfl
 

src/Init/Control/State.lean

@@ -25,6 +25,12 @@ of a value and a state.
 @[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
+/--
+Interpret `σ → m (α × σ)` as an element of `StateT σ m α`.
+-/
+@[always_inline, inline, expose]
+def StateT.mk {σ : Type u} {m : Type u → Type v} {α : Type u} (x : σ → m (α × σ)) : StateT σ m α := x
+
 /--
 Executes an action from a monad with added state in the underlying monad `m`. Given an initial
 state, it returns a value paired with the final state.

src/Init/Prelude.lean

@@ -4047,6 +4047,12 @@ ordinary actions in `m`.
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   ρ → m α
 
+/--
+Interpret `ρ → m α` as an element of `ReaderT ρ m α`.
+-/
+@[always_inline, inline]
+def ReaderT.mk {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ρ → m α) : ReaderT ρ m α := x
+
 instance (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] : Inhabited (ReaderT ρ m α) where
   default := fun _ => default