Exercises Week 6 - Structural Induction - Answers
(1.) To prove: x `elem` (xs ++ ys) = (x `elem` xs) || (x `elem` ys), for all x,xs,ys.
Proof: by structural induction.
Let P(xs) = "∀x,ys . x `elem` (xs ++ ys) = (x `elem` xs) || (x `elem` ys)".
base case: P([]) = "∀ x, ys . x `elem` ([] ++ ys) = (x `elem` []) || (x `elem` ys)".
x `elem` ([] ++ ys) | ||
= x `elem` ys | -- defn. ++ | |
= False || x `elem` ys | -- defn. || | |
= (x `elem` []) || x `elem` ys | -- defn. elem |
step case: P(as) => P(a:as).
assume: P(as) = "∀ x, ys . x `elem` (as ++ ys) = (x `elem` as) || (x `elem` ys)" (I.H.)
show: P(a:as) = "∀ x, ys . x `elem` ((a:as) ++ ys) = (x `elem` (a:as)) || (x `elem` ys)"
x `elem` ((a:as) ++ ys) | ||
= 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 |
Which is what we had to prove.
(2.) To prove: length (rev xs) = length xs, for all xs.
Proof: by structural induction.
Let P(xs) = "length (rev xs) = length xs".
base case: P([]) = "length (rev []) = length []".
length (rev []) | ||
= length [] | -- defn. rev |
step case: P(as) => P(a:as).
assume: P(as) = "length (rev as) = length as" (I.H.)
show: P(a:as) = "length (rev (a:as)) = length (a:as)"
length (rev (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 |
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.
Let P(xs) = "∀x . x `elem` rev xs = x `elem` xs"
base case: P([]) = "∀x . x `elem` rev [] = x `elem` []".
x `elem` rev [] | ||
= x `elem` [] | -- defn. rev |
step case: P(as) => P(a:as).
assume: P(as) = "∀x . x `elem` rev as = x `elem` as" (I.H.)
show: P(a:as) = "∀x . x `elem` rev (a:as) = x `elem` (a:as)"
x `elem` rev (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 |
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.
Let P(xs) = "take (length xs) xs = xs".
base case: P([]) = "take (length []) [] = []".
take (length []) [] | ||
= take 0 [] | -- defn. length | |
= [] | -- defn. take |
step case: P(as) => P(a:as).
assume: P(as) = "take (length as) as = as" (I.H.)
show: P(a:as) = "take (length (a:as)) (a:as) = a:as"
take (length (a:as)) (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. |
Which is what we had to prove.
(6.) To prove: even x = not (odd x), for all x.
Proof: by structural induction.
Let P(x) = "even x = not (odd x)".
base case: P(Zero) = "even Zero = not (odd Zero)".
even Zero | ||
= True | -- defn. even | |
= not False | -- defn. not | |
= not (odd Zero) | -- defn. odd |
step case: P(a) => P(Succ a).
assume: P(a) = "even a = not (odd a)" (I.H.)
show: P(Succ a) = "even (Succ a) = not (odd (Succ a))"
even (Succ a) | ||
= not (even a) | -- defn. even | |
= not (not (odd a)) | -- I.H. | |
= odd a | -- basic logic (not (not x) = x) | |
= not (odd (Succ a)) | -- defn. odd |
Which is what we had to prove.
(7.) To prove: plus x Zero = x, for all x.
Proof: by structural induction.
Let P(x) = "plus x Zero = x".
base case: P(Zero) = "plus Zero Zero = Zero".
plus Zero Zero | ||
= Zero | -- defn. plus |
step case: P(a) => P(Succ a).
assume: P(a) = "plus a Zero = a" (I.H.)
show: P(Succ a) = "plus (Succ a) Zero = (Succ a)"
plus (Succ a) Zero | ||
= Succ (plus a Zero) | -- defn. plus | |
= Succ a | -- I.H. |
Which is what we had to prove.
(8.) To prove: even (plus x x), for all x.
Proof: by structural induction.
Let P(x) = "even (plus x x)".
base case: P(Zero) = "even (plus Zero Zero)".
even (plus Zero Zero) | ||
= even Zero | -- defn. plus | |
= True | -- defn. even |
step case: P(a) => P(Succ a).
assume: P(a) = "even (plus a a)" (I.H.)
show: P(Succ a) = "even (plus (Succ a) (Succ a))"
even (plus (Succ a) (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 (not (not x) = x) | |
= 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.
Let P(x) = "∀y. plus x (Succ y) = Succ (plus x y)":
base case: P(Zero) = "∀y. plus Zero (Succ y) = Succ (plus Zero y)".
plus Zero (Succ y) | ||
= Succ y | -- defn. plus | |
= Succ (plus Zero y) | -- defn. plus |
step case: P(a) => P(a:as).
assume: P(a) = "∀y. plus a (Succ y) = Succ (plus a y)" (I.H.)
show: P(Succ a) = "∀y. plus (Succ a) (Succ y) = Succ (plus (Succ a) y)"
plus (Succ a) (Succ y) | ||
= Succ (plus a (Succ y)) | -- defn. plus | |
= Succ (Succ (plus a y)) | -- I.H. | |
= Succ (plus (Succ a) y) | -- defn. plus |
Which is what we had to prove.
(9.) To prove: size p = length (flatten p), for all p.
Proof: by structural induction.
Let P(p) = "size p = length (flatten p)".
base case: P(Empty) = "size Empty = length (flatten Empty)".
size Empty | ||
= 0 | -- defn. size | |
= length [] | -- defn. length | |
= length (flatten Empty) | -- defn. flatten |
step case: ( P(v) /\ P(w) ) => P(Node a v w).
assume: P(v) = "size v = length (flatten v)"
and P(w) = "size w = length (flatten w)" (I.H.)
show: P(Node a v w) = "size (Node a v w) = length (flatten (Node a v w))"
size (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 |
Which is what we had to prove.
(10.) To prove: flatten (swap p) = rev (flatten p), for all p.
Proof: by structural induction.
Let P(p) = "flatten (swap p) = rev (flatten p)".
base case: P(Empty) = "flatten (swap Empty) = rev (flatten Empty)".
flatten (swap Empty) | ||
= flatten Empty | -- defn. swap | |
= [] | -- defn. flatten | |
= rev [] | -- defn. rev | |
= rev (flatten Empty) | -- defn. flatten |
step case: ( P(v) /\ P(w) ) => P(Node a v w).
assume: P(v) = "flatten (swap v) = rev (flatten v)"
and P(w) = "flatten (swap w) = rev (flatten w)" (I.H.)
show: P(Node a v w) = "flatten (swap (Node a v w)) = rev (flatten (Node a v w))"
flatten (swap (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 |
Which is what we had to prove.