为什么这个 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)” 虽然它应该具有类型“选项（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.

的原因

解决此问题的一种方法是使用一种代码而不是 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 的定义中。其次，它迫使您使用难以操作的依赖类型进行编程。尽管没有 one-size-fits-all 解决方案 -- 这取决于您的应用程序，但可以重构您的定义来完全避免类型匹配问题。

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

Why does this Coq Definition fail? Coq Namespace error for Inductive Type

coq