Monad Morphisms Commute with Loops

The bundled corollaries, for MonadHom, of cslib's IsMonadHom.map_list* lemmas and of ToCslib.Control.Monad.HomTransport: a monad morphism between lawful monads commutes with forIn', forIn, forM, foldlM, and mapM over lists, and with forIn over any container whose loop is the loop over ForIn.toList. Each is an equation whose left-hand side is the morphism applied to the loop, so simp pushes morphisms into loop bodies the way mmap_bind pushes them into binds, and grind can index the list forms. Lawfulness is what lets the bundled arrow — which carries only its pure and bind laws — satisfy cslib's predicate (MonadHom.isMonadHom).

@[simp]

theorem MonadHom.mmap_forIn' {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) {ι : Type x} {β : Type u} (l : List ι) (init : β) (f : (a : ι) → a ∈ l → β → m (ForInStep β)) : (fun {α : Type u} (x : m α) => F.toFun α x) (forIn' l init f) = forIn' l init fun (a : ι) (h : a ∈ l) (b : β) => (fun {α : Type u} (x : m α) => F.toFun α x) (f a h b)

theorem MonadHom.mmap_forIn {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) {ι : Type x} {β : Type u} (l : List ι) (init : β) (f : ι → β → m (ForInStep β)) : (fun {α : Type u} (x : m α) => F.toFun α x) (forIn l init f) = forIn l init fun (a : ι) (b : β) => (fun {α : Type u} (x : m α) => F.toFun α x) (f a b)

Not a simp lemma: simp already derives it from mmap_forIn' through core's List.forIn'_eq_forIn.

@[simp]

theorem MonadHom.mmap_forM {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) {ι : Type x} (l : List ι) (f : ι → m PUnit.{u + 1}) : (fun {α : Type u} (x : m α) => F.toFun α x) (forM l f) = forM l fun (a : ι) => (fun {α : Type u} (x : m α) => F.toFun α x) (f a)

Stated with the class method forM, the simp normal form of List.forM.

@[simp]

theorem MonadHom.mmap_foldlM {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) {σ : Type u} {ι : Type x} (f : σ → ι → m σ) (init : σ) (l : List ι) : (fun {α : Type u} (x : m α) => F.toFun α x) (List.foldlM f init l) = List.foldlM (fun (s : σ) (a : ι) => (fun {α : Type u} (x : m α) => F.toFun α x) (f s a)) init l

@[simp]

theorem MonadHom.mmap_mapM {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) {ι : Type x} {β : Type u} (f : ι → m β) (l : List ι) : (fun {α : Type u} (x : m α) => F.toFun α x) (List.mapM f l) = List.mapM (fun (a : ι) => (fun {α : Type u} (x : m α) => F.toFun α x) (f a)) l

@[simp]

theorem MonadHom.mmap_forIn_of_pureForIn {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) {ρ : Type y} {ι : Type x} {β : Type u} [ForIn m ρ ι] [ForIn n ρ ι] [ForIn Id ρ ι] [Std.Internal.PureForIn m ρ ι] [Std.Internal.PureForIn n ρ ι] (xs : ρ) (init : β) (f : ι → β → m (ForInStep β)) : (fun {α : Type u} (x : m α) => F.toFun α x) (forIn xs init f) = forIn xs init fun (a : ι) (b : β) => (fun {α : Type u} (x : m α) => F.toFun α x) (f a b)