Here are some answers for the exercises.

1. To prove: x `elem` (xs ++ ys) = (x `elem` xs) || (x `elem` ys), for all x,xs,ys.

Proof: by structural induction over xs.

base case: xs = [].

x `elem` (xs ++ ys)
= x `elem` ([] ++ ys)		-- xs = []
= x `elem` ys		-- defn. ++
= False || x `elem` ys		-- defn. ||
= (x `elem` []) || x `elem` ys		-- defn. elem
= (x `elem` xs) || x `elem` ys		-- xs = []

step case: xs = a:as.

1. I.H.: x `elem` (as ++ ys) = (x `elem` as) || (x `elem` ys), for all x,ys

2. Look at the following:

x `elem` (xs ++ ys)
= x `elem` ((a:as) ++ ys)		-- xs = a:as
= x `elem` (a : (as ++ ys)		-- defn. ++
= x == a || (x `elem` (as ++ ys))		-- defn. elem
= x == a || ((x `elem` as) || (x `elem` ys))		-- I.H.
= (x == a || (x `elem` as)) || (x `elem` ys)		-- || is associative
= (x `elem` (a:as)) || (x `elem` ys)		-- defn. elem
= (x `elem` xs) || (x `elem` ys)		-- xs = a:as

Which is what we had to prove.

2. To prove: length (rev xs) = length xs, for all xs.

Proof: by structural induction over xs.

base case: xs = [].

length (rev xs)
= length (rev [])		-- xs = []
= length []		-- defn. rev
= length xs		-- xs = []

step case: xs = a:as.

1. I.H.: length (rev as) = length as

2. Look at the following:

length (rev xs)
= length (rev (a:as))		-- xs = a:as
= length (rev as ++ [a])		-- defn. rev
= length (rev as) + length [a]		-- length/++ lemma
= length as + length [a]		-- I.H.
= length as + 1		-- defn. length
= 1 + length as		-- + commutative
= length (a:as)		-- defn. length
= length xs		-- xs = a:as

Which is what we had to prove.

3. To prove: x `elem` rev xs = x `elem` xs, for all x,xs.

Proof: by structural induction over xs.

base case: xs = [].

x `elem` rev xs
= x `elem` rev []		-- xs = []
= x `elem` []		-- defn. rev
= x `elem` xs		-- xs = []

step case: xs = a:as.

1. I.H.: x `elem` rev as = x `elem` as, for all x.

2. Look at the following:

x `elem` rev xs
= x `elem` rev (a:as)		-- xs = a:as
= x `elem` (rev as ++ [a])		-- defn. rev
= (x `elem` rev as) || (x `elem` [a])		-- exercise 1.
= (x `elem` as) || (x `elem` [a])		-- I.H.
= (x `elem` [a]) || (x `elem` as)		-- || commutative
= x == a || (x `elem` as)		-- defn. elem
= x `elem` (a:as)		-- defn. elem
= x `elem` xs		-- xs = a:as

Which is what we had to prove.

4. To prove: x `elem` xs ==> length xs > 0, for all x,xs

Proof: by case split on xs.

case 1: xs = [].

x `elem` xs ==> length xs > 0
= x `elem` [] ==> length [] > 0		-- xs = []
= False ==> length [] > 0		-- defn. elem
= True		-- basic logic

case 2: xs = a:as.

x `elem` xs ==> length xs > 0
= x `elem` (a:as) ==> length (a:as) > 0		-- xs = a:as
= x `elem` (a:as) ==> (1 + length as) > 0		-- defn. length
= x `elem` (a:as) ==> True		-- basic arithmetic, length as >= 0
= True		-- basic logic

Which is what we had to prove.

5. To prove: take (length xs) xs = xs, for all xs.

Proof: by structural induction over xs.

base case: xs = [].

take (length xs) xs
= take (length []) []		-- xs = []
= take 0 []		-- defn. length
= []		-- defn. take
= xs		-- xs = []

step case: xs = a:as.

1. I.H.: take (length as) as = as.

2. Look at the following:

take (length xs) xs
= take (length (a:as)) (a:as)		-- xs = a:as
= take (1 + length as) (a:as)		-- defn. length
= a : take (1 + length as - 1) as		-- defn. take, length as >= 0
= a : take (length as) as		-- basic arithmetic
= a : as		-- I.H.
= xs		-- xs = a:as

Which is what we had to prove.

6. To prove: even x = not (odd x), for all x.

Proof: by structural induction over x.

base case: x = Zero.

even x
= even Zero		-- x = Zero
= True		-- defn. even
= not False		-- defn. not
= not (odd Zero)		-- defn. odd
= not (odd x)		-- x = Zero

step case: x = Succ a.

1. I.H.: even a = not (odd a).

2. Look at the following:

even x
= even (Succ a)		-- x = Succ a
= not (even a)		-- defn. even
= not (not (odd a))		-- I.H.
= odd a		-- basic logic
= not (odd (Succ a))		-- defn. odd
= not (odd x)		-- x = Succ a

Which is what we had to prove.

7. To prove: plus x Zero = x, for all x.

Proof: by structural induction over x.

base case: x = Zero.

plus x Zero
= plus Zero Zero		-- x = Zero
= Zero		-- defn. plus
= x		-- x = Zero

step case: x = Succ a.

1. I.H.: plus a Zero = a.

2. Look at the following:

plus x Zero
= plus (Succ a) Zero		-- x = Succ a
= Succ (plus a Zero)		-- defn. plus
= Succ a		-- I.H.
= x		-- x = Succ a

Which is what we had to prove.

8. To prove: even (plus x x), for all x.

Proof: by structural induction over x.

base case: x = Zero.

even (plus x x)
= even (plus Zero Zero)		-- x = Zero
= even Zero		-- defn. plus
= True		-- defn. even

step case: x = Succ a.

1. I.H.: even (plus a a).

2. Look at the following:

even (plus x x)
= even (plus (Succ a) (Succ a))		-- x = Succ a
= even (Succ (plus a (Succ a)))		-- defn. plus
= not (even (plus a (Succ a)))		-- defn. even
= not (even (Succ (plus a a)))		-- helper lemma (see below)
= not (not (even (plus a a)))		-- defn. even
= even (plus a a)		-- basic logic
= True		-- I.H.

Which is what we had to prove.

We also need to prove the helper lemma:

To prove: plus x (Succ y) = Succ (plus x y), for all x,y.

Proof: by structural induction over x.

base case: x = Zero.

plus x (Succ y)
= plus Zero (Succ y)		-- x = Zero
= Succ y		-- defn. plus
= Succ (plus Zero y)		-- defn. plus
= Succ (plus x y)		-- x = Zero

step case: x = Succ a.

1. I.H.: plus a (Succ y) = Succ (plus a y), for all y.

2. Look at the following:

plus x (Succ y)
= plus (Succ a) (Succ y)		-- x = Succ a
= Succ (plus a (Succ y))		-- defn. plus
= Succ (Succ (plus a y))		-- I.H.
= Succ (plus (Succ a) y)		-- defn. plus
= Succ (plus x y)		-- x = Succ a

Which is what we had to prove.

9. To prove: size p = length (flatten p), for all p.

Proof: by structural induction over p.

base case: p = Empty.

size p
= size Empty		-- p = Empty
= 0		-- defn. size
= length []		-- defn. length
= length (flatten Empty)		-- defn. flatten
= length (flatten p)		-- p = Empty

step case: p = Node a v w.

1. I.H.:

size v = length (flatten v), and

size w = length (flatten w)

2. Look at the following:

size p
= size (Node a v w)		-- p = Node a v w
= 1 + size v + size w		-- defn. size
= 1 + length (flatten v) + length (flatten w)		-- I.H. * 2
= length (flatten v ++ [a] ++ flatten w)		-- length/++ lemma * 2
= length (flatten (Node a v w))		-- defn. flatten
= length (flatten p)		-- p = Node a v w

Which is what we had to prove.

10. To prove: flatten (swap p) = rev (flatten p), for all p.

Proof: by structural induction over p.

base case: p = Empty.

flatten (swap p)
= flatten (swap Empty)		-- p = Empty
= flatten Empty		-- defn. swap
= []		-- defn. flatten
= rev []		-- defn. rev
= rev (flatten Empty)		-- defn. flatten
= rev (flatten p)		-- p = Empty

step case: p = Node a v w.

1. I.H.:

flatten (swap v) = rev (flatten v), and

flatten (swap w) = rev (flatten w)

2. Look at the following:

flatten (swap p)
= flatten (swap (Node a v w))		-- p = Node a v w
= flatten (Node a (swap w) (swap v))		-- defn. swap
= flatten (swap w) ++ [a] ++ flatten (swap v)		-- defn. flatten
= rev (flatten w) ++ [a] ++ rev (flatten v)		-- I.H. * 2
= rev (flatten w) ++ rev [a] ++ rev (flatten v)		-- defn. rev
= rev ([a] ++ flatten w) ++ rev (flatten v)		-- rev/++ lemma
= rev (flatten v ++ [a] ++ flatten w)		-- rev/++ lemma
= rev (flatten (Node a v w))		-- defn. flatten
= rev (flatten p)		-- p = Node a v w

Which is what we had to prove.

11. To prove: flatten (spine xs) = xs, for all xs.

Proof: by structural induction over xs.

base case: xs = [].

flatten (spine xs)
= flatten (spine [])		-- xs = []
= flatten Empty		-- defn. spine
= []		-- defn. flatten
= xs		-- xs = []

step case: xs = a:as.

1. I.H.: flatten (spine as) = as.

2. Look at the following:

flatten (spine xs)
= flatten (spine (a:as))		-- xs = a:as
= flatten (Node a Empty (spine as))		-- defn. spine
= flatten Empty ++ [a] ++ flatten (spine as)		-- defn. flatten
= [] ++ [a] ++ flatten (spine as)		-- defn. flatten
= a : flatten (spine as)		-- defn. ++
= a : as		-- I.H.
= xs		-- xs = a:as

Which is what we had to prove.