How can I prove that elem z (xs ++ ys) == elem z xs || elem z ys?

Question

I have the following:

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

How can I prove that for all x's y's and z's...

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

I attempted to make the left side equivalent to the right side, however none of my attempts have been fruitful.

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

Can someone help me out?

Answer 1

Equational reasoning is fun! You'll get the knack of it pretty quickly, if you do a few proofs yourself. I warmly recommend ch. 13 of Graham Hutton's Programming in Haskell for a concise introduction.

Anyway, you can prove that, for all equatable and finite (see Tom Ellis's answer) xs, ys and z,

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

by induction on list xs. For that, you need to use the definitions of ++, ||, and elem, and use the fact that || is associative:

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

False || b = b
True  || _ = True

elem _ [] = False
elem x (y:ys) = x == y || elem x ys

Base case

Let ys be a value of type Eq a => [a], and z a value of type Eq a => a; then we have

elem z ([] ++ ys)
=     {applying ++}
elem z ys
=     {unapplying ||}
False || elem z ys
=     {unapplying elem}
elem z [] || elem z ys

Inductive case

Let xs, ys be values of type Eq a => [a], and x, z values of type Eq a => a. Assume (induction hypothesis) that

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

Then we have

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)