Theorem 20. sum (map (1+) xs) = length xs + sum xs

Proof. Induction over xs. The base case is

sum (map (1+) [ ])

= sum [ ] { map.1 }

= 0+sum [ ] { 0 + x = x }

= length [ ] + sum [ ] { length.1 }

For the inductive case, assume sum (map (1+) xs) = length xs + sum xs.

Then

sum (map (1+) (x : xs))

= sum ((1 + x) : map (1+) xs) { map.2 }

= (1+x) + sum (map (1+) xs) { sum.2 }

= (1+x) + (length xs + sum xs) { hypothesis }

= (1+length xs) + (x + sum xs) { (+).algebra }

= length (x : xs) + sum (x : xs) { length.2, sum.2 }

The foldr function is important because it expresses a basic looping pattern.

There are many important properties of foldr and related functions. Here is

one of them:

Exercise 8. Recall Theorem 20, which says sum (map (1+) x8) -length xs+ sum xs. Explain in English what this theorem says. Using the definitions of the functions involved (sum, length and map), calculate the values of the left and right-hand sides of the equation using x. 1, 2, 3, 4). Exercise 8. Recall Theorem 20, which says sum (map (1+) x8) -length xs+ sum xs. Explain in English what this theorem says. Using the definitions of the functions involved (sum, length and map), calculate the values of the left and right-hand sides of the equation using x. 1, 2, 3, 4)