gpt4 book ai didi

list-comprehension - 在 Coq 中重写列表理解

转载 作者:行者123 更新时间:2023-12-02 09:07:16 26 4
gpt4 key购买 nike

我有以下 Haskell 函数,它输出分割列表的所有可能方法:

split :: [a] -> [([a], [a])]
split [] = [([], [])]
split (c:cs) = ([], c : cs) : [(c : s1, s2) | (s1, s2) <- split cs]

一些示例输入:

*Main> split [1]
[([],[1]),([1],[])]
*Main> split [1,2]
[([],[1,2]),([1],[2]),([1,2],[])]
*Main> split [1,2,3]
[([],[1,2,3]),([1],[2,3]),([1,2],[3]),([1,2,3],[])]

我正在尝试在 Coq 中编写相同的函数,因为默认情况下没有模式匹配,而且我不想 define a notation for it然而,所以我决定编写一个递归函数:

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint split {X : Type} (l : list X) : list (list X * list X) :=
match l with
| [] => [([], [])]
| c::cs =>
let fix split' c cs :=
match cs with
| [] => []
| s1::s2 => (c++[s1], s2) :: split' (c++[s1]) s2
end
in
([], c :: cs) :: ([c], cs) :: split' [c] cs
end.

产生相同的结果:

     = [([], [1]); ([1], [])]
: list (list nat * list nat)
= [([], [1; 2]); ([1], [2]); ([1; 2], [])]
: list (list nat * list nat)
= [([], [1; 2; 3]); ([1], [2; 3]); ([1; 2], [3]); ([1; 2; 3], [])]
: list (list nat * list nat)

但是它太冗长了,有关于如何使用 Coq 中的 HOF 将其转换为更具可读性的函数的提示吗?

最佳答案

Haskell 版本中的理解是 map 的语法糖(或更一般地 flat_map)。

Fixpoint split {X : Type} (l : list X) : list (list X * list X) :=
match l with
| [] => [([], [])]
| c::cs =>
([], c :: cs) :: map (fun '(s1, s2) => (c :: s1, s2)) (split cs)
end.

关于list-comprehension - 在 Coq 中重写列表理解,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/56611464/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com