coq - 如何在coq中对列表进行分区
问题描述
我有一个自然数列表，想将其分成三个列表，比例为 3:2:1。想使用分区功能。请指导我
定点分区 (l:list A) : list A * list A := match l with | 无=>（无，无）| x :: tl => let (g,d) := partition tl in if fx then (x::g,d) else (g,x::d) end。
解决方案
您的问题未详细说明，但这里有几个指针：
首先，您的函数可能与 不同partition，因为partition假设存在一个函数，给定列表中的一个元素，该函数知道它属于分区的哪一部分。
但是，鉴于您的松散规范，似乎元素应该属于三个分区之一，而不是基于它们自己的值，而是基于它们出现的列表的某些属性以及有多少其他元素。
这是解决此问题的一种方法：在分区中的值分布没有外部约束的情况下，您可以通过将列表划分为 6 个相等的分区，然后将 3 个分区组合在一起来获得 3:2:1 的比率，并将2个分区分开。
现在的问题是要有一个创建n分区的功能。根据您的技能水平，以及您是否需要编写有关该功能的证明，可能有不同的方法来解决它。
n编写一个返回任何列表的实际函数n将需要具有某些n-ary 产品类型的依赖类型。你可以通过一个函数来伪造它：
get_partitions : list T -> (n : nat) -> (i : nat) -> list T
这样get_partitions l n i过滤lat 索引i、i + n、i + 2n等的元素（即索引等于imod的元素n）。
然后你可以得到你的六个分区get_partitions l 6 0, get_partitions l 6 1, ..., get_partitions l 6 5。
这将是一个易于编写的解决方案，但可能不是最好的证明目的......有人可能有更好的想法。:-)