Proof by induction with multiple lists

I am following the Functional Programming in Scala lecture on Coursera and at the end of the video 5.7, Martin Odersky asks to prove by induction the correctness of the following equation :

(xs ++ ys) map f = (xs map f) ++ (ys map f)

How to handle proof by induction when there are multiple lists involved ?

I have checked the base cases of xs being Nil and ys being Nil. I have proven by induction that the equation holds when xs is replaced by x::xs, but do we also need to check the equation with ys replaced by y::ys ?

And in that case (without spoiling the exercise too much...which is not graded anyway) how do you handle : (xs ++ (y::ys)) map f ?

This is the approach I have used on a similar example, to prove that

(xs ++ ys).reverse = ys.reverse ++ xs.reverse

Proof (omitting the base case, and easy x::xs case) :

(xs ++ (y::ys)).reverse
= (xs ++ (List(y) ++ ys)).reverse         //y::ys = List(y) ++ ys
= ((xs ++ List(y)) ++ ys).reverse         //concat associativity
= ys.reverse ++ (xs ++ List(y)).reverse   //by induction hypothesis (proven with x::xs)
= ys.reverse ++ List(y).reverse ++ xs.reverse //by induction hypothesis
= ys.reverse ++ (y::Nil).reverse ++ xs.reverse //List(y) = y :: Nil
= ys.reverse ++ Nil.reverse ++ List(y) ++ xs.reverse //reverse definition
= (ys.reverse ++ List(y)) ++ xs.reverse //reverse on Nil (base case)
= (y :: ys).reverse ++ xs.reverse         //reverse definition

Is this right ?

The property involves multiple lists, but ++ only recurses on its left argument. That's a hint that you can prove by induction on that left argument. In general, when proving a proposition about some recursive function, the first thing you try is inducting on the same argument that function recurses on.

I'll do this one for you as an example:

Claim: (xs ++ ys) map f = (xs map f) ++ (ys map f)

Proof: by induction on xs.

• Base case: xs = Nil

  • lhs = (Nil ++ ys) map f = ys map f

    (by ++'s definition)

  • rhs = (Nil map f) ++ (ys map f) = Nil ++ ys map f = ys map f

    (by map's, then ++'s definitions)

  • Hence lhs = rhs

• Inductive case: xs = z :: zs

  • hypothesis: (zs ++ ys) map f = (zs map f) ++ (ys map f)
  • goal: ((z :: zs) ++ ys) map f = ((z :: zs) map f) ++ (ys map f)

  • lhs = (z :: (zs ++ ys)) map f = f(z) :: ((zs ++ ys) map f) (1)

    (by map's definition)

  • rhs = ((z :: zs) map f) ++ (ys map f) = (f(z) :: (zs map f)) ++ (ys map f)

    (by map's definition)

  • in turn, rhs = f(z) :: ((zs map f) ++ (ys map f)) (2)

    (by ++'s definition)

  • From hypothesis, (1) and (2), we have proven goal.

Therefore, we have proven the claim to be true reguardless of xs, ys, and f.