为什么这个 Coq 定义失败了？归纳类型的 Coq 命名空间错误

Question

我有以下感应类型和测试功能：

Inductive parameter : Type :=
| Nop
| OneP : forall A, A -> parameter  
| TwoP : forall (A : Type) (r : nat) (b : A), parameter
.
Check (TwoP nat 1 5).


Definition test (p : parameter) : option (nat * nat) :=
match p with 
| TwoP nat x y => Some (x, y)
| _ => None
end.

测试功能失败并出现错误：

术语“Some (x, y)”的类型为“option (Datatypes.nat * nat)”，而预期的类型为“option (Datatypes.nat * Datatypes.nat)”。

我不明白为什么我的定义不起作用。nat 和 Datataypes.nat 之间有区别吗？

任何帮助，将不胜感激。谢谢！

Answer 1

在 Coq 中，不可能测试类型是什么。考虑以下程序：

Definition is_nat (A : Type) : bool :=
  match A with
  | nat => true
  | _   => false
  end.

如果您尝试运行它，Coq 会告诉您最后一个分支是多余的，并拒绝该定义。问题是它nat被视为变量名，而不是nat标准库中的数据类型。因此，第一个分支匹配每个 type A，而最后一个分支是多余的。在您的示例中，模式nat最终屏蔽了数据类型nat，这就是您最终看到限定名称的原因Datatypes.nat。

解决此问题的一种方法是使用一种代码而不是Type. 例如：

Inductive type : Type :=
| Bool
| Nat.

Definition type_denote t : Type :=
  match t with
  | Bool => bool
  | Nat => nat
  end.

Coercion type_denote : type >-> Sortclass.

Inductive parameter : Type :=
| Nop
| OneP : forall (A : type), A -> parameter
| TwoP : forall (A : type) (r : nat) (b : A), parameter
.
Check (TwoP Nat 1 5).

Definition test (p : parameter) : option (nat * nat) :=
match p with
| TwoP Nat x y => Some (x, y)
| _ => None
end.

该解决方案有两个问题。首先，它要求您预测 中需要的所有类型parameter，并将这些类型添加到 的定义中type。其次，它迫使您使用依赖类型进行编程，这可能很难操作。尽管没有万能的解决方案，但也许可以重构您的定义来完全避免类型匹配问题——这取决于您的应用程序。