如何在 Coq 中“专门化”一个多态类型？

Question

（注意，我的目标是了解更多关于 Coq 的信息，不一定要解决这个特定问题。IRL，我希望在这种情况下我会重构以删除有问题的类型。）

我有一个这样定义的类型：

Inductive natprod : Type := pair (n1 n2 nat).

我想让我的产品类型多态，所以我现在定义

Inductive prod {X Y : Type} : Type := pair (x : X) (y : Y).

但是，我不能在同一个模块中同时定义prod 和natprod，因为它们都有构造函数pair。但是我有一堆natprod的函数和定理，所以我不想扔掉natprod。相反，我基本上想说“当我写natprod 时，我的意思是prod nat nat。”

所以我尝试了这个：

Definition natprod := prod nat nat.

但是，我收到以下错误：

Illegal application (Non-functional construction): 
The expression "prod" of type "Type" cannot be applied to the term
 "nat" : "Set"

我怎样才能做我想做的事？

Answer 1

事实证明，问题在于X 和Y 被定义为prod 的隐式参数。我们可以通过强制它们显式来解决这个问题：

Definition natprod := @prod nat nat.

或者，

Notation natprod := (@prod nat nat).

更像是一个宏，不需要在证明中展开。