功能证明（Haskell）

Question

我没有阅读RWH；而不是一个人退出，我下了命令[[Haskell：函数式编程的技巧]]。现在，我对第146页的这些功能证明感到好奇。具体地说，我正在尝试证明8.5.1 sum (reverse xs) = sum xs。我可以做一些归纳证明，但后来我被卡住了。HYP：

sum ( reverse xs ) = sum xs

BASE：

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

INDUCTION：

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

所以现在我只是想证明Left sum ( reverse xs ++ [x] )等于Right x + sum xs，但这与我从sum ( reverse (x:xs) ) = sum (x:xs)开始的位置相差不远。

我不太确定为什么需要证明这一点，使用reverse x:y:z = z:y:x的符号证明（通过defn）似乎是完全合理的，并且因为+是可交换的（对数），所以reverse 1+2+3 = 3+2+1，

我没有阅读RWH；而不是一个人退出，我下令Haskell：函数式编程的技巧。现在，我对第146页的这些功能证明感到好奇。具体地说，我正在尝试证明8.5.1 ...

Answer 1

sum (reverse [])     = sum []                     -- def reverse
sum (reverse (x:xs)) = sum (reverse xs ++ [x])    -- def reverse
                     = sum (reverse xs) + sum [x] -- sum lemma below
                     = sum (reverse xs) + x       -- def sum
                     = x + sum (reverse xs)       -- commutativity assumption!
                     = x + sum xs                 -- inductive hypothesis
                     = sum (x:xs)                 -- definition of sum

但是，没有严格保证有关联性和可交换性的基本假设，对于违反这些假设的Float和Double等许多数值类型，这将无法正常工作。

Answer 2

基本上您需要证明这一点

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

Answer 3

使用总和的定义将x（sum reverse xs ++ [x]）分解为x + sum（reverse（xs）），并使用归纳假设，您知道sum（reverse（xs））= sum（xs ）。但是我同意，对于这样的问题，归纳法是矫kill过正。

Answer 4

[我认为您在这里被困。您需要证明以下引理：

sum (xs ++ ys) == sum xs + sum ys

Answer 5

我不是证明专家，但这是我想出的，其中xs代表上一步的结果。

lemma 1: prove x + sum xs = sum x:xs
base: sum [] = 0
induction: sum x:xs = x + sum xs where [x | x <- xs]

lemma 2: prove sum xs + sum ys = sum (xs ++ ys)
base: sum [] + sum [] = 0
induction: (x + sum xs) + (y + sum ys) = sum (x:xs ++ y:ys) where 
    [(x, y) | (x, y) <- zip xs ys]