列表中的歸納 - 證明更強的屬性（Haskell）

Question

我會馬上說出這是一個任務，我不是在尋找答案 - 只是某個方向，因爲我一直在爲它現在有一段時間了。給出下面的尾遞歸總和函數：

sumTR [ ] acc = acc 
sumTR (x:xs) acc = sumTR xs (x + acc) 

我們通過感應來證明：

sumTR xs (sumTR ys acc) = sumTR (ys ++ xs) acc 

證明基本情況（中引起上XS和治療YS爲恆定）之後，我到達：

sumTR x:xs(sumTR ys acc) = ... = sumTR xs (x + sumTR ys acc) 
sumTR (ys ++ x:xs) acc = ... = sumTR xs (sumTR ys (x + acc)) 

我們的講師通過一個簡單的例子去（SUM1 XS = SUM2 XS，用SUM1是簡單而又重複的），當他到達的地步，你不能讓他們更多的相似，他證明通過記下sum2 xs acc = acc + xs的總和這樣的「更強的屬性」。然後，他設置了一個歸納假設，涉及'for all acc'，然後在以後設置爲0。

我遇到的主要問題是acc已經在LHS和RHS上，所以我覺得我已經接近了，但是我並沒有真正證明它是一個更強大的屬性（問題並沒有要求它具體而言，但我認爲我們應該使用它）。此外，我不確定在將元素取出（或將其插入）函數時，我可以使用多少的添加關聯性。

任何幫助表示讚賞！

Answer 1

這是很容易做到的ys感應，從此空ys，我們有

sumTR xs (sumTR [] acc) = -- by first case of (inner) sumTR 
sumTR xs acc =    -- by definition of (++) 
sumTR ([] ++ xs) acc  -- Q.E.D. 

和y:ys，我們有

sumTR xs (sumTR (y:ys) acc) = -- by second case of (inner) sumTR 
sumTR xs (sumTR ys (y + acc)) = -- by induction 
sumTR (ys ++ xs) (y + acc) =  -- by second case of sumTR, "in reverse" 
sumTR (y:(ys ++ xs)) acc =  -- by definition of (++) 
sumTR ((y:ys) ++ xs) acc   -- Q.E.D. 

與ys去幫助我們，因爲(++)是通過左邊參數遞歸來定義的，在這種情況下爲ys。