我有以下内容：
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
有人可以帮我吗？
这里有一个提示。
++运算符由对第一个参数的归纳定义：
[] ++ 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。
我们需要证明：
p(z,[],ys).p(z,x:xs,ys)假设归纳假设p(z,xs,ys)您还需要elem在某些时候利用 的定义。
等式推理很有趣！如果你自己做一些证明，你会很快掌握它的诀窍。我热烈推荐ch。Graham Hutton 的Programming in Haskell中的第 13 节进行了简要介绍。
无论如何，您可以证明，对于所有等式和有限的（请参阅汤姆·埃利斯的回答） xs，ys并且z，
elem z (xs ++ ys) == elem z xs || elem z ys
通过归纳列表xs。为此，您需要使用 、 和 的定义，++并使用关联的事实：||elem||
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
False || b = b
True || _ = True
elem _ [] = False
elem x (y:ys) = x == y || elem x ys
让ys是 一个 类型的 值Eq a => [a]和z一个 类型 的 值Eq a => a; 那么我们有
elem z ([] ++ ys)
= {applying ++}
elem z ys
= {unapplying ||}
False || elem z ys
= {unapplying elem}
elem z [] || elem z ys
让xs,ys是类型的值Eq a => [a]，和x,z类型的值Eq a => a。假设（归纳假设）
elem z (xs ++ ys) == elem z xs || elem z ys
然后我们有
elem z ((x:xs) ++ ys)
= {applying ++)
elem z (x : (xs ++ ys))
= {applying elem}
z == x || elem (xs ++ ys)
= {induction hypothesis}
z == x || (elem z xs || elem z ys)
= {associativity of ||}
(z == x || elem z xs) || elem z ys
= {unapplying elem}
elem z (x:xs) || elem z ys
(QED)
为了扩展公认的答案，这个等式在xs无穷大时也是正确的。如果elem z xs = True，那么elem z (xs ++ ys) = True = elem z xs || elem z ys。否则，elem z (xs ++ ys) = ⊥ = elem z xs || elem z ys可以在 ghci 中轻松验证。
Haskell 中的列表不满足归纳原则，因为 Haskell 是一种惰性语言，列表可能是无限的。相反，我认为您应该只以相同的形式编写两个表达式以表明它们是等价的。所需的形式是
f [] = z
f (x:xs) = g x (f xs)
要使用这种方法来证明所需的结果，请采取
f xs = elem z (xs ++ ys)
f' xs = elem z xs || elem z ys
请注意，通过模式匹配xs和使用 and 的定义，(++)这些elem等价于
f [] = elem z ys
f (x:xs) = x == z || elem z (xs ++ ys)
f' [] = elem z ys
f' (x:xs) = x == z || elem z xs || elem z ys
我们可以将递归调用重写为
f [] = elem z ys
f (x:xs) = x == z || f xs
f' [] = elem z ys
f' (x:xs) = x == z || f' xs
如果我们定义g x rest = x == z || rest那么
f [] = elem z ys
f (x:xs) = g x (f xs)
f' [] = elem z ys
f' (x:xs) = g x (f' xs)
然后注意 和 的表达式f是f'相等的。
我之前的回答不正确：