如何证明Haskell中filter (all p) . cp = cp . map (filter p)等式？

首先明确几个核心函数的定义：

• 笛卡尔积函数 cp 的递归定义：

  cp :: [[a]] -> [[a]]
  cp []       = [[]]
  cp (xs:xss) = [x:ys | x <- xs, ys <- cp xss]
  

• filter (all p)：过滤出所有元素都满足谓词 p 的列表；map (filter p)：对输入列表的每个子列表，先过滤出满足 p 的元素，再执行笛卡尔积。

一、用融合律证明目标等式 #

这个等式完全可以通过针对递归函数的融合律来证明，本质上是融合律在笛卡尔积函数 cp 上的具体应用。

融合律的适用条件（针对cp） #

对于递归定义的函数 cp，若存在函数 f 和 g，满足：

1. f (cp []) = cp (map g [])
2. 对任意子列表 xs 和列表 xss，f (cp (xs:xss)) = cp (map g xs : map g xss)

则可推出 f . cp = cp . map g。

验证条件并推导 #

令 f = filter (all p)，g = filter p，逐一验证条件：

1. 基例验证（xss = []）

• 左边：f (cp []) = filter (all p) [[]] = [[]]（空列表满足all p）
• 右边：cp (map g []) = cp [] = [[]]
• 两边相等，基例成立。

2. 归纳步骤验证（假设xss = zss时等式成立，证明xss = xs:zss时成立）

• 左边展开：

  f (cp (xs:zss)) = filter (all p) [x:ys | x <- xs, ys <- cp zss]
  

  利用all p (x:ys) = p x && all p ys，过滤条件等价于p x且all p ys，因此左边可改写为：

  [x:ys | x <- xs, p x, ys <- cp zss, all p ys]
  

  根据归纳假设，filter (all p) (cp zss) = cp (map g zss)，同时x <- xs, p x等价于x <- filter p xs = g xs，代入后左边变为：

  [x:ys | x <- g xs, ys <- cp (map g zss)] = cp (g xs : map g zss) = cp (map g (xs:zss))
  

  这正是等式的右边，归纳步骤成立。

综上，filter (all p) . cp = cp . map (filter p)得证。

二、融合律本身的证明 #

以针对cp这类递归函数的融合律为例，用结构归纳法证明：

融合律的通用形式（针对递归列表函数） #

设递归函数h满足：

• h [] = e
• h (a:as) = k a (h as)

若函数f、g和递归函数h'满足：

1. f e = h' []
2. 对任意a和b，f (k a b) = k' (g a) (f b)（其中h' (a:as) = k' a (h' as)）

则有 f . h = h' . map g。

归纳证明 #

1. 基例（as = []）

• 左边：f (h []) = f e = h' []
• 右边：h' (map g []) = h' []
• 两边相等，基例成立。

2. 归纳步骤（假设as = zs时等式成立，证明as = a:zs时成立）

• 左边：f (h (a:zs)) = f (k a (h zs)) = k' (g a) (f (h zs))（根据融合条件2）
• 右边：h' (map g (a:zs)) = h' (g a : map g zs) = k' (g a) (h' (map g zs))（根据h'的递归定义）
• 根据归纳假设f (h zs) = h' (map g zs)，左边与右边相等，归纳步骤成立。

融合律得证。

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