# HG changeset patch # User Markus Kaiser # Date 1357757147 -3600 # Node ID ce9610f08925735b6500ac3ebe8e6acf561a1b62 # Parent 34fea195e2385f0825b16e38daa331b295ebbf1c# Parent ea3fba2381bca5d8cc1addda90064150d6a4e641 Merge diff -r 34fea195e238 -r ce9610f08925 exercises/src/Exercise_10.hs --- a/exercises/src/Exercise_10.hs Fri Dec 21 01:44:45 2012 +0100 +++ b/exercises/src/Exercise_10.hs Wed Jan 09 19:45:47 2013 +0100 @@ -10,72 +10,128 @@ {- Aufgabe G10.1 -} {- - -Abstraktionsfunktion alpha: - - \alpha [] = {} -- alpha_empty - \alpha (x:xs) = {x} \union \alpha xs -- alpha_cons +\alpha ist wie in den Folien definiert: +alpha [] = {} +alpha (y:ys) = {y} union (alpha ys) Simulationseigenschaften: -1. \alpha empty = {} -- sim_empty -2. \alpha (insert x xs) = {x} \union \alpha xs -- sim_insert -3. isin x xs = x \in \alpha xs -- sim_isin -4. size xs = |\alpha xs| -- sim_size +R_empty: \alpha empty = {} + : a empty = {} +empty = [] -Implementierung 1 - Listen mit Duplikaten: +a empty +== a [] -- by def of empty +== {} -- by def of alpha - empty = [] -- imp_empty - insert x xs = x : xs -- imp_insert - isin x xs = elem x xs -- imp_isin - size xs = length (nub xs) -- imp_size - elem _ [] = False -- elem_empty - elem x (y:ys) = x == y || elem x ys -- elem_cons +R_insert: \alpha (insert x xs) = {x} \union \alpha xs + : a (insert x xs) = {x} union a xs +insert x xs = (x : xs) + +a (insert x xs) +== a (x : xs) -- by def of insert +== {x} union (a xs) -- by def of alpha - nub [] = [] -- nub_empty - nub (x:xs) | x `elem` xs = nub xs -- nub_cons_elem - | otherwise = x : nub xs -- nub_cons_notelem +R_isin: isin x xs = x \in \alpha xs + : isin x xs = x \in a xs +isin x xs = elem x xs -Korrektheitsbeweise: +isin x xs +== elem x xs -- by implementation +== x \in (a xs) -- by L_elem -1. \alpha empty - = -2. \alpha (insert x xs) - = -3. isin x xs - = -4. size xs - = +R_size: size xs = |\alpha xs| + : size xs = | a xs| +size xs = length (nub xs) + +size xs +== length (nub xs) -- by implementation +== |a xs| -- by L_length + Hilfslemmata: - elem x xs = x \in \alpha xs -- lemma_elem +Funktionen: + +elem x [] = False -- elem_Empty +elem x (y:ys) = x == y || elem x ys -- elem_Cons + +nub [] = [] -- nub_Empty +nub (y:ys) = -- nub_Cons + if y `elem` ys then nub ys + else {- not elem -} y : (nub ys) - Proof by structural induction on xs +--- + +L_elem(xs): elem x xs = x \in a xs +Proof by structural induction on xs + +Base case: L_elem([]) +To show: elem x [] = x \in a [] +elem x [] +== False -- by elem_Empty - Base case: lemma_elem([]) - To show: +x \in a [] +== x \in {} -- by alpha +== False -- by {} - Induction step: lemma_elem(ys) => lemma_elem(y : ys) - IH: - To show: +Induction step: L_elem(ys) => L_elem(y : ys) +IH: elem x ys = x \in (a ys) +To show: elem x (y:ys) = x \in a (y:ys) +elem x (y:ys) +== x == y || elem x ys -- by elem_Cons +== x == y || x \in (a ys) -- by IH - length (nub xs) = |\alpha xs| -- lemma_length +x \in a (y:ys) +== x \in ({y} union (a ys)) -- alpha_Cons +== x \in {y} || x \in (a ys) -- by union +== x == y || x \in (a ys) -- by basic property + +qed + +--- - Proof by structural induction on xs + +L_length(xs): length (nub xs) = |a xs| +Proof by structural induction on xs - Base case: lemma_length([]) - To show: +Base case: L_length([]) +To show: length (nub []) = |a []| +length (nub []) +== length [] -- by nub_Empty +== 0 -- by def of length + +|a []| +== |{}| -- by alpha +== 0 -- by def of || - Induction step: lemma_length(ys) => lemma_length(y : ys) - IH: - To show: +Induction step: L_length(ys) => L_length(y : ys) +IH: length (nub ys) = |a ys| +To show: length (nub (y:ys)) = |a (y:ys)| +Proof by cases +case: y `elem` ys + length (nub (y:ys)) + == length (nub ys) -- by nub_Cons + == |a ys| -- IH + + |a (y:ys)| + == |{y} union a ys| -- alpha_Cons + == |(a ys)| -- by basic property - Proof by cases: - Case: +case: not (y `elem` ys) + length (nub (y:ys)) + == length (y : (nub ys)) -- by nub_Cons + == 1 + length [] + length (nub ys) -- by length_Cons + == 1 + length (nub ys) -- by length_Empty + == 1 + |a ys| -- IH - Case: + |a (y:ys)| + == |{y} union a ys| -- alpha_Cons + == |{y}| + |a ys| -- by def of union, case + == 1 + |a ys| -- by def of || + +qed -} @@ -94,16 +150,135 @@ {- siehe Queue.hs und SuperQueue.hs -} {- +Simulationseigenschaften zu beweisen: + + \alpha empty = [] + isEmpty q = \alpha q == [] + \alpha (enqueue x q) = \alpha q ++ [x] + ~ isEmpty q ==> \alpha (dequeue q) = (head (\alpha q), tail (\alpha q)) + q == q' = \alpha q == \alpha q' + Definition von \alpha: - \alpha (Queue front kcab) = undefined + \alpha (Queue front kcab) = front ++ reverse kcab + +Beweis fuer "empty": + + \alpha empty + = \alpha (Queue [] []) -- by def of empty + = [] ++ reverse [] -- by def of \alpha + = [] -- by def of reverse, ++ + +Beweis fuer "isEmpty": + + Hilfssatz: q == Queue [] [] = \alpha q == [] + + isEmpty q + = q == Queue [] [] -- by def of isEmpty + = \alpha q == [] -- by lemma + +Beweis fuer "enqueue": + + Sei q = Queue front kcab -- by exhaustivity of constructor + \alpha (enqueue x q) + = \alpha (enqueue x (Queue front kcab)) + -- by def of q + = \alpha (Queue (front (x : kcab))) -- by def of enqueue + = front ++ reverse (x : kcab) -- by def of \alpha + = front ++ (reverse kcab ++ [x]) -- by def of reverse + = (front ++ reverse kcab) ++ [x] -- by commutativity of ++ + = \alpha (Queue front kcab) ++ [x] -- by def of \alpha + = \alpha q ++ [x] -- by def of q + +Hilfslemma L: + + Zu beweisen: \alpha (Queue [] kcab) = \alpha (Queue (reverse kcab) []) + + \alpha (Queue [] kcab) + = [] ++ reverse kcab -- by def of \alpha + = reverse kcab -- by def of ++ + + \alpha (Queue (reverse kcab) []) + = reverse kcab ++ [] -- by def of \alpha + = reverse kcab -- by def of ++ + +Beweis fuer "dequeue": + + Annahme: ~ isEmpty q + + Sei q = Queue front kcab + + Fallunterscheidung auf front und kcab: + + Fall front = [], kcab = []: + ~ isEmpty (Queue front kcab) + = ~ isEmpty (Queue [] []) + = False + Nichts mehr zu beweisen, weil die Annahme nicht erfuellt ist. -Simulationseigenschaften: (5) + Fall front /= []: + \alpha (dequeue q) + = \alpha (dequeue (Queue front kcab)) + -- def of q + = \alpha (head front, Queue (tail front) kcab) + -- def of dequeue (2nd equation) + = (head front, \alpha (Queue (tail front) kcab)) + -- \alpha is an homomorphism + + Es bleibt zu beweisen, dass + head front = head (\alpha q) + \alpha (Queue (tail front) kcab) = tail (\alpha q) + + head (\alpha q) + = head (\alpha (Queue front kcab)) -- def of q + = head (front ++ reverse kcab) -- def of \alpha + = head front -- basic prop of head, front /= [] + + \alpha (Queue (tail front) kcab) + = tail front ++ reverse kcab -- def of \alpha + + tail (\alpha q) + = tail (\alpha (Queue front kcab)) -- def of q + = tail (front ++ reverse kcab) -- def of \alpha + = tail front ++ reverse kcab -- basic prop of tail, front /= [] + Fall front = [], kcab /= []: + \alpha (dequeue q) + = \alpha (dequeue (Queue front kcab)) -- def of q + = \alpha (dequeue (Queue [] kcab)) -- assumption front = [] + = \alpha (dequeue (Queue (reverse kcab) [])) + -- def of dequeue (1st equation) + = (head (\alpha (Queue (reverse kcab) [])), + tail (\alpha (Queue (reverse kcab) []))) + -- by reduction to already proved + -- case, reverse kcab /= [] + = (head (\alpha (Queue [] kcab)), tail (\alpha (Queue [] kcab))) + -- by lemma L (twice) + = (head (\alpha q), tail (\alpha q)) -- by def of q (twice) -Beweise: +Beweis fuer ==: + + Zu beweisen: q == q' = \alpha q == \alpha q' + + Seien q = Queue (front kcab) + q' = Queue (front' kcab') + + q == q' + = Queue (front kcab) == Queue (front' kcab') + -- by def of q, q' + = toList (Queue (front kcab)) == toList (Queue (front' kcab')) + -- by def of == + = front ++ reverse kcab == front' ++ reverse kcab' + -- by def of toList + + \alpha q == \alpha q' + = \alpha (Queue (front kcab)) == \alpha (Queue (front' kcab')) + -- by def of == + = front ++ reverse kcab == front' ++ reverse kcab' + -- by def of \alpha + -} @@ -125,4 +300,4 @@ {---------------------------------------------------------------------} {- Aufgabe H10.3 -} -{- siehe Morsi.hs -} +{- siehe Morsi.hs -} \ No newline at end of file diff -r 34fea195e238 -r ce9610f08925 exercises/src/Queue.hs --- a/exercises/src/Queue.hs Fri Dec 21 01:44:45 2012 +0100 +++ b/exercises/src/Queue.hs Wed Jan 09 19:45:47 2013 +0100 @@ -1,4 +1,4 @@ -module Queue where +module Queue (Queue, empty, isEmpty, enqueue, dequeue) where import Test.QuickCheck import Test.QuickCheck.Poly (A) @@ -6,19 +6,20 @@ deriving (Eq, Show) empty :: Queue a -empty = undefined +empty = Queue [] isEmpty :: Queue a -> Bool -isEmpty (Queue xs) = undefined +isEmpty (Queue []) = True +isEmpty _ = False enqueue :: a -> Queue a -> Queue a -enqueue x (Queue xs) = undefined +enqueue x (Queue xs) = Queue (xs ++ [x]) dequeue :: Queue a -> (a, Queue a) -dequeue (Queue (x : xs)) = undefined +dequeue (Queue (x : xs)) = (x, Queue xs) toList :: Queue a -> [a] -toList (Queue xs) = undefined +toList (Queue xs) = xs {- QuickCheck Tests -} diff -r 34fea195e238 -r ce9610f08925 exercises/src/SetPairList.hs --- a/exercises/src/SetPairList.hs Fri Dec 21 01:44:45 2012 +0100 +++ b/exercises/src/SetPairList.hs Wed Jan 09 19:45:47 2013 +0100 @@ -1,35 +1,48 @@ --- ? +module SetPairList(Set, empty, insert, isin, size, union, delete) where -- Abstraction function {- - alpha (S x) = undefined + alpha :: Set a -> {a} + alpha (S []) = {} + alpha (S ((a, b):xs)) = {a..b} union (alpha xs) To show: (10 things) + alpha empty = {} + invar s ==> alpha (insert x s) = {x} union alpha s + invar s ==> alpha (delete x s) = alpha s \ {x} + invar s ==> isin x s = x \in alpha s + invar s ==> size s = |alpha s| + invar s1, invar s2 ==> alpha (union s1 s2) = (alpha s1) union (alpha s2) + + invar empty + invar s ==> invar (insert x s) + invar s ==> invar(delete x s) + invar s1, invar s2 ==> invar (union s1 s2) -} -- Interface -newtype Set a = S (...) +newtype Set a = S (PairList a) invar :: Integral a => Set a -> Bool -invar (S s) = undefined +invar (S s) = invarPL s empty :: Set a -empty = undefined +empty = S emptyPL insert :: Integral a => a -> Set a -> Set a -insert n (S s) = undefined +insert n (S s) = S (insertPL n s) isin :: Integral a => a -> Set a -> Bool -isin n (S s) = undefined +isin n (S s) = isinPL n s size :: Integral a => Set a -> Integer -size (S s) = undefined +size (S s) = sizePL s union :: Integral a => Set a -> Set a -> Set a -union (S s1) (S s2) = undefined +union (S s1) (S s2) = S (unionPL s1 s2) delete :: Integral a => a -> Set a -> Set a -delete n (S s) = undefined +delete n (S s) = S (deletePL n s) -- Implementation type PairList a = [(a, a)] diff -r 34fea195e238 -r ce9610f08925 exercises/src/SuperQueue.hs --- a/exercises/src/SuperQueue.hs Fri Dec 21 01:44:45 2012 +0100 +++ b/exercises/src/SuperQueue.hs Wed Jan 09 19:45:47 2013 +0100 @@ -1,29 +1,31 @@ -module SuperQueue where +module SuperQueue (Queue, empty, enqueue, dequeue) where import Test.QuickCheck import Test.QuickCheck.Poly (A) data Queue a = Queue [a] [a] empty :: Queue a -empty = undefined +empty = Queue [] [] isEmpty :: Queue a -> Bool -isEmpty (Queue front kcab) = undefined +isEmpty (Queue [] []) = True +isEmpty _ = False enqueue :: a -> Queue a -> Queue a -enqueue x (Queue front kcab) = undefined +enqueue x (Queue front kcab) = Queue front (x : kcab) dequeue :: Queue a -> (a, Queue a) -dequeue (Queue front kcab) = undefined +dequeue (Queue [] kcab) = dequeue (Queue (reverse kcab) []) +dequeue (Queue front kcab) = (head front, Queue (tail front) kcab) toList :: Queue a -> [a] -toList (Queue front kcab) = undefined +toList (Queue front kcab) = front ++ reverse kcab instance Eq a => Eq (Queue a) where - q == q' = undefined + q == q' = toList q == toList q' instance Show a => Show (Queue a) where - show = undefined + show = show . toList {- QuickCheck Tests -}