如何在 Coq 中编写不带参数的定义？

Question

我在 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 的并集。

定义 union_of_lists : natlist ->纳特列表 -> natlist

即 在 (union_of_lists [1,2,3] [1,4,1]) 中计算 simpl 应该返回 [1,2,3,1,4,1]

我有以下疑问。

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

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

Answer 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参数并返回一个natlist的函数）。

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