功能证明(Haskell)

Question

我在阅读RWH时失败了; 而不是一个退出,我命令Haskell:功能编程工艺.现在我对第146页的这些功能性证据感到好奇.特别是我试图证明8.5.1 sum (reverse xs) = sum xs.我可以做一些感应证明,但后来我卡住了..

HYP:

sum ( reverse xs ) = sum xs

基础:

sum ( reverse [] ) = sum []

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

Right = 0          (sum.1)

感应:

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,

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

However, there are underlying assumptions of associativity and commutativity that are not strictly warranted and this will not work properly for a number of numerical types such as Float and Double where those assumptions are violated.

Lemma: sum (xs ++ ys) == sum xs + sum ys given the associativity of (+)

Proof:

sum ([] ++ ys)     = sum ys           -- def (++)
                   = 0 + sum ys       -- identity of addition
                   = sum [] ++ sum ys -- def sum

sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))  -- def (++)
                   = x + sum (xs ++ ys)    -- def sum 
                   = x + (sum xs + sum ys) -- inductive hypothesis
                   = (x + sum xs) + sum ys -- associativity assumption!
                   = sum (x:xs) + sum ys   -- def sum

Answer 2

基本上你需要证明这一点

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

然后很容易导致

                        = x + sum (reverse xs)
                        = x + sum xs  -- by inductive hyp.

问题是显示sum分布在列表串联上.