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

标签： modulecoq

Answer 1

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

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

根据经验，我建议始终在模块函子之外定义归纳类型。我想您的类型foo将取决于 module 的某些属性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.