Coq：错误：在当前环境中找不到引用_ [英] Coq: Error: The reference _ was not found in the current environment

问题描述

我是Coq的新手。
我在使用单位，乘积和总和定义列表，地图和树木时遇到了麻烦。
我得到标题中的错误消息。
注释上方的代码可以正常工作，而注释下方的代码则不能正常工作。

I'm new to Coq. I'm having trouble defining lists, maps, and trees using units, products, and sums. I get the error message in the title. The code above the comment works fine, the code below it does not.

Inductive one : Type := nil : one.

Inductive sum (t0 t1 : Type) : Type :=
  | inject_left : t0 -> sum t0 t1
  | inject_right : t1 -> sum t0 t1.

Inductive product (t0 t1 : Type) : Type := pair : t0 -> t1 -> product t0 t1.

Definition list (t0 : Type) : Type := sum one (product t0 (list t0)).

Definition map (t0 t1 : Type) : Type := list (product t0 t1).

(* From here on nothing works. *)

Definition List (t0 : Type) : Type := sum one (product t0 (List t0)).

Definition map (t0 t1 : Type) : Type :=
  sum one (product (product t0 t1) (map t0 t1)).

Definition Map (t0 t1 : Type) : Type :=
  sum one (product (product t0 t1) (Map t0 t1)).

Definition tree (t0 : Type) : Type :=
  sum one (product t0 (product (tree t0) (tree t0))).

Definition Tree (t0 : Type) : Type :=
  sum one (product t0 (product (Tree t0) (Tree t0))).

推荐答案

Definition List (t0 : Type) : Type := sum one (product t0 (List t0)).

在Coq中，无法使用 Definition ，则需要使用 Fixpoint （或更强的功能）。参见 http://coq.inria.fr/refman/Reference-Manual003.html ＃@ command14

In Coq, you cannot write a recursive function by using Definition, you need to use Fixpoint (or something stronger). See http://coq.inria.fr/refman/Reference-Manual003.html#@command14

现在，这还不是全部，但是必须以可证明的方式终止递归定义（以确保所用逻辑的一致性）。特别是，您不能这样写：

Now, that's not all, but a recursive definition has to be provably-terminating (to ensure consistency of the logic you use). In particular, you cannot write something like:

Fixpoint List (t0 : Type) : Type := sum one (product t0 (List t0)).

由于您要对输入的同一个参数进行递归调用，因此显然无法终止

Since you're doing a recursive call on the same argument you got in. This obviously fails to terminate.

无论如何，要定义此类类型，您可能应该使用 Inductive （和 CoInductive ），

Anyway, to define types like these, you should probably rather use Inductive (and CoInductive), as you already figured out.

这篇关于Coq：错误：在当前环境中找不到引用_的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！