Coq - объединить типы из функторов модуля с одинаковыми параметрами?

Question

Как я могу заставить Coq распознавать, что два типа, каждый из которых импортируется из модуля, созданного из функтора модуля с использованием одного и того же аргумента, но присутствующих в разных модулях, на самом деле являются одним и тем же типом? * Минимальный пример

Module Type S.
End S.

Module F (s : S).
Inductive foo : Type := a.
End F.

Module G (s : S).
Include F s.
End G.

Module H (s : S).
Include F.
End H.

Module I (s : S).

Module G := G s.
Module H := H s.

(* This is a type error - but the foos are the same! *)
Axiom bar : forall g : G.foo, forall h : H.foo, g = h.

End I.

В приведенном выше файле Coq я хочу объявить аксиому, которая требует, чтобы тип foo в G s был таким же, как тип foo в H s. Ясно, что это действительно так. Но могу ли я заставить Coq его распознать?

Answer 1

Это невозможно. Между индуктивными типами нет структурной эквивалентности. Используя дважды Include, вы создаете два разных типа. У них совпадают имена, но это просто совпадение.

В общем, индуктивные типы плохо поддерживаются модульной системой. Каждый раз, когда вы пробуете что-то необычное, Coq будет жаловаться, что «ядро еще не распознает, что параметр может быть создан с помощью индуктивного типа».

Как правило, я предлагаю всегда определять индуктивный тип. типы вне функторов модуля. Я полагаю, что ваш тип foo будет зависеть от некоторого свойства модуля s, поэтому вам нужно сделать его немного более общим c:

Module Type S.
Axiom t : Type.
End S.

Inductive foo (t : Type) : Type := a : t -> foo t.

Module F (s : S).
Definition foo := foo s.t.
End F.