algebra.v

Require Import Coq.Lists.List.
Import ListNotations.

Inductive hlist : list Type -> Type :=
| nil : hlist []
| cons {Ts : list Type}
       {T : Type} : T -> hlist Ts -> hlist (T :: Ts).

Notation "[ ]" := nil (format "[ ]") : hlist_scope.
Notation "[ x ]" := (cons x nil) : hlist_scope.
Notation "[ x ; y ; .. ; z ]" :=
  (cons x (cons y .. (cons z nil) ..)) : hlist_scope.

Fixpoint arity_type (T : Type) (n : nat) : Type :=
  match n with
  | 0 => T
  | S n => T -> (arity_type T n)
  end.

Definition Signature := list nat.

Fixpoint signature_types
         (T : Type) (s : Signature) : list Type :=
  match s with
  | [] => []
  | a :: s => (arity_type T a) :: (signature_types T s)
  end.

Inductive Universal :
  forall (carrier : Type) (signature : Signature),
    hlist (signature_types carrier signature) -> Type :=
  mkUniversal c s l : Universal c s l.

Open Scope hlist_scope.

Class Semigroup :=
  { semi_carrier : Type;
    semi_operation :
      semi_carrier -> semi_carrier -> semi_carrier;
    semi_assoc : forall x y z : semi_carrier,
        semi_operation x (semi_operation y z) =
        semi_operation (semi_operation x y) z;
    semi_uni :
      Universal semi_carrier ([2])%list [semi_operation]
  }.

Coercion semi_carrier : Semigroup >-> Sortclass.
Coercion semi_uni : Semigroup >-> Universal.

Lemma plus_assoc : forall x y z, plus x (plus y z) =
                            plus (plus x y) z.
Proof.
  induction x; intros.
  - reflexivity.
  - simpl. auto.
Qed.

Definition semi_nat : Semigroup :=
  {| semi_carrier := nat;
     semi_operation := plus;
     semi_assoc := plus_assoc;
     semi_uni := ltac:(constructor)
  |}.

Definition expand_universal'
           {c s l}
           (u : Universal c s l)
           (n : nat)
           (op : arity_type c n) :=
  Universal c (n :: s)%list (cons op l).

Class Monoid :=
  { mono_semigroup : Semigroup;
    mono_element : mono_semigroup;
    mono_uni : expand_universal' mono_semigroup 0 mono_element
  }.

Coercion mono_semigroup : Monoid >-> Semigroup.

Definition mono_nat :=
  {| mono_semigroup := semi_nat;
     mono_element := 0;
     mono_uni := ltac:(constructor)
  |}.

Definition zero : mono_nat := mono_element.
Definition one : semi_nat := 1.
Definition one' : nat := semi_operation one zero.