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

【问题标题】：Structural Induction - (zip xs ys)!!n = (xs!!n, ys!!n)结构归纳 - (zip xs ys)!!n = (xs!!n, ys!!n)
【发布时间】：2017-02-06 08:13:01
【问题描述】：

给定n >= 0 and n < min (length xs) (length ys) 显示 (zip xs ys)!!n = (xs!!n, ys!!n) 在 xs 上的结构归纳。

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

【问题讨论】：

我生疏了，但我认为你可以通过等式推理和扩展zip 和!! 的定义来证明zip xs ys !! 0 = (xs !! 0, ys !! 0)，然后证明如果zip xs ys !! n = (xs !! n, ys !! n) 然后zip xs ys !! n + 1 = (xs !! n + 1, ys !! n + 1)。
感谢您的回答。我忘了提到它应该是列表长度上的结构归纳。即 xs 在归纳步骤中变为 (x:xs)。

标签： haskell induction

【解决方案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

希望这会有所帮助。

【讨论】：

感谢您的回答！在您使用 IH 的最后一种情况下，这不会被认为是对 n 的归纳吗？还有你从哪里得到的函数定义？
绝不是！感应结束xs。 IH 是永久的。 forall n. n >= 0 /\ n zip xs ys !! n = (xs !! n , ys !! n)。对n 和ys 进行案例分析的需要只是为了“按摩”目标，以便使用等式推理轻松操纵它。
如果你觉得答案没问题，请标记为答案。