Почему Coq возражает против следующего типа модуля PairUsualDecidableTypeFull?

Мне удалось обойти это, просто «обернув» Coq UsualDecidableTypeFull, определив:

Module Type UDTFW <: UsualDecidableType.

  Parameter t : Type.
  Definition eq := @Logic.eq t.
  Definition eq_equiv : Equivalence eq := _.
  Parameter eq_refl : forall x : t, x = x.
  Parameter eq_sym : forall x y : t, x = y -> y = x.
  Parameter eq_trans : forall x y z : t, x = y -> y = z -> x = z.
  Parameter eq_dec : forall x y, { @Logic.eq t x y }+{ [email protected] t x y }.
  Parameter eqb : t -> t -> bool.
  Parameter eqb_eq : forall x y : t, eqb x y = true <-> x = y.

End UDTFW.

вместе с:

Module Make_UDTFW (X : UsualDecidableTypeFull) <: UDTFW.

  Definition t := X.t.
  Definition eq := X.eq.
  Definition eq_equiv := X.eq_equiv.
  Definition eq_refl := X.eq_refl.
  Definition eq_sym := X.eq_sym.
  Definition eq_trans := X.eq_trans.
  Definition eq_dec := X.eq_dec.
  Definition eqb := X.eqb.
  Definition eqb_eq := X.eqb_eq.

End Make_UDTFW.

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

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

Во-первых, известно, что стандартная библиотека неполна. Таким образом, отсутствие одного конкретного определения/леммы/модуля не означает, что его не должно быть. И это тем более верно для модулей, так как модульная система Coq используется мало.

Что касается вашей проблемы, в Coq граница между Module и Module Type тонкая. В частности, у вас могут быть определения в Module Type, а не только объявления (я не уверен, что эти термины «определение» и «объявление» являются правильными словами для использования здесь, но я надеюсь, что это хотя бы понятно). Например,

Module Type Sig.
  Parameter n : nat.
  Definition plus x y := x + y.
End Sig.

является сигнатурой, объявляющей поле n типа nat и определяющей поле plus как сложение натуральных чисел. При написании модуля, который должен соответствовать этой сигнатуре, вы можете реализовать объявления по своему усмотрению, пока типы соответствуют, но для определений вы должны в основном написать точно такое же тело, как и в сигнатуре. Например, вы можете написать:

Module M <: Sig.
  Definition n := 3.
  Definition plus x y := x + y.
End M.

Вы можете увидеть, какие поля являются объявлениями, а какие определениями, используя Print: объявления отображаются как Parameter, а определения — как Definition (но фактическое тело определения не печатается, что, по общему признанию, сбивает с толку). В вашем случае eq, eq_equiv, eq_refl, eq_sym и eq_trans являются определениями в UsualDecidableTypeFull, поэтому у вас нет выбора для их реализации, вы должны определить eq как Logic.eq, eq_equiv как eq_equivalence (ср. определения в Равенства) и т. д. Когда используя Admitted для реализации eq_refl, вы используете тело, отличное от указанного в подписи. Таким образом, определение вашего модуля отклонено с сообщением the body of definitions differs.

Если я вернусь к вашей первоначальной проблеме написания функтора PairUsualDecidableTypeFull, покопавшись в Равенства и РавенстваФакты, я написал эту реализацию, которая максимально повторно использует существующие компоненты стандартной библиотеки.

Module DT_to_Full (D:DecidableType') <: DecidableTypeFull.
    Include Backport_DT (D).
    Include HasEqDec2Bool.
End DT_to_Full.

Module PairUsualDecidableTypeFull (D1 D2:UsualDecidableTypeFull)
  <: UsualDecidableTypeFull.

    Module M := PairUsualDecidableType D1 D2.
    Include DT_to_Full (M).
End PairUsualDecidableTypeFull.