How to use structural induction to prove law on lists

I want to prove that the following equation holds using structural induction on (finite) lists

subs (map f xs) = map (map f) (subs xs)

where subs [] = [[]]                                          (subs.1)
      subs (x:xs) = subs (xs) ++ map (x:) (subs xs)           (subs.2)

      map f [] = []                                           (map.1)
      map f (x:xs) = f x : map f xs                           (map.2)

: is the cons operator and ++ the join operator on lists.

I'm using structural induction on xs, the base step for [] is easy to prove but I hit a wall when trying to solve the inductive step for (x:xs)

subs (map f) (x:xs)                                             (map.2)
subs (f x : map f xs)                                           (subs.2)
subs (map f xs) ++ map ((f x):) (subs (map f xs))               (hyp)
(map (map f) (subs xs)) ++ map ((f x):) (map (map f)(subs xs))

From here I couldn't find a way to proceed so I moved to the right-hand side of the equation and I kind of found a way to find a "proof" but something tells me that it's bogus

map (map f) (subs (x:xs))                     (subs.2)
map (map f) (subs xs ++ map (x:) (subs xs))   (generalise term)
map (map f) ys                                (hyp)
subs (map f ys)                               ???
subs (map f (y:ys)) 
□

My reasoning here is: (x:xs) is a list with at least length 1, it should be legal to generalise subs xs ++ map (x:) (subs xs) as either (y:ys) or ys (because (x:xs) is not empty) so I chose the latter first to be able to use the induction hypothesis and after that I rewritten ys as (y:ys) to establish the case.

Does this make any sense at all? If not, could anybody show me the right approach to tackle this proof?

You'll want a helper lemma to make this endeavor more digestible.

Notations for map and subs:

I'm going to condense the map notation a bit so that we can express it as the binary operator $f \diamond l = \mathrm{map} ~ f ~ l$. Similarly, we will express the subs as a unary operation $\lfloor\!\!\lfloor l \rfloor\!\!\rfloor = \mathrm{subs} ~ l$.

This might seem terse at the moment, but it's useful to visually capture a "commutativity" property we will illustrate in a moment that sits at the core of the proof of this extensional equation.

Reformulation of the problem:

We want to show that
$$
\lfloor\!\!\lfloor f \diamond l \rfloor\!\!\rfloor = (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor
$$

which basically states that if we try to hoist the $f$ outside of the brackets, then we have to turn it into a map.

Now, if we follow your original blueprint, your inductive hypothesis establishes that
$$
\lfloor\!\!\lfloor f \diamond x ::l \rfloor\!\!\rfloor = (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~(f ~x ::) \diamond ((f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor)
$$

In order for this proof to proceed, you need to tame the term on the righthand side of the concatenation. But what would you want it to look like?

Well, recall that maps distribute into concatenations:
$$
(f \diamond l_1) +\!\!\!+ ~(f \diamond l_2) = f \diamond (l_1 +\!\!\!+~ l_2)
$$

which suggests that we might be able to get our equation into an amenable form if we can rewrite the second term so that it is of the form $(f \diamond) \diamond \cdot$.

Here's where our helper lemma comes in to save the day:

Lemma ("Commutativity"):You have to use finger quotes when you read the name of this lemma out loud.
$$
(f ~x ::) \diamond ((f \diamond) \diamond l) = (f \diamond) \diamond ((x ::) \diamond l)
$$
Proof: Structural induction on $l$. This is actually a pretty easy proof, so I'll leave it to the reader™. However, the core of this proof is essentially showing that
\begin{align*}
(f~x ::) \diamond ((f \diamond) \diamond a :: [...]) &= (f~x ::) \diamond ((f \diamond a) :: \underbrace{((f \diamond) \diamond [...])}_{\text{induction hypothesis}}) \\
&= \underbrace{(f~x :: f \diamond a)}_{\text{map distributivity}} :: (f~x ::) \diamond((f \diamond) \diamond [...])) \\
&= (f \diamond (x :: a)) :: (f~x ::) \diamond((f \diamond) \diamond [...])) \\
& \text{discharge the induction hypothesis} \\
&= (f \diamond (x :: a)) :: (f \diamond) \diamond ((x ::) \diamond [...]) \\
& \text{distributivity} \\
&= (f \diamond) \diamond ((x :: a) :: ((x ::) \diamond [...])) \\
& \text{distributivity} \\
&= (f \diamond) \diamond ((x ::) \diamond (a :: [...]))
\end{align*}
which concludes the proof of the lemma. $\square$

Finishing your inductive proof:

Once we have this gem, we can continue your structural induction proof.

\begin{align*}
\lfloor\!\!\lfloor f \diamond x ::l \rfloor\!\!\rfloor &= (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~(f ~x ::) \diamond ((f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor) \\
& \text{by the lemma} \\
&= (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~(f\diamond) \diamond ((x ::) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor) \\
& \text{by distributivity of map} \\
&= (f \diamond) \diamond (\lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~ (x::) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor) \\
& \text{by the definiton of } \lfloor\!\!\lfloor x :: l \rfloor\!\!\rfloor \\
&= (f \diamond) \diamond \lfloor\!\!\lfloor x :: l \rfloor\!\!\rfloor
\end{align*}

which satisfies your goal.

The equational acrobatics we've just performed seems a bit excessive, which is why I'm willing to bet that there's some elegant fusion law, recursion scheme, or some other representation (probably some categorical law given the nature of the problem) that nicely unwraps this proof. Unfortunately, AFAIK, I'm not aware of more elegant approaches. While this is a valid proof, it's somewhat unsatisfying. It is as much of a proof of this theorem as my performances of Taylor Swift is considered entertainment: it is technically correct, just not in the way that I intend it to be.

StackExchange Computer Science Q#72672, answer score: 4