List as free monoid.

freemonoid.v

Require Import List.

Section Monoid.
  Class Monoid {A:Type} (dot : A -> A -> A) (unit : A) : Prop :=
    {
      dot_assoc :
        forall x y z:A,
          dot x (dot y z) = dot (dot x y) z;
      unit_left :
        forall x, dot unit x = x;
      unit_right : forall x, dot x unit = x
    }.

  Class Homomorph
        {A:Type}{dotA:A->A->A}{unitA:A}{MonoidA:Monoid dotA unitA}
        {B:Type}{dotB:B->B->B}{unitB:B}{MonoidB:Monoid dotB unitB}
        (morph : A -> B) : Prop :=
    {
      preserve_unit :
        morph unitA = unitB;
      preserve_product :
        forall (x y:A), morph (dotA x y) = dotB (morph x) (morph y)
    }.
      
End Monoid.


Section Free_Monoid.
  Context (A:Type).

  Instance free_monoid :
    Monoid (fun x y => x ++ y)
           (nil:list A).
  Proof.
    split.
    apply app_assoc.
    apply app_nil_l.
    apply app_nil_r.
  Qed.

  Instance filter_free_monoid :
    (forall f, Homomorph (filter f)).
  Proof.
    intro.
    split.
    simpl.
    reflexivity.
    intros.
    induction x.
    simpl.
    reflexivity.
    simpl.
    case (f a).
    simpl.
    rewrite IHx.
    reflexivity.
    apply IHx.
  Qed.
  
End Free_Monoid.