我如何证明如果sumlist=10，则sumlist==sum（反向列表）？
我想过这样一个理由：“反向不会改变列表中的值，所以这个陈述是正确的。”
但我想知道我是否可以用更完整的答案来证明这一点。
以下是我正在使用的定义：
reverse :: [a] -> [a]
reverse [] = []
reverse (x : xs) = reverse xs ++ [x]
sum :: Num a => [a] -> a
sum [] = 0
sum (x : xs) = x + sum xs
编辑：所以我问了我的教授，他告诉我使用这个总和定义
sum :: [Int] -> Int
sum [] = 0
sum (x : xs) = x + sum xs
回答
你不能在一般情况下证明它，因为它只适用于其实现(+)是可交换和关联的类型。此属性不适用于 Double，例如：
Prelude> list = 1e16 : replicate 10 1 :: [Double]
Prelude> sum list
1.0e16
Prelude> sum (reverse list)
1.000000000000001e16
回答
您将通过归纳证明，假设(+)是可交换和关联的 with 0as an identity（这是 的通常假设Num）。我们还必须使用 的定义(++)，即：
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
我们需要知道这个关于求和和追加到末尾的属性：
引理1
sum (xs ++ [x]) = sum xs + x。证明。基本情况：
sum ([] ++ [x]) = sum [x] -- definition of (++) = x + sum [] -- definition of sum = x + 0 -- definition of sum = x -- 0 identity of +感应案例：
Suppose sum (xs ++ [x]) = sum xs + x (inductive hypothesis) sum ((x':xs) ++ [x]) = sum (x' : (xs ++ [x])) -- definition of (++) = x' + sum (xs ++ [x]) -- definition of sum = x' + (sum xs + x) -- inductive hypothesis = (x' + sum xs) + x -- (+) associative = sum (x' : xs) + x -- definition of sum (right to left)Qed。
有时在找到这些等式证明时，“从两端”工作是有帮助的——试图减少两者sum ((x' : xs) ++ [x])并sum (x' : xs) + x在中间减少相同的东西。简单证明的结构通常遵循以下模式：
- 使用定义（从左到右）
- 使用重要的性质（归纳假设，或交换性，或你有什么）
- 使用定义（从右到左）
现在我们可以继续主定理，它将以类似的方式进行（利用引理）。
定理：
sum (reverse xs) == sum xs【读者练习】
Qed。
希望这是有帮助的。
THE END
二维码