如何证明若列表sum值为10，则sum list等于sum (reverse list)？

前置定义 #

证明过程用到的所有函数定义如下：

• reverse 函数定义：

reverse :: [a] -> [a]
reverse [] = []
reverse (x : xs) = reverse xs ++ [x]

• 教授指定的 sum 函数定义：

sum :: [Int] -> Int
sum [] = 0
sum (x : xs) = x + sum xs

• 列表拼接运算符 ++ 定义：

(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

前置引理证明 #

首先证明引理：对任意有限 Int 列表 xs、ys，有 sum (xs ++ ys) = sum xs + sum ys
采用结构归纳法对 xs 进行归纳：

1. 基例：xs = []
   左边：sum ([] ++ ys) = sum ys（由 ++ 的基例定义）
   右边：sum [] + sum ys = 0 + sum ys = sum ys（由 sum 的基例定义、Int 加法单位元性质）
   左边等于右边，基例成立。
2. 归纳假设：假设对于长度为 k 的列表 xs，引理成立，即 sum (xs ++ ys) = sum xs + sum ys
3. 归纳步骤：证明对于长度为 k+1 的列表 x:xs，引理成立
   左边：sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))（由 ++ 的归纳步骤定义）
   = x + sum (xs ++ ys)（由 sum 的归纳步骤定义）
   = x + (sum xs + sum ys)（代入归纳假设）
   右边：sum (x:xs) + sum ys = (x + sum xs) + sum ys（由 sum 的归纳步骤定义）
   = x + (sum xs + sum ys)（由 Int 加法的结合律）
   左边等于右边，归纳步骤成立。
   因此该引理对所有有限长度的 Int 列表成立。

原命题证明 #

原命题：对任意有限 Int 列表 xs，有 sum (reverse xs) = sum xs
采用结构归纳法对 xs 进行归纳：

1. 基例：xs = []
   左边：sum (reverse []) = sum [] = 0（由 reverse 的基例定义、sum 的基例定义）
   右边：sum [] = 0
   左边等于右边，基例成立。
2. 归纳假设：假设对于长度为 k 的列表 xs，原命题成立，即 sum (reverse xs) = sum xs
3. 归纳步骤：证明对于长度为 k+1 的列表 x:xs，原命题成立
   左边：sum (reverse (x:xs)) = sum (reverse xs ++ [x])（由 reverse 的归纳步骤定义）
   = sum (reverse xs) + sum [x]（代入前置引理）
   = sum (reverse xs) + (x + sum [])（由 sum 的归纳步骤定义）
   = sum (reverse xs) + (x + 0)（由 sum 的基例定义）
   = sum (reverse xs) + x（加法单位元性质）
   = sum xs + x（代入归纳假设）
   右边：sum (x:xs) = x + sum xs（由 sum 的归纳步骤定义）
   = sum xs + x（由 Int 加法的交换律）
   左边等于右边，归纳步骤成立。
   因此原命题对所有有限长度的 Int 列表成立。

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