coq - 将整数列表转换为自然数列表

Question

我想将 alist of integer转换为 a list of nat。这是我返回的函数Coq。

Fixpoint list_int_to_nat (l : list integer) : list nat :=
    match l with
      | nil => nil
      | x :: l' => let i := Z.to_nat x in
        list_int_to_nat l'
    end.

你能帮我把列表的每个元素翻译integer成一个列表吗nat，因为在我的函数中我没有使用第一个元素i？非常感谢您的帮助。

Answer 1

您还可以使用map：

Definition list_int_to_nat l := map Z.to_nat l.

Answer 2

你写了一个递归函数，它总是在尾部调用自己，而你对头部什么都不做，所以最终你的函数总是返回nil。

您在这里想要的是使用cons构造函数 from在返回列表的开头list添加。i

Fixpoint list_int_to_nat (l : list integer) : list nat :=
    match l with
    | nil => nil
    | x :: l' => let i := Z.to_nat x in
       i :: list_int_to_nat l'
end.

（这里我使用了 :: 表示法，我觉得它更方便）。

这应该可以解决问题。