substitution in proofs with recursive formulas

The following problem and partial solution are from Richard Bird's Thinking Functionally with Haskell (pp 132-133, 139)

given

foldl f e (x:xs) = foldl f (f e x) xs
foldl f e [] = e

Prove foldl (@) e xs = foldr (<>) e xs for all finite lists xs provided that

(x <> y) @ z = x <> (y @ z)
e @ x = x <> e

induction case (left-hand side):

foldl (@) e (x:xs) = {def foldl}
foldl (@) (e @ x) xs = {proviso 2}
foldl (@) (x <> e) xs

This is obviously not the last step of the proof, but it's the source of my question: Because e is expanded recursively by foldl, it seems like its definition depends on the stage of the recursion, and therefore it's not clear to me that e @ x = x <> e is always a valid substitution. Above in foldl (@) (e @ x) xs, argument e of foldl takes on the value of e @ x, so I would think that proviso 2 can't be applied -- to make the substitution it would need to be (e @ x) @ x

Solution

This can be proved for e fixed in the statement of the theorem (i.e., with the identity e @ x = x <> e holding for all x but only a specific e), but it's quite a bit more complicated than the part of the proof you've shown. I don't have a copy of the original source, so I don't know how much additional guidance the solution gives.

Anyway, I found it helpful to first prove an intermediate result:

forall y, z, xs: foldl (@) (y <> z) xs = y <> foldl (@) z xs       -- (A)

This can be proved inductively on xs. The base case is:

foldl (@) (y <> z) []
= y <> z                    -- foldl definition
= y <> foldl (@) z []       -- foldl definition

The inductive case is:

foldl (@) (y <> z) (x:xs)
= foldl (@) ((y <> z) @ x) xs     -- foldl definition
= foldl (@) (y <> (z @ x)) xs     -- assumption #1
= y <> foldl (@) (z @ x) xs       -- inductive assumption for z: = z @ x
= y <> foldl (@) z (x:xs)         -- foldl definition

So, (A) is established.

Now, we can turn to the desired result:

forall xs. foldl (@) e xs = foldr (<>) e xs         -- (B)

which can also be proved inductively.

The base case is:

foldl (@) e []
= e                          -- foldl definition
= foldr (<>) e []            -- foldr definition

The inductive step is:

foldl (@) e (x:xs)
= foldl (@) (e @ x) xs            -- foldl definition
= foldl (@) (x <> e) xs           -- assumption #2 for fixed e only
= x <> foldl (@) e xs             -- intermediate result (A) specialized to z := e
= x <> foldr (<>) e xs            -- inductive assumption
= foldr (<>) e (x:xs)             -- definition of foldr