Наследование классов типов разных типов в Coq

После нескольких дней работы над этой проблемой я получил наследование классов типов различных типов, что, насколько я могу судить, является правильным.

Я был на правильном пути в обновлении своего вопроса. Все, что мне нужно было сделать, это добавить явное наследование Semigroup. Я до сих пор не уверен, почему он должен быть явным, если наследование из коллекции неявно наследует от складываемого и разворачиваемого. Может быть, это из-за всего наследства.

Кроме того, я узнал, что включение функций в объявление типа неверно или, по крайней мере, не нужно. Я выяснил, прочитав статью автора классов типов в Coq и Coq справочное руководство. (Если вы прокрутите вниз до класса типов EqDec, вы увидите, что eqb набран в фигурных скобках.)

Итак, вот как теперь выглядит мой класс типов Sequence:

Class Sequence (S : Type -> Type)
  `{C : Collection S}
  `{G : forall (A : Type), Semigroup (S A)}
  `{M : forall (A : Type), Monoid (S A)} :=
{
  insert_append_eq :
    forall (A : Type) (h : S A) (x : A),
    op (insert A x (empty A)) h = insert A x h
}.

Чтобы быть уверенным, что класс типов был создан правильно, я определил тип List и сделал его экземпляром Sequence. К сожалению, для этого сначала нужно было сделать его экземпляром каждого родительского класса типов. Интересно, есть ли способ попроще.

И просто чтобы включить больше примеров кода, потому что я считаю их более понятными, чем объяснения на естественном языке, вот мой класс типов Semigroup и его экземпляр List:

Class Semigroup (S : Type) :=
{
  op :
    S -> S -> S;
  semigroup_assoc :
    forall x y z : S,
    op x (op y z) = op (op x y) z
}.

Inductive List (A : Type) : Type :=
  | Nil : List A
  | Cons : A -> List A -> List A
.

Instance semigroup_list : forall A, Semigroup (List A) :=
{
  op := fix append l l' :=
    match l with
      | Nil => l'
      | Cons x xs => Cons A x (append xs l')
    end
}.
Proof.
intros.
induction x.
apply eq_refl.
rewrite IHx.
apply eq_refl.
Defined.

Спасибо за помощь, Перс. Звучит грубо, но ваш ответ был настолько разочаровывающим, что мне пришлось выяснить, ошибались ли вы на самом деле. :)

Нет, моноид - это конкретный S, применяемый к конкретному A. Вы не можете обобщать это дальше. Приведенный ниже код должен работать, хотя я не могу его проверить.

Class Sequence (S : Type -> Type) (A : Type)
  foldr empty insert append
  `{C : Collection S foldr empty insert}
  `{M : Monoid (S A) (append A) (empty A)} :=
{
  insert_append_id :
    forall (h : S A) (x : A),
    append _ (insert _ x (empty _)) h = insert _ x h
}.

Как вариант, у вас может быть другой вид моноида.

Class Mon (F : Type -> Type) (mul : forall X, F X -> F X -> F X)
  (one : forall X, F X) : Type :=
{
  idl : forall X x, mul X (one X) x = x;
  idr : forall X x, mul X x (one X) = x;
  asc : forall X x y z, mul X x (mul X y z) = mul X (mul X x y) z;
}.