Furthermore, previously on the same chapter, it says that:
scanl f e = foldr g [e] where g x xs = e : map (f x) xs
Using this definition, I tried proving it by induction, but since I got stuck, I tried seeing if I could find some way to use the first duality theorem (with the foldl definition), or fusion, but to no avail.
The induction proof I wrote is the following:
scanl f e = foldr g [e]
where g y ys = e : map (f y) ys
By the principle of extensionality, this is equivalent to:
scanl f e xs = foldr g [e] xs
where g y ys = e : map (f y) ys
We prove this equality by induction on xs.
Case([]). For the left-hand side we reason
scanl f e []
= {scanl.1}
[e]
For the right-hand side
foldr g [e] []
= {foldr.1}
[e]
Case(x:xs). For the left-hand side we reason
scanl f e (x:xs)
= {scanl.2}
e : scanl f (f e x) xs
= {f has unit e}
e : scanl f x xs
= {induction hypothesis}
e : foldr g [x] xs
For the right-hand side
foldr g [e] (x:xs)
= {foldr.2}
g x (foldr g [e] xs)
= {definition of g}
e : map (f x) (foldr g [e] xs)
= {definition of map}
e : foldr ((:) . (f x)) [] (foldr g [e] xs)