我如何证明 elem z (xs ++ ys) == elem z xs || elem 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

这里有一个提示。

++ 运算符是通过对 first 参数的归纳定义的：

[]     ++ 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 的定义。

Answer 2

等式推理很有趣！如果你自己做一些证明，你会很快掌握它的诀窍。我热烈推荐ch。 Graham Hutton 的 Programming in Haskell 中的第 13 节进行了简要介绍。

无论如何，你可以证明，对于所有等式和有限（参见Tom Ellis's answer）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)

Answer 3

为了扩展可接受的答案，当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 中轻松验证。

Answer 4

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 上的模式匹配并使用(++) 和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' 的表达式是相等的。

我之前的回答不正确：

这不是真的。考虑 xs = 重复 0 ys = [1] z = 1 然后 elem z ys = elem 1 [1] = 真 所以 元素 z xs || elem z ys = 真 但 elem z (xs ++ ys) = elem 1 (重复 0 ++ [1]) = False 因为在 `repeat 0` 中搜索 `1` 永远不会终止。 这是一个典型的例子，说明为什么惰性语言的方程理论不如严格语言的丰富。 正如其他答案所建议的那样，您可以通过结构归纳证明*有限*`xs` 的定理。但这有点乞求问题。什么是*有限*列表？