Structural Induction - (zip xs ys)!!n = (xs!!n, ys!!n)

Question

Given n >= 0 and n < min (length xs) (length ys) show that (zip xs ys)!!n = (xs!!n, ys!!n) with structural Induction over xs.

Is it even possible to do this in a clean way? I cant find any spots where I can use the Induction Hypothesis.

Answer 1

First, I'll give definitions of zip and !!:

zip :: [a] -> [b] -> [(a,b)]
zip [] [] = []                             -- (zip-1)
zip (x:xs) (y:ys) = (x,y) : zip xs ys      -- (zip-2)
zip _ _ = []                               -- (zip-3)

(!!) :: [a] -> Int -> a
(x : _) !! 0 = x                           -- (!!-1)
(_ : xs) !! n = xs !! (n - 1)              -- (!!-2)

Let xs, ys and n arbitrary. Now, suppose that n >=0 and n < min (length xs) (length ys). We proceed by induction on xs.

• Case xs = []. Now we do case analysis on ys. In both cases, we have that there's no n >=0 and n < min (length xs) (length ys). So, this case is trivially true.
• Case xs = x : xs'. We proceed by case analysis on ys.
• Case xs = x : xs' and ys = []. Again, we have the theorem trivially true since there's no n such that that n >=0 and n < min (length xs) (length ys).
• Case xs = x : xs' and ys = y : ys'. Now we do case analysis on n.

• Case xs = x : xs', ys = y : ys' and n = 0. We have that

  zip (x : xs') (y : ys') !! 0 = {by equation (zip-2)}
  (x,y) : zip xs' ys'     !! 0 = {by equation (!!-1)}
  (x,y)                        = {by equation (!!-1) - backwards}
  ((x : xs') !! 0, (y : ys') !! 0).
  

• Case xs = x : xs', ys = y : ys' and n = n' + 1.

   zip (x : xs') (y : ys') !! (n + 1) = {by equation zip-2}
   (x,y) : zip xs' ys' !! (n + 1) = {by equation (!!-2)}
   zip xs' ys' !! n               = {by induction hypothesis}
   (xs' !! n , ys' !! n)          = {by equation (!!-2) backwards}
   ((x : xs') !! (n + 1), (y : ys') !! (n + 1))
  

  QED

Hope that this helps.