2

我是 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))).
4

1 回答 1

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

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

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

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

由于您正在对输入的同一参数进行递归调用。这显然无法终止。

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

于 2012-07-02T05:24:19.010 回答