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所以你要把它做得更通用一点。

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.