I'll say right off the bat this is for an assignment, and I'm not looking for an answer - just some direction, since I've been working on it for quite a while now. Given the following tail-recursive sum function:
sumTR [ ] acc = acc
sumTR (x:xs) acc = sumTR xs (x + acc)
we have to prove by induction that:
sumTR xs (sumTR ys acc) = sumTR (ys ++ xs) acc
After proving the base case (inducting on xs and treating ys as a constant) I arrived at:
sumTR x:xs(sumTR ys acc) = ... = sumTR xs (x + sumTR ys acc)
sumTR (ys ++ x:xs) acc = ... = sumTR xs (sumTR ys (x + acc))
Our lecturer went through a simpler example (sum1 xs = sum2 xs, with sum1 being simple recursion), and when he reached the point where you can't make them any more similar, he proved a 'stronger property', by noting something like sum2 xs acc = acc + sum of xs. Then he set an inductive hypothesis involving 'for all acc', and then set acc to 0 later on.
The main problem I'm having is that acc is already on LHS and RHS, so I feel like I've gotten close but that I'm not really proving a stronger property (the question doesn't ask for it specifically, but I think we're supposed to use it). Also I'm not sure how extensively I'm allowed to use the associativity of addition when taking elements out (or inserting them into) the function.
Any help is appreciated!
It is much easier to do the induction on ys, since then for empty ys, we have
sumTR xs (sumTR [] acc) = -- by first case of (inner) sumTR
sumTR xs acc = -- by definition of (++)
sumTR ([] ++ xs) acc -- Q.E.D.
and for y:ys, we have
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.
Going with ys helped us because (++) is defined by recursion on its left-hand argument, which is ys in this case.