Library Monoid


Require Import Utf8.
Require Import FunctionalExtensionality ProofIrrelevance.

Set Implicit Arguments.

Generalizable All Variables.

Record ComputationalMonoid (M : Type) :=
  {
    monoid_obj :> _ := M;
    id : monoid_obj;
    comp : monoid_objmonoid_objmonoid_obj
  }.

Arguments id {M _}.

Infix "★" := (comp _) (at level 40, left associativity).

Class IsMonoid (M : Type) (cmonoid : ComputationalMonoid M) : Prop :=
  {
    left_id : x : cmonoid, id x = x;
    right_id : x : cmonoid, x id = x;
    assoc : a b c : cmonoid, (a b) c = a (b c)
  }.

Create HintDb monoid discriminated.
Hint Resolve left_id right_id : monoid.
Hint Immediate @assoc @left_id @right_id : monoid.
Hint Rewrite @left_id @right_id using typeclasses eauto : monoid.

Record Monoid (M : Type) :=
  {
    cmonoid :> ComputationalMonoid M;
    is_monoid :> @IsMonoid M cmonoid
  }.

Definition is_commutative M (M' : Monoid M) := a b : M', a b = b a.

Monoid Action

Class IsMonoidAction G' (G : ComputationalMonoid G') (S : Type) (f : GSS) : Prop :=
  { id_action : s, f id s = s;
    action_respectful : g g' s, f g (f g' s) = f (g g') s }.

Record MonoidAction G' (G : ComputationalMonoid G') (S : Type) :=
  {
    monoid_action :> GSS;
    is_monoid_action : @IsMonoidAction G' G S monoid_action
  }.

Infix "
" := (@monoid_action _ _ _) (at level 70).
Infix "
" := (@MonoidAction _) (at level 70) : type_scope.

Monoid Homomorphism

Definition 3.1.4.1. Let M := ( M, id, ) and M' := ( M', id', ) be monoids. A monoid homomorphism f from M to M', denoted f : M M', is a function f : M M' satisfying two conditions:

Record MonoidHomomorphism `(MH : @IsMonoid M0 M) `(M'H : @IsMonoid M'0 M') :=
  {
    MonoidHomomorphism_Function :> MM';
    MonoidHomomorphism_IdentityLaw
    : MonoidHomomorphism_Function id = id;
    MonoidHomomorphism_CompositionLaw
    : m1 m2,
        MonoidHomomorphism_Function (m1 m2)
        = (MonoidHomomorphism_Function m1) (MonoidHomomorphism_Function m2)
  }.

Definition identity_monoid_homomorphism `(MH : @IsMonoid M0 M)
: MonoidHomomorphism MH MH.
   (fun xx); reflexivity.
Defined.

Definition compose_monoid_homomorphisms
           `(MH : @IsMonoid M0 M)
           `(MH' : @IsMonoid M0' M')
           `(MH'' : @IsMonoid M0'' M'')
: MonoidHomomorphism MH' MH''
  → MonoidHomomorphism MH MH'
  → MonoidHomomorphism MH MH''.
  intros m1 m2.
   (fun xm1 (m2 x));
    abstract (
        intros;
        repeat rewrite MonoidHomomorphism_IdentityLaw;
        repeat rewrite MonoidHomomorphism_CompositionLaw;
        reflexivity
      ).
Defined.

Lemma MonoidHomomorphism_Eq
      `(MH : @IsMonoid M0 M)
      `(M'H : @IsMonoid M'0 M')
      (M1 M2 : MonoidHomomorphism MH M'H)
: ( x, MonoidHomomorphism_Function M1 x = MonoidHomomorphism_Function M2 x)
  → M1 = M2.
  intro H.
  assert (H0 : MonoidHomomorphism_Function M1 = MonoidHomomorphism_Function M2) by
      (apply functional_extensionality_dep; assumption).
  destruct M1, M2; simpl in *; subst; f_equal; apply proof_irrelevance.
Qed.