(** List monad *)

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Sorting.Sorting.
Require Import Beroal.Init.

Set Implicit Arguments.

(** * [list] is a functor *)

Definition functor_pres_id (e : Type) (xs : list e)
	: xs = map (@Beroal.Init.id _) xs.
Proof.
refine (fun e => _).
refine (fix rec (xs : list e) : xs = map (@id _) xs := _).
destruct xs as [|x xss].
refine (refl_equal _).
simpl.
	refine (f_equal (cons x) (rec _)).
Qed.

(** functor preserves composition : [Coq.Lists.List.map_map] *)

(** * Monad of lists *)

Definition singleton (e : Type) (x : e) := x :: nil.

(** 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.
Proof.
refine (fun e0 e1 f ys => _).
refine (fix rec (xs : list e0) := _).
destruct xs as [|x xss].
simpl.
	refine (refl_equal _).
simpl.
	refine (eq_ind _ (fun dep => _ ++ dep = _) _ _ (sym_eq (rec _))).
	refine (sym_eq (app_ass _ _ _)).
Qed.

(** μ, join *)

(** bind = [flip flat_map] *)

Definition join (e : Type) := @flat_map (list e) _ (@id _).

(** [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.
Proof.
refine (fun e0 e1 e2 f => _).
refine (fix rec (xs : list e0) fy {struct xs} := _).
destruct xs as [|x xss].
simpl.
	refine (refl_equal _).
unfold cf.
	simpl.
	refine (eq_ind _ (fun dep => dep = _) _ _ (sym_eq (map_app _ _ _))).
	refine (f_equal _ (rec _ _)).
Qed.

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.
Proof.
refine (fun e0 e1 e2 f => _).
refine (fix rec (xs : list e0) fy {struct xs} := _).
destruct xs as [|x xss].
simpl.
	refine (refl_equal _).
unfold cf.
	simpl.
	refine (f_equal _ (rec _ _)).
Qed.

Definition monad_id_left (e0 e1 : Type) (fy : e0 -> list e1) (x : e0)
	: fy x = flat_map fy (singleton x).
Proof.
refine (fun e0 e1 fy x => _).
simpl.
refine (app_nil_end _).
Qed.

Definition monad_id_right (e : Type) (xs : list e)
	: xs = flat_map (@singleton _) xs.
Proof.
refine (fun e => _).
refine (fix rec (xs : list e) := _).
destruct xs as [|x xss].
simpl.
	refine (refl_equal _).
simpl.
	refine (f_equal _ (rec _)).
Qed.

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.
Proof.
refine (fun e0 e1 e2 fy fz => _).
refine (fix rec (xs : list e0) := _).
destruct xs as [|x xss].
simpl.
	refine (refl_equal _).
simpl.
	refine (eq_ind _ (fun dep => dep = _) _ _
		(sym_eq (flat_map_app _ _ _))).
	refine (f_equal _ (rec _)).
Qed.



Definition sort_singleton (e : Type) (le0 : relation e)
	(dec : forall x y : e, {le0 x y} + {le0 y x})
	x : sort le0 (singleton x).
Proof.
refine (fun e le0 dec x => cons_sort (@nil_sort _ _) (@nil_leA _ _ _)).
Qed.