2

我在Coq中定义了以下归纳类型。

Inductive natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l) (at level 60, right associativity). 
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y  nil) ..).

natlist 基本上是一个自然数列表（类似于 Python 中的列表）。我正在尝试使用下面的定义找到两个 natlist 的联合。

Definition union_of_lists : natlist -> natlist -> natlist

即 Eval simpl in (union_of_lists [1,2,3] [1,4,1]) 应该返回 [1,2,3,1,4,1]

我有以下疑问。

  • 由于这个定义没有参数，我如何实际获取输入并处理它们？
  • union_of_lists 的定义究竟返回了什么？它只是一个natlist吗？

非常感谢任何帮助或提示。

4

1 回答 1

1

我自己找到了答案 :) 我所做的是，我编写了一个单独的 Fixpoint 函数append，然后将其分配给union_of_lists.

Fixpoint append(l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | (h :: t) => h :: app t l2
  end.`

接着

Definition union_of_lists : natlist -> natlist -> natlist := append.

Eval simpl in (append [1,2,3] [1,2,3]) (* returns [1,2,3,1,2,3] *)

该定义union_of_lists返回一个函数，该函数接受natlist一个参数并返回另一个类型的函数natlist -> natlist（即函数接受一个natlist参数并返回 a natlist）。

这个定义union_of_lists类似于函数式编程中的函数，它可以返回一个函数或一个值。

于 2010-09-06T20:30:42.503 回答