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 }