Haskell中结构归纳证明：(take n . map f) xs = (map f . take n) xs

已知定义 #

首先明确题目给出的Haskell函数定义：

take :: Int -> [a] -> [a]
take 0 _ = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = f x : map f xs

(.) :: (b -> c) -> (a -> b) -> a -> c
(.) f g x = f(g x)

证明过程 #

我们先利用函数组合的定义，把原等式两边展开，将问题转化为更直观的形式：

• 左边：(take n . map f) xs = take n (map f xs)（依据：函数组合(.)的定义，(f.g)x = f(gx)）
• 右边：(map f . take n) xs = map f (take n xs)（同样依据(.)的定义）

因此只需证明：take n (map f xs) = map f (take n xs) 对任意函数f、整数n、有限列表xs成立，采用结构归纳法分情况讨论：

情况1：xs是空列表[] #

• 左边：take n (map f []) = take n []（依据：map的定义，map _ [] = []）
  再根据take的定义take _ [] = []，左边结果为[]
• 右边：map f (take n []) = map f []（依据：take的定义，take _ [] = []）
  再根据map的定义map _ [] = []，右边结果为[]
• 左边=右边，此情况成立。

情况2：xs是非空列表(x:xs')（xs'是xs的尾部，有限列表） #

再细分n的取值：

子情况2.1：n=0

• 左边：take 0 (map f (x:xs')) = []（依据：take的定义，take 0 _ = []）
• 右边：map f (take 0 (x:xs')) = map f []（依据：take的定义，take 0 _ = []）
  再根据map的定义，右边结果为[]
• 左边=右边，此子情况成立。

子情况2.2：n>0

• 左边：take n (map f (x:xs')) = take n (f x : map f xs')（依据：map的定义，map f (x:xs) = f x : map f xs）
  再根据take的定义（n>0且列表非空），take n (y:ys) = y : take (n-1) ys，代入得：左边 = f x : take (n-1) (map f xs')
• 右边：map f (take n (x:xs')) = map f (x : take (n-1) xs')（依据：take的定义，take n (x:xs) = x : take (n-1) xs）
  再根据map的定义，map f (y:ys) = f y : map f ys，代入得：右边 = f x : map f (take (n-1) xs')
• 此时，根据归纳假设：对于有限列表xs'，take (n-1) (map f xs') = map f (take (n-1) xs')成立（因为xs'长度比xs小，有限列表的归纳基础已在情况1验证）
• 因此左边的后半部分与右边的后半部分相等，最终左边=右边，此子情况成立。

综上，所有可能情况均满足等式，原命题得证。

入手方法与通用证明思路 #

这类函数式编程中的等式证明，核心思路是利用递归结构的定义，通过归纳法拆解问题，具体步骤如下：

1. 先展开定义简化问题：遇到函数组合、递归函数，先根据给定定义把复杂表达式拆成基础函数的嵌套调用，比如先把(f.g)x展开成f(gx)，降低问题复杂度。
2. 选择合适的归纳方式：针对列表的问题优先用结构归纳法，因为列表本身是递归定义的（空列表或x:xs），分这两种情况讨论可以覆盖所有有限列表；如果涉及整数参数，可在列表归纳的子情况里再细分参数的边界值（比如n=0和n>0）。
3. 穷尽边界情况：先处理所有无需递归的边界（空列表、参数为0等），这些情况通常直接套用定义就能得出相等结论，是归纳证明的基础。
4. 递归情况依赖归纳假设：对于非边界的递归情况，把问题缩小到更小的子问题（比如列表的尾部、参数减1），利用“子问题已成立”的归纳假设，推导出当前情况的等式成立。
5. 每一步标注依据：确保所有变形都有明确的定义或假设支持，避免逻辑跳跃，让证明过程清晰可追溯。

内容的提问来源于stack exchange，提问作者Tamakas