module Sol_Exercise_4 where
import Test.QuickCheck
import Data.List

{- G1 -}

hasFibonacciProperty :: [Integer] -> Bool
hasFibonacciProperty (x:y:z:zs) = x + y == z && hasFibonacciProperty (y:z:zs)
hasFibonacciProperty _ = True

{- G2 -}

{-
Note: [x] is just a syntactic abbreviation for (x : [])

Lemma reverse (snoc xs x) = x : reverse xs
Proof by structural induction on xs

Base case:
To show: reverse (snoc [] x) = x : reverse []
reverse (snoc [] x)
== reverse [x]                 (by snoc_Nil)
== reverse [] ++ [x]           (by reverse_Cons)
== [] ++ [x]                   (by reverse_Nil)
== [x]                         (by append_Nil)
x : reverse []
== [x]                         (by reverse_Nil)

Induction step:
IH: reverse (snoc ys x) = x : reverse ys
To show: reverse (snoc (y : ys) x) = x : reverse (y : ys)
reverse (snoc (y : ys) x)
== reverse (y : snoc ys x)     (by snoc_Cons)
== reverse (snoc ys x) ++ [y]  (by reverse_Cons)
== (x : reverse ys) ++ [y]     (by IH)
== x : (reverse ys ++ [y])     (by append_Cons)
x : reverse (y : ys)
== x : (reverse ys ++ [y])     (by reverse_Cons)
-}

{- G3 -}

perms :: [Char] -> [[Char]]
perms "" = [""]
perms xs = reverse (sort (nub [y:ys | y <- xs, ys <- perms (delete y xs)]))

{- G4 -}

match :: [Char] -> [Char] -> Bool
match [] ys = null ys
match ('?' : ps) (_ : ys) = match ps ys
match ('*' : ps) [] = match ps []
match ('*' : ps) (y : ys) = match ps (y : ys) || match ('*' : ps) ys
match (p : ps) [] = False
match (p : ps) (y : ys) = p == y && match ps ys


{- H1 -}

matchingWords ws = aux [w | w <- ws, not (null w)]
  where aux [] = True
        aux [w] = True
        -- we have just removed the empty words, so `head` and `last` are safe here
        aux (w1 : w2 : ws) = last w1 == head w2 && aux (w2 : ws)

{- H2 -}

chunks :: [Int] -> [a] -> [[a]]
chunks _ [] = []
chunks [] _ = []
chunks (k : ks) xs = take k xs : chunks ks (drop k xs)

-- The type annotation `xs :: [Char]` forces GHC to use a reasonable type here
-- otherwise, it would just test lists of `()` (which has just one element, therefore quite boring)

prop_chunks_concat xs ks =
  all (> 0) ks ==> sum ks <= length xs ==> not (null ks) ==>
    concat (chunks ks (xs :: [Char])) == take (sum ks) xs

prop_chunks_no_null xs ks =
  all (> 0) ks ==> sum ks <= length xs ==> not (null ks) ==>
    let notNull xs = not (null xs) in
      all notNull (chunks ks (xs :: [Char]))

-- To check these properties, call `checkPropConcat` and `checkPropNoNull` in GHCi

checkPropConcat =
  quickCheckWith stdArgs{maxDiscardRatio=9001,maxSize=5} prop_chunks_concat

checkPropNoNull =
  quickCheckWith stdArgs{maxDiscardRatio=9001,maxSize=5} prop_chunks_no_null

{- H3 -}

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

Base case:
To show: length (snoc [] x) = length (x : [])
length (snoc [] x)
== length [x]                   (by snoc_Nil)
== length [] + 1                (by length_Cons)
== 0 + 1                        (by length_Nil)
== 1
length (x : [])
== length [] + 1                (by length_Cons)
== 0 + 1                        (by length_Nil)
== 1

Induction step:
IH: length (snoc ys x) = length (x : ys)
To show: length (snoc (y : ys) x) = length (x : (y : ys))
length (snoc (y : ys) x)
== length (y : snoc ys x)       (by snoc_Cons)
== length (snoc ys x) + 1       (by length_Cons)
== length (x : ys) + 1          (by IH)
== length ys + 2                (by length_Cons)
length (x : (y : ys))
== length (y : ys) + 1          (by length_Cons)
== length ys + 2                (by length_Cons)
-}