# HG changeset patch # User Markus Kaiser # Date 1355955655 -3600 # Node ID 498aea38199b5feead88c96a822423295f97d7fa # Parent 3fea6fff726577d8c09821e3cc0b5f6367564cff week 9 tutorial diff -r 3fea6fff7265 -r 498aea38199b exercises/src/Exercise_9.hs --- a/exercises/src/Exercise_9.hs Wed Dec 12 20:32:09 2012 +0100 +++ b/exercises/src/Exercise_9.hs Wed Dec 19 23:20:55 2012 +0100 @@ -55,18 +55,26 @@ {- Aufgabe G9.1 -} {- -Lemma mirror (mirror t) = t +Lemma(t): mirror (mirror t) = t Proof by structural induction on t -Base case: -To show: +Base case: Lemma(Empty) +To show: mirror (mirror Empty) = Empty +mirror (mirror Empty) += mirror Empty mirror_Empty += Empty mirror_Empty -Induction step: -IH1: -IH2: -To show: +Induction step: Lemma(l), Lemma(r) => Lemma((Node x l r)) +IH1: mirror (mirror l) = l +IH2: mirror (mirror r) = r +To show: mirror (mirror (Node x l r)) = Node x l r +mirror (mirror (Node x l r)) += mirror (Node x (mirror r) (mirror l)) mirror_Node += Node x (mirror (mirror l)) (mirror (mirror r)) mirror_Node += Node x l (mirror (mirror r)) IH1 += Node x l r IH2 -QED? +QED! -} @@ -75,7 +83,10 @@ {- Aufgabe G9.2 -} balanced :: Tree a -> Bool -balanced t = undefined +balanced t = dist max t - dist min t <= 1 + where + dist f (Node _ l r) = 1 + f (dist f l) (dist f r) + dist _ Empty = 0 @@ -83,13 +94,23 @@ {- Aufgabe G9.3 -} type Coords = (Int, Int) -data Shape = Missing +data Shape = + Line Coords Coords + | Circle Coords Int + move :: Coords -> Shape -> Shape -move (x,y) _ = undefined +move (x,y) (Line (a,b) (c,d)) = Line (a+x, b+y) (c+x, d+y) +move (x,y) (Circle (a,b) r) = Circle (a+x, b+y) r + polygon :: [Shape] -> Bool -polygon _ = undefined +polygon ((Line from to) : ss) = polygon' from to ss + where + polygon' f t [] = f == t + polygon' f t ((Line lf lt) : ss) = t == lf && polygon' f lt ss + polygon' _ _ _ = False +polygon _ = False