我怎样才能证明elem z(xs ++ ys)== elem z xs || 你好吗？

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在某些时候利用定义.