module Exercise_4 where

{- H1 -}

strictlyDescending :: [Integer] -> Bool
strictlyDescending [] = True
strictlyDescending (x:xs)= length xs == 0 || x > head xs && strictlyDescending xs

{- H2 -}

chunks :: Int -> [a] -> [[a]]
chunks = undefined

irregularChunks :: [Int] -> [a] -> [[a]]
irregularChunks = undefined

{- H3 -}

{-WETT-}
upsAndDowns :: Ord a => [a] -> [[a]]
upsAndDowns xs = upsAndDowns2 xs []

upsAndDowns2 :: Ord a => [a] -> [a] -> [[a]]
upsAndDowns2 (x:xs) (y:ys)
	| x >= y = upsAndDowns2 xs (x:y:ys)
	| otherwise = reverse (y:ys) : downsAndUps2 (x:xs) []
upsAndDowns2 (x:xs) [] = upsAndDowns2 xs [x]
upsAndDowns2 [] ys = [reverse ys]

downsAndUps2 :: Ord a => [a] -> [a] -> [[a]]
downsAndUps2 (x:xs) (y:ys)
	| x <= y = downsAndUps2 xs (x:y:ys)
	| otherwise = reverse (y:ys) : upsAndDowns2 (x:xs) []
downsAndUps2 (x:xs) [] = downsAndUps2 xs [x]
downsAndUps2 [] ys = [reverse ys]


{-TTEW-}

{- H4 -}

{-
Lemma: length ( reverse xs) = length xs
Proof by structural induction on xs

Base case:
To show: length ( reverse []) = length []
length ( reverse xs)
= length [] -- by reverse_Nil

Induction step:
To show: length ( reverse (x:xs)) = length (x:xs)
length ( reverse (x:xs))
= length (reverse xs ++ [x])       -- by reverse_Cons
= length (reverse xs) + length [x] -- by length_append
= length xs + length [x]		   -- by IH
= length xs	+ length [] + 1	   	   -- by length_Cons
= length xs + 1					   -- by length_Nil
length (x:xs)
= length xs + 1					   -- by length_Nil
 -}