Coq: 错误: 在当前环境中找不到引用 _

Question

我是Coq的新手。我在使用单位、乘积和总和定义列表、地图和树时遇到问题。我在标题中收到错误消息。注释上面的代码工作正常，它下面的代码不能。

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))).

Answer 1

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

在 Coq 中，你不能使用 Definition 编写递归函数，你需要使用 Fixpoint（或更强的东西）。见 http://coq.inria.fr/refman/Reference-Manual003.html#@command14

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

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

因为你正在对你进入的相同参数进行递归调用。这显然无法终止。

---

无论如何，要定义这样的类型，您可能应该使用 Inductive（和CoInductive），正如您已经发现的那样。