# 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?

• I do not completely understand your notation. You seem to be describing some fix-point operators. Is the notation well known? If so, it is probably a good idea to mention a name or link. – Discrete lizard Apr 10 '17 at 20:08
• @Discretelizard sorry about that. I used Haskell syntax. – futtetennista Apr 14 '17 at 8:35

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$

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*}

• Regarding "I'm not aware of more elegant approaches": the property which is proven here is exactly the free theorem associated to the (poly)type of subs, namely [a] -> [[a]]. Indeed, we don't even need to look at the code of subs, its type (and its termination) suffices! The property can also be recognized by category theorists as the naturality condition between the functor [-] and the functor [[-]]. We can even use a tool to deduce these properties. – chi Apr 11 '17 at 20:10