结构归纳法 - (zip xs ys)!!n = (xs!!n, ys!!n)

Question

鉴于n >= 0 and n < min (length xs) (length ys) 证明 (zip xs ys)!!n = (xs!!n, ys!!n) 在 xs 上具有结构归纳法。

是否有可能以干净的方式做到这一点？我找不到可以使用 Induction Hypothesis.

的地方

Answer 1

首先，我将给出zip和!!的定义：

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)

让 xs、ys 和 n 任意。现在，假设 n >=0 和 n < min (length xs) (length ys)。我们在 xs.

上进行归纳

个案xs = []。现在我们对ys进行案例分析。在这两种情况下，我们都没有 n >=0 和 n < min (length xs) (length ys)。所以，这个案例是平凡的。
个案xs = x : xs'。我们对 ys 进行案例分析。
案例 xs = x : xs' 和 ys = []。同样，我们有这个定理平凡为真，因为没有 n 使得 n >=0 和 n < min (length xs) (length ys).
案例 xs = x : xs' 和 ys = y : ys'。下面我们对n.

案例 xs = x : xs'、ys = y : ys' 和 n = 0。我们有那个

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

案例 xs = x : xs'、ys = y : ys' 和 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

希望对您有所帮助。

结构归纳法 - (zip xs ys)!!n = (xs!!n, ys!!n)

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

haskell

induction