Во-первых, стандартная библиотека, как известно, неполная.Таким образом, тот факт, что одно конкретное определение / лемма / модуль не предоставлен, не означает, что его там быть не должно.И это еще более справедливо для модулей, поскольку система модулей 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 (см. Определения в Equalsities ) и т. Д. При использовании Admitted для реализации eq_refl вы используете тело, отличное от указанного в подписи.Таким образом, определение вашего модуля отклоняется с сообщением the body of definitions differs.
Если я вернусь к вашей первоначальной проблеме написания функтора PairUsualDecidableTypeFull, перейдя к Equalities и EqualitiesFacts, я написал эту реализацию, которая максимально использует существующие компоненты стандартной библиотеки.
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.