Formalized Coq proof that lists form a semigroup, monoid, functor and monad.

list_monad.v

Require Import List.
Import ListNotations.

(** A semigroup consists of an total associative operation. **)
Inductive semigroup (A : Type) (Op : A -> A -> A) : Prop :=
| semigroup_intro :
    (forall (a b c : A), Op a (Op b c) = Op (Op a b) c) -> semigroup A Op.

(** Proof that lists with append form a semigroup. **)
Theorem list_semigroup :
  forall A : Type, semigroup (list A) (@app A).
Proof.
  intros. apply semigroup_intro, app_assoc.
Qed.

(** A monoid consists of a semigroup with left and right identities. **)
Inductive monoid A Op (sg : semigroup A Op) (U : A) : Prop :=
| monoid_intro :
    semigroup A Op
    -> (forall (a : A), Op U a = Op a U /\ Op U a = a)
    -> monoid A Op sg U.

(** Proof that lists with append and the empty list form a monoid. **)
Theorem list_monoid : forall A, monoid (list A) (@app A) (@list_semigroup A) [].
Proof.
  intros. apply monoid_intro. apply list_semigroup. split.
  - rewrite app_nil_r. reflexivity.
  - reflexivity.
Qed.

(** A functor consists of a type constructor F and fmap preserving
    morphisms. **)
Inductive functor (F : Type -> Type) :
  (forall a b, (a -> b) -> F a -> F b) -> Prop :=
| functor_intro
    (fmap : forall t1 t2, (t1 -> t2) -> F t1 -> F t2)
    (l1   : forall t f, fmap t t id f = f)
    (l2   : forall a b c, forall (f : F a) (p : b -> c) (q : a -> b),
          fmap a c (fun a => p (q a)) f = fmap b c p (fmap a b q f)) :
    functor F fmap.

(** Proof that lists with map form a functor. **)
Theorem list_functor : functor list map.
Proof.
  apply functor_intro.
  - apply map_id.
  - intros. induction f; simpl.
    + reflexivity.
    + rewrite IHf. reflexivity.
Qed.

(** A monad consists of a functor F, operations bind and lift that
    satisfy the monad laws. **)
Inductive monad : (Type -> Type) -> Prop :=
| monad_intro
    (F        : Type -> Type)
    (fmap     : forall t1 t2, (t1 -> t2) -> F t1 -> F t2)
    (Fp       : functor F fmap)
    (bind     : forall t1 t2, F t1 -> (t1 -> F t2) -> F t2)
    (lift     : forall t, t -> F t)
    (left_id  : forall t1 t2 a f, bind t1 t2 (lift t1 a) f = f a)
    (right_id : forall t m, bind t t m (lift t) = m)
    (assoc    : forall t1 t2 t3 m f g, bind t2 t3 (bind t1 t2 m f) g
                                  = bind t1 t3 m (fun x => bind t2 t3 (f x) g))
  : monad F.

Fixpoint concat {A : Type} (l : list (list A)) : list A :=
  match l with
  | []    => []
  | h :: t => app h (concat t)
  end.

Definition singleton (A : Type) (x : A) := [x].

Definition concatMap (A : Type) (B : Type) (l : list A) (f : A -> list B) : list B :=
  concat (map f l).

(** Helper lemma, concatenation distributes over append. **)
Lemma concat_app_distr : forall (A : Type) (a : list (list A)) (b : list (list A)),
    concat (a ++ b) = concat a ++ concat b.
Proof.
  intros.
  induction a.
  - simpl. reflexivity.
  - simpl. rewrite IHa. rewrite app_assoc. reflexivity.
Qed.

(** Proof that lists with fmap = map, bind = concatMap, lift x = [x]
    form a monad. **)
Theorem list_monad : monad list.
Proof.
  apply monad_intro with (fmap := map) (bind := concatMap) (lift := singleton).
  apply list_functor.
  - intros. unfold concatMap. simpl. apply app_nil_r.
  - intros. unfold concatMap. induction m.
    + reflexivity.
    + simpl. rewrite IHm. reflexivity.
  - intros. unfold concatMap. induction m.
    + reflexivity.
    + simpl. rewrite <- IHm. rewrite map_app.
      rewrite concat_app_distr. reflexivity.
Qed.