haskell - 我如何证明 elem z (xs++ ys) == elem z xs ||元素z ys？

Question

我有以下内容:

elem :: Eq a => a -> [a] -> Bool
elem _ [] = False
elem x (y:ys) = x == y || elem x ys

我如何证明对于所有 x 的 y 和 z ...

elem z (xs ++ ys) == elem z xs || elem z ys

我试图让左边等同于右边，但是我的尝试都没有结果。

L.S elem z (x:xs ++ y:ys) = z==x || z==y || elem xs || elem ys

R.S elem z (x:xs) || elem z (y:ys) = z==x || z==y || elem xs || elem ys

有人可以帮帮我吗？

Answer 1

这是一个提示。

++ 运算符是通过对第一个 参数进行归纳来定义的:

[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

你想证明

elem z (xs ++ ys) == elem z xs || elem z ys

这是z、xs 和ys 的属性。我们称它为 p(z,xs,ys)。此外，++的第一个参数是xs，因此建议对xs进行归纳。

我们需要证明:

1. 基本情况:p(z,[],ys)。
2. 归纳案例:p(z,x:xs,ys)假设归纳假设p(z,xs,ys)

在某些时候，您还需要利用 elem 的定义。