coq - Coq 中的产品类型

Question

我在将参数传递给 coq 中的产品类型时遇到问题。我有一个看起来像这样的定义，

    Definition bar (a:Type) := a->Type.

我需要定义一个函数，它接收“a”和“bar a”生成的东西并输出它们的乘积/有序对。所以我尝试了以下方法。

    Definition foo (a:Type)(b:bar a):= prod a b.

这给了我错误

The term "b" has type "bar a" while it is expected to have type "Type".

这里真正令人困惑的是，

    Definition foo (a:Type) := prod a (bar a). 

工作正常。显然“bar a”的类型为“Type”，所以我不确定如何修复我的原始定义。我怀疑我没有正确传递变量。

Answer 1

要查看错误，请展开 foo 定义中的 bar a:

Definition foo (a:Type)(b:a->Type):= prod a b.

现在应该清楚了，b不是一个类型，它是一个从a到Type的函数。

并且由于您永远不会获得 a 类型的对象，因此您无法将 b 应用于任何对象，也无法获得 Type 来自它。

对于第二个定义，再次展开看看它为什么有效:

Definition foo (a:Type) := prod a (a->Type).

a 和 a->Type 都是产品的有效 Type。