Induction sur les listes - Prouver une propriété plus forte (Haskell)

Question

Je dirais dès le départ que c'est pour une mission, et je ne cherche pas de réponse - juste une direction, depuis que je travaille dessus pour assez longtemps maintenant. Compte tenu de la fonction somme récursive suivante:

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

nous devons prouver par induction que:

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

Après avoir prouvé le cas de base (introniser sur xs et le traitement ys comme une constante) je suis arrivé à :

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

Notre professeur est passé par un exemple plus simple (Som1 xs = SUM2 xs, avec sum1 étant récursion simples), et quand il a atteint le point où vous ne pouvez pas les rendre plus semblable, il prouve d une «propriété plus forte», en notant quelque chose comme sum2 xs acc = acc + somme de xs. Puis il a mis une hypothèse inductive impliquant «pour tous les acc», puis mis ACC à 0 plus tard. Le principal problème que j'ai est que l'acc est déjà sur LHS et RHS, donc je me sens comme si je suis proche mais que je ne prouve pas vraiment une propriété plus forte (la question ne le demande pas) spécifiquement, mais je pense que nous sommes supposés l'utiliser). Aussi je ne suis pas sûr combien je suis autorisé à utiliser l'associativité de l'addition quand on enlève des éléments (ou les insère dans) la fonction.

Toute aide est appréciée!

Answer 1

Il est beaucoup plus facile de faire l'induction sur ys, depuis lors, pour vide ys, nous avons

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

et y:ys, nous avons

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. 

Voulez-vous profiter ys nous a aidés parce que (++) est défini par la récursivité sur son argument de gauche, qui est ys dans ce cas.