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 文件中，我想声明一个公理，要求 G s 中的类型 foo 与 H s 中的类型 foo 相同。显然，事实确实如此。但是我可以让 Coq 识别它吗？

Answer 1

这是不可能的。归纳类型之间没有结构对等。通过使用Include 两次，您将创建两种不同的类型。他们碰巧同名，但这只是巧合。

更一般地说，模块系统对归纳类型的支持很差。任何时候你尝试一些花哨的东西，Coq 都会抱怨“内核还没有识别出一个参数可以被归纳类型实例化。”

根据经验，我建议始终在模块函子之外定义归纳类型。我想你的类型foo 会依赖于模块s 的一些属性，所以你必须让它更通用一点：

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.