Ваша проблема не указана, но вот пара указателей:
Во-первых, ваша функция, вероятно, будет отличаться от partition, потому что partition предполагает существование функции, которая, учитываяодин элемент из списка, знает, к какой части раздела он принадлежит.
Однако, учитывая вашу свободную спецификацию, кажется, что элементы должны принадлежать одному из трех разделов не на основе их собственного значения, а скореео каком-либо свойстве списка, в котором они появляются, и о количестве других элементов.
Вот один из способов решения этой проблемы: отсутствие внешних ограничений на распределение значений в разделахВы можете получить соотношение 3: 2: 1, разделив список на 6 равных разделов, а затем объединив вместе 3 раздела и раздельно 2 раздела.
Теперь проблема заключается в том, чтобы создать функцию для созданияn разделов. В зависимости от вашего уровня квалификации и того, нужно ли вам писать доказательства о функции, могут быть разные способы сделать это.
Написание фактической функции, которая возвращает n списков для любого *Для 1017 * потребуется зависимый тип с некоторым n -арным типом продукта. Вы можете подделать его, имея функцию:
get_partitions : list T -> (n : nat) -> (i : nat) -> list T
, так что get_partitions l n i фильтрует элементы l по индексам i, i + n, i + 2n и т. Д. (Т.е. элементы, чьиindex равен i mod n).
Тогда вы можете получить свои шесть разделов как get_partitions l 6 0, get_partitions l 6 1, ..., get_partitions l 6 5.
Thisбыло бы легко написать решение, но не может быть лучше для целей доказывания ... У кого-то могут быть лучшие идеи. : -)