自然数列表的拆分

Question

我有一个自然数列表，希望在列表中的每个"new"元素处将其分解。为了更清楚，如果我有列表[5; 5; 5; 10; 10; 15; 15]，那么我希望有三个列表作为输出：[5; 5; 5]、[10; 10]和[15; 15]。我遇到的主要问题是，我不知道如何在Fixpoint上输出几个元素。我想我需要嵌套Fixpoint，但我不知道怎么做。作为一个非常原始的想法，我有：

Fixpoint count (v:nat) (l:list nat) : nat :=
match l with
| [] => 0
| h :: t => (if beq_nat h v then 1 else 0) + (count v t)
end.
Fixpoint prefix (n: count)( l :list nat)=
match l with
| [] => []
| m :: l' => if beq_nat count  m then []
else m :: prefix n l'
end.

Answer 1

我认为在这个例子中不需要嵌套固定点。这看起来像是，您需要一个累加器来记住您已经收集的列表。您想要的是一个返回以下类型的函数：list (list nat)

通过prefix功能，您可以添加一个新参数(最初设置为空列表[](，该参数可以记住您已经识别的相同数字的列表：

Fixpoint prefix (acc: list (list nat)) (n: count)( l :list nat)=
match l with
| [] => acc
| m :: l' => 
(* Here some code that depending if m is equal to n will either 
add a new list to acc or add a new element to the first list of acc *)
end.

我没有试图在答案上更精确，因为这看起来像是一个家庭作业。

我建议您尝试使用函数式编程语言(如OCaml或Haskell(编写代码，而不使用命令式部分(分配等(，然后尝试在Coq中模仿它(如果这对您来说更容易的话(。

您可能还想查看一些在线资源，了解如何在函数式编程中使用累加器。

还要注意，前缀的代码不会编译。