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

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

• "You'll want a helper lemma" -- in my experience, that's almost always the fix. Prove something stronger, then go on. In induction proofs, that can mean to strengthen the claim to get a stronger induction hypothesis. – Raphael Apr 11 '17 at 17:33
• 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
• Of course, using free theorems for these exercises would be cheating -- since their goal is to make you practice with inductive proofs :-) – chi Apr 11 '17 at 20:11
• Thanks @chi! I had my suspicions that this would be a free theorem, I'm grateful for the literature reference :) – Lee Apr 11 '17 at 22:08
• Thanks @Lee ! I've re-done your proof step-by-step and I could "reproduce" it :) I suspected that was the way to go but I lacked the intuition about which lemma should I prove. I guess you get this kind of intuitions after doing a few induction proofs - just not there yet - so I'm curious to know if you folks can suggest any rules of thumb to determine which lemmas are useful. For example: when I re-did the proof manually I actually established the lemma as the last step, before I made sure it was really useful to establish the original proof. Is this how you folks do it? – futtetennista Apr 14 '17 at 8:28