Given:
data Tree a = Tip | Node a (Tree a) (Tree a)
mirror Tip = Tip
mirror (Node a l r) = Node a (mirror r) (mirror l)
flatten Tip = []
flatten (Node a l r) = flatten l ++ [a] ++ flatten r
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
prove that:
flatten . mirror = reverse . flatten
This is: for all t :: Tree a,
flatten (mirror t) = reverse (flatten t) { by function equality }
Proof by induction on structure of t :: Tree a
case t = Tip:
flatten (mirror Tip) = reverse (flatten Tip) { goal with t := Tip }
flatten Tip = ... { LHS: defn mirror }
[] = ... { LHS: defn flatten }
[] = reverse (flatten Tip) { reiterate RHS }
[] = reverse [] { RHS: defn flatten }
[] = [] { RHS: defn reverse }
QED { reflexivity of equality }
case t = Node a l r:
flatten (mirror (Node a l r)) = reverse (flatten (Node a l r))
{ goal with t := Node a l r }
flatten (Node a (mirror r) (mirror l)) = ...
{ LHS: defn mirror }
flatten (mirror r) ++ [a] ++ flatten (mirror l) = ...
{ LHS: defn flatten }
flatten (mirror r) ++ ([a] ++ flatten (mirror l)) = ...
{ clarify: ++ associates right }
... = reverse (flatten (Node a l r)) { reiterate RHS }
... = reverse (flatten l ++ [a] ++ flatten r) { RHS: defn flatten }
... = reverse (flatten l ++ ([a] ++ flatten r)) { clarify: ++ associates right }
... = reverse ([a] ++ flatten r) ++ reverse (flatten l)
{ lemma 1: see below }
... = (reverse (flatten r) ++ reverse [a]) ++ reverse (flatten l)
{ lemma 1: see below }
... = reverse (flatten r) ++ (reverse [a] ++ reverse (flatten l))
{ lemma 2: see below }
... = reverse (flatten r) ++ ([a] ++ reverse (flatten l))
{ lemma 3: see below }
flatten (mirror r) ++ ([a] ++ flatten (mirror l)) =
reverse (flatten r) ++ ([a] ++ reverse (flatten l))
{ reiterate LHS }
reverse (flatten r) ++ ([a] ++ flatten (mirror l)) =
reverse (flatten r) ++ ([a] ++ reverse (flatten l))
{ subn, ind. hyp. on r }
reverse (flatten r) ++ ([a] ++ reverse (flatten l)) =
reverse (flatten r) ++ ([a] ++ reverse (flatten l))
{ subn, ind. hyp. on l }
QED { reflexivity of equality }
Lemma 1:
for all xs, ys :: [a],
reverse (xs ++ ys) = reverse ys ++ reverse xs
Proof by induction on structure of xs :: [a]
case xs = []:
reverse ([] ++ ys) = reverse ys ++ reverse [] { goal with xs := [] }
reverse ys = reverse ys ++ reverse [] { defn ++ }
reverse ys = reverse ys ++ [] { defn reverse }
reverse ys = reverse ys { lemma 1.5, see below }
QED { reflexivity of equality }
case xs = (a:as):
reverse ((a:as) ++ ys) = reverse ys ++ reverse (a:as)
{ goal with xs := a : as }
reverse (a : (as ++ ys)) = ... { LHS, defn of ++ }
reverse (as ++ ys) ++ [a] = ... { LHS, defn of reverse }
... = reverse ys ++ reverse (a:as) { reiterate RHS }
... = reverse ys ++ (reverse as ++ [a]) { RHS, defn reverse }
reverse (as ++ ys) ++ [a] = (reverse ys ++ reverse as) ++ [a]
{ reiterate LHS }
reverse (as ++ ys) = (reverse ys ++ reverse as) { focus from context }
reverse (as ++ ys) = reverse (as ++ ys) { ind. hyp. on as, ys }
QED { reflexivity of equality }
Lemma 1.5:
for all xs :: [a],
xs ++ [] = xs
Proof by induction on structure of xs :: [a]
case xs = []:
[] ++ [] = [] { goal with xs := [] }
[] = [] { defn ++ }
QED { reflexivity of equality }
case xs = (y:ys):
(y : ys) ++ [] = y : ys { goal with xs := y : ys }
y : (ys ++ []) = y : ys { defn ++ }
y : ys = y : ys { ind hyp on ys }
QED { reflexivity of equality }
Lemma 2:
for all xs, ys, zs :: [a],
(xs ++ ys) ++ zs = xs ++ (ys ++ zs)
Proof by induction on structure of xs :: [a]
case xs = []:
([] ++ ys) ++ zs = [] ++ (ys ++ zs) { goal with xs := [] }
ys ++ zs = [] ++ (ys ++ zs) { defn ++, LHS }
ys ++ zs = ys ++ zs { defn ++, RHS }
QED { reflexivity of equality }
case xs = (a:as):
((a:as) ++ ys) ++ zs = (a:as) ++ (ys ++ zs) { goal with xs := a : as }
(a : (as ++ ys)) ++ zs = (a:as) ++ (ys ++ zs) { defn ++, LHS }
(a : (as ++ ys)) ++ zs = a : (as ++ (ys ++ zs)) { defn ++, RHS }
a : ((as ++ ys) ++ zs) = a : (as ++ (ys ++ zs)) { lemma 2.5, LHS, see below }
a : (as ++ (ys ++ zs)) = a : (as ++ (ys ++ zs)) { lemma 2.5, ind. hyp. on as }
QED { reflexivity of equality }
Lemma 2.5:
for all a :: a, xs, ys :: [a],
(a : xs) ++ ys = a : (xs ++ ys)
Proof by induction on structure of xs :: [a]
case xs = []:
(a : []) ++ ys = a : ([] ++ ys) { goal with xs := [] }
a : ([] ++ ys) = a : ([] ++ ys) { defn ++, LHS }
QED { reflexivity of equality }
case xs = (a:as):
(a : as) ++ ys = a : (xs ++ ys) { goal with xs := a : as }
a : (as ++ ys) = a : (xs ++ ys) { LHS, defn ++ }
QED { reflexivity of equality }
Lemma 3:
for all a :: a,
reverse [a] = [a] { original goal }
reverse (a : []) = [a] { list notation, twice }
reverse [] ++ [a] = [a] { defn reverse }
[] ++ [a] = [a] { defn reverse }
[a] = [a] { defn ++ }
QED { reflexivity of equality }