List operations and monad morphisms

This file proves that monadic operations on lists commute with monad homomorphisms (and applicative homomorphisms), and that List.reverse is a monad homomorphism on List.

Preservation of list operations under applicative homomorphisms

theorem Cslib.IsApplicativeHom.map_listMapA {m : Type u → Type um} {n : Type u → Type un} [Applicative m] [Applicative n] {F : {α : Type u} → m α → n α} (hf : IsApplicativeHom m n fun {α : Type u} => F) {α : Type v} {β : Type u} (f : α → m β) (l : List α) : F (List.mapA f l) = List.mapA (F ∘ f) l

theorem Cslib.IsApplicativeHom.map_listForA {m : Type u → Type um} {n : Type u → Type un} [Applicative m] [Applicative n] {F : {α : Type u} → m α → n α} (hf : IsApplicativeHom m n fun {α : Type u} => F) {α : Type v} (l : List α) (f : α → m PUnit.{u + 1}) : F (l.forA f) = l.forA (F ∘ f)

Preservation of list operations under monad homomorphisms

theorem Cslib.IsMonadHom.map_listMapM' {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {α : Type v} {β : Type u} (f : α → m β) (l : List α) : F (List.mapM' f l) = List.mapM' (F ∘ f) l

theorem Cslib.IsMonadHom.map_listMapMLoop {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {α : Type v} {β : Type u} (f : α → m β) (l : List α) (acc : List β) : F (List.mapM.loop f l acc) = List.mapM.loop (F ∘ f) l acc

theorem Cslib.IsMonadHom.map_listMapM {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {α : Type v} {β : Type u} (f : α → m β) (l : List α) : F (List.mapM f l) = List.mapM (F ∘ f) l

theorem Cslib.IsMonadHom.map_listForM {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {α : Type v} (l : List α) (f : α → m PUnit.{u + 1}) : F (l.forM f) = l.forM (F ∘ f)

theorem Cslib.IsMonadHom.map_listFoldlM {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {s : Type u} {α : Type v} (f : s → α → m s) (init : s) (l : List α) : F (List.foldlM f init l) = List.foldlM (fun (s_1 : s) (a : α) => F (f s_1 a)) init l

theorem Cslib.IsMonadHom.map_listFoldrM {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {s : Type u} {α : Type v} (f : α → s → m s) (init : s) (l : List α) : F (List.foldrM f init l) = List.foldrM (fun (a : α) (s_1 : s) => F (f a s_1)) init l

theorem Cslib.IsMonadHom.map_listFindSomeM? {m : Type u → Type um} {n : Type u → Type un} [Monad m] [Monad n] {F : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => F) {α : Type v} {β : Type u} (f : α → m (Option β)) (l : List α) : F (List.findSomeM? f l) = List.findSomeM? (F ∘ f) l

theorem Cslib.IsMonadHom.map_listFindM? {m n : Type → Type v} [Monad m] [Monad n] {F : {α : Type} → m α → n α} (hf : IsMonadHom m n fun {α : Type} => F) {α : Type} (p : α → m Bool) (l : List α) : F (List.findM? p l) = List.findM? (F ∘ p) l

theorem Cslib.IsMonadHom.map_listAnyM {m n : Type → Type v} [Monad m] [Monad n] {F : {α : Type} → m α → n α} (hf : IsMonadHom m n fun {α : Type} => F) {α : Type v} (p : α → m Bool) (l : List α) : F (List.anyM p l) = List.anyM (F ∘ p) l

theorem Cslib.IsMonadHom.map_listAllM {m n : Type → Type v} [Monad m] [Monad n] {F : {α : Type} → m α → n α} (hf : IsMonadHom m n fun {α : Type} => F) {α : Type v} (p : α → m Bool) (l : List α) : F (List.allM p l) = List.allM (F ∘ p) l

theorem Cslib.IsMonadHom.map_listFilterAuxM {m n : Type → Type v} [Monad m] [Monad n] {F : {α : Type} → m α → n α} (hf : IsMonadHom m n fun {α : Type} => F) {α : Type} (p : α → m Bool) (l acc : List α) : F (List.filterAuxM p l acc) = List.filterAuxM (F ∘ p) l acc

theorem Cslib.IsMonadHom.map_listFilterM {m n : Type → Type v} [Monad m] [Monad n] {F : {α : Type} → m α → n α} (hf : IsMonadHom m n fun {α : Type} => F) {α : Type} (p : α → m Bool) (l : List α) : F (List.filterM p l) = List.filterM (F ∘ p) l

Preservation of list operations under alternative homomorphisms

theorem Cslib.IsAlternativeHom.map_listFirstM {m : Type u → Type um} {n : Type u → Type un} [Alternative m] [Alternative n] {F : {α : Type u} → m α → n α} (hf : IsAlternativeHom m n fun {α : Type u} => F) {α : Type v} {β : Type u} (f : α → m β) (l : List α) : F (List.firstM f l) = List.firstM (F ∘ f) l

Monad homomorphisms on the List monad

theorem Cslib.IsApplicativeHom.map_listSingleton {F : {α : Type u_1} → List α → List α} (hf : IsApplicativeHom List List fun {α : Type u_1} => F) {α : Type u_1} (a : α) : F [a] = [a]

theorem Cslib.IsMonadHom.map_listFlatMap {F : {α : Type u_1} → List α → List α} (hf : IsMonadHom List List fun {α : Type u_1} => F) {α β : Type u_1} (l : List α) (g : α → List β) : F (List.flatMap g l) = List.flatMap (fun (x : α) => F (g x)) (F l)

theorem Cslib.IsFunctorHom.map_listNil {F : {α : Type u_1} → List α → List α} (hf : IsFunctorHom List List fun {α : Type u_1} => F) {α : Type u_1} : F [] = []

theorem List.isMonadHom_reverse : Cslib.IsMonadHom List List fun {α : Type u_1} => reverse

theorem Cslib.isMonadHom_list_iff (f : {α : Type u} → List α → List α) : IsMonadHom List List f ↔ (f = fun (x : Type u) => id) ∨ f = @List.reverse

The only monad morphisms on lists are the identity and reversal.