Индукция в списках - Доказательство Сильной Собственности (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. Затем он установил индуктивную гипотезу, включающую "для всех акк", а затем установил акк в 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 в этом случае.