递归公式证明替换疑问：foldl与foldr等价性证明困惑

内容出自Richard Bird所著《Thinking Functionally with Haskell》（第132-133、139页）

给定foldl的定义：

foldl f e (x:xs) = foldl f (f e x) xs
foldl f e [] = e

需证明：对于所有有限列表xs，当满足以下两个前提时，foldl (@) e xs = foldr (<>) e xs

前提条件：

• 结合律：(x <> y) @ z = x <> (y @ z)
• 单位元交换：e @ x = x <> e

归纳步骤中的疑问 #

在推导左侧表达式时，有如下步骤：

foldl (@) e (x:xs) = {foldl定义} 
foldl (@) (e @ x) xs = {前提2} 
foldl (@) (x <> e) xs

这一步并非证明的最终步骤，但却是疑问的来源：由于foldl会递归展开，其初始参数e会在递归中被替换，因此不确定前提2是否始终适用。比如在foldl (@) (e @ x) xs中，foldl的初始参数已经变成了e @ x，所以觉得不能直接应用前提2——如果要替换，应该是针对(e @ x) @ x这类形式，而非原本的e @ x。

完整证明补充 #

为完成等价性证明，我们需要先证明一个辅助归纳假设：foldl (@) (x <> y) xs = x <> foldl (@) y xs，再结合原命题进行推导。

原命题推导过程 #

两侧化简结果不同，因此需要引入辅助归纳假设：

foldl (@) (x <> y) xs = x <> foldl (@) y xs


该假设的基础情况显然成立，以下是归纳步骤的推导：

辅助归纳假设的证明 #

结合辅助归纳假设，原命题左侧的foldl (@) (x <> e) xs可转化为x <> foldl (@) e xs，与右侧结果一致，从而完成原命题的证明。

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