[Haskell-beginners] structural induction, two lists, simultaneous

[Pascal Knodel]

Hi list,


Proposition:

map f (ys ++ zs)  =  map f ys ++ map f zs

(Haskell, the craft of functional programming, exercise 11.31)


Almost every time I'm asked to do (structural) induction over multiple
'things', in this example lists, I don't know how to do it.
(I encountered similar difficulties when I worked through chapter 9, see
https://github.com/pascal-knodel/haskell-craft/tree/master/Chapter%209 ,
ex. 9.5 , 
https://github.com/pascal-knodel/haskell-craft/blob/master/Chapter%209/E%279%27%275.hs).
I think my proof in this case isn't formally correct. It feels like it 
isn't.

I would like to do the example with your help, so that I feel a
little bit safer.

Let's start with the base case. If I have two lists, do I select
one, say  ys := [] . Only one or one after another? Or both 'parallel'?
I could state  ys ++ zs := []  too, does it help?

I could imagine that the proposition could be expanded to something like

     map f (l1 ++ l2 ++ ... ++ lN) = map f ys ++ map f zs
  =  map f l1 ++ map f l2 ++ ... ++ map f lN

And I could imagine that it is possible to do induction over more than 
two lists too.

What is the reason why we can do it over two 'objects' at the same time?
How do I start? Can you explain this to me?


Attempt:

-- ---------------
-- 1. Proposition:
-- ---------------
--
--   map f (ys ++ zs)  =  map f ys ++ map f zs
--
--
-- Proof By Structural Induction:
-- ------------------------------
--
--
--   1. Induction Beginning (1. I.B.):
--   ---------------------------------
--
--
--     (Base case 1.)  :<=>  ys := []
-- 
--       =>  (left)  :=  map f (ys ++ zs)
--                                          | (Base case 1.)
--                    =  map f ([] ++ zs)
--                                          | ++
--                    =  map f zs
--
--
--          (right)  :=  map f ys ++ map f zs
--                                               | (Base case 1.)
--                    =  map f [] ++ map f zs
--                                               | map
--                    =  map f zs
--
--
--       => (left)  =  (right)
--
--       ✔
--
--
--  1. Induction Hypothesis (1. I.H.):
--  ----------------------------------
--
--    For an arbitrary, but fixed list "ys", the statement ...
--
--      map f (ys ++ zs)  =  map f ys ++ map f zs
--
--    ... holds.
--
--
--  1. Induction Step (1. I.S.):
--  ----------------------------
--
--
--     (left)  :=  map f ( (y : ys) ++ zs )
--                                                      | ++
--              =  map f (  y : ( ys ++ zs )  )
--                                                      | map
--              =  f y : map f ( ys ++ zs )
--                                                      | (1. I.H.)
--              =  f y : map f ys ++ map f zs
--                                                      | map
--              =  map f (y : ys) ++ map f zs
--
--
--    (right)  :=  map f (y : ys) ++ map f zs
--
--
--    =>  (left)  =  (right)
--
--
--    ?■?  (1. Proof)


But in this 'proof attempt' only "ys" was considered (1. I.H.).
What do I miss?

Pascal