我如何证明使用列表归纳？

Question

我必须通过xs列表归纳显示:所有列表xs和ys的reverse(xs ++ ys)=(reverse ys)++(reverse xs).

Answer 1

首先,

reverse (xs ++ ys) ? reverse ys ++ reverse xs

如果xs是无限或部分⁽¹⁾列表并且ys是有限非空列表,则不是真的.因为在这种情况下xs ++ ys也是无限的或部分的,在这两种情况下,

reverse (xs ++ ys) ? ?

但

reverse ys ++ reverse xs ? reverse ys ++ ?

并且reverse ys是一个有限的非空列表,因此reverse ys ++ ?不是?一个非空初始部分的部分列表.

因此,让我们假设xs是一个有限的列表,即xs ? []或xs ? x : zs在那里zs是一种有限的名单.

对于基本情况,我们有

reverse ([] ++ ys)
? reverse ys         -- by 1.

和

reverse ys ++ reverse []
? reverse ys ++ []   -- by 3.

所以它仍然表明了这一点

zs ++ [] ? zs

所有列表zs(这是真实的,即使ys ? ?或者ys是无限或部分),完成基本情况的证明.

你通过归纳证明了zs(很简单).

然后你去感应步骤.前两个步骤是:

reverse ((x:xs) ++ ys)
? reverse (x:(xs ++ ys))            -- by 2.
? reverse (xs ++ ys) ++ [x]         -- by 4.

那你需要

⁽¹⁾部分列表是表单的列表

zs ++ ?

其中zs是一个有限列表,即它是通过"限制"有限数量(可能是0)的元素来获得?而不是[].