coq - 为什么这个 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 数据类型。因此，第一个分支匹配每个类型 A，而最后一个分支是多余的。在您的示例中，模式 nat 最终屏蔽了数据类型 nat，这就是您最终看到限定名称 Datatypes.nat 的原因。

解决此问题的一种方法是使用代码类型而不是类型。例如:

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 的定义中。其次，它迫使您使用依赖类型进行编程，这可能很难操作。尽管没有万能的解决方案，但也许可以重构您的定义来完全避免类型匹配问题——这取决于您的应用程序。