Library Beroal.ListMonad
List monad
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Sorting.Sorting.
Require Import Beroal.Init.
functor preserves composition : Coq.Lists.List.map_map
singleton is a natural transformation
Check fun (e0 e1 : Type) (f : e0 -> e1) (x : e0)
=> (refl_equal _) : map f (singleton x) = singleton (f x).
Definition flat_map_app (e0 e1 : Type) (f : e0 -> list e1) ys xs
: flat_map f (xs ++ ys) = flat_map f xs ++ flat_map f ys.
=> (refl_equal _) : map f (singleton x) = singleton (f x).
Definition flat_map_app (e0 e1 : Type) (f : e0 -> list e1) ys xs
: flat_map f (xs ++ ys) = flat_map f xs ++ flat_map f ys.
μ, join
bind = flip flat_map
join is a natural transformation
Definition flat_map_nt_law0 (e0 e1 e2 : Type) (f : e1 -> e2)
(xs : list e0) (fy : e0 -> list e1)
: map f (flat_map fy xs) = flat_map (cf (map f) fy) xs.
Definition flat_map_nt_law1 (e0 e1 e2 : Type) (f : e0 -> e1)
(xs : list e0) (fy : e1 -> list e2)
: flat_map fy (map f xs) = flat_map (cf fy f) xs.
Definition monad_id_left (e0 e1 : Type) (fy : e0 -> list e1) (x : e0)
: fy x = flat_map fy (singleton x).
Definition monad_id_right (e : Type) (xs : list e)
: xs = flat_map (@singleton _) xs.
Definition monad_assoc (e0 e1 e2 : Type)
(fy : e0 -> list e1) (fz : e1 -> list e2) (xs : list e0)
: flat_map fz (flat_map fy xs) = flat_map (fun x => flat_map fz (fy x)) xs.
Definition sort_singleton (e : Type) (le0 : relation e)
(dec : forall x y : e, {le0 x y} + {le0 y x})
x : sort le0 (singleton x).