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

Question

Étant donné n >= 0 and n < min (length xs) (length ys) montrer que (zip xs ys)!!n = (xs!!n, ys!!n) avec induction structurelle sur xs.

Est-il même possible de le faire de manière propre? Je ne peux pas trouver tous les endroits où je peux utiliser le Induction Hypothesis.

Answer 1

D'abord, je vais vous donner des définitions de zip et !!:

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) 

Laissez-xs, ys et n arbitraires. Maintenant, supposons que n >=0 et n < min (length xs) (length ys). Nous procédons par induction au xs.

• Cas xs = []. Maintenant, nous faisons l'analyse de cas sur ys. Dans les deux cas, nous avons qu'il n'y a pas n >=0 et n < min (length xs) (length ys). Donc, ce cas est trivialement vrai.
• Cas xs = x : xs'. Nous procédons par analyse de cas sur ys.
• Cas xs = x : xs' et ys = []. Encore une fois, nous avons le théorème trivialement vrai puisqu'il n'y a pas n tel que cela n >=0 et n < min (length xs) (length ys).
• Cas xs = x : xs' et ys = y : ys'. Maintenant, nous faisons l'analyse de cas sur n.

• Cas xs = x : xs', ys = y : ys' et n = 0. Nous avons que

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

• cas xs = x : xs', ys = y : ys' et 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

Espérons que cela aide.