{-
--------------------------------------------------------------
-- Problem 1a
Formulate QuickCheck properties and generators to test the correctness
of a sorting function |mysort :: [Weekday] -> [Weekday]|.
-}

import Test.QuickCheck
import Data.List((\\), sort)

ordered :: Ord a => [a] -> Bool
ordered (x:y:ys)  =  x <= y && ordered (y:ys)
ordered _         =  True -- shorter lists are always ordered

bagEq :: Eq a => [a] -> [a] -> Bool 
bagEq xs ys = null (xs \\ ys) && null (ys \\ xs)

prop_mysort_correct :: [Weekday] -> Bool
prop_mysort_correct xs = ordered ys && bagEq xs ys
  where ys = mysort xs

instance Arbitrary Weekday where
  arbitrary = elements [Mon .. Sun]

-- Part of the problem formulation + some testing code:

data Weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun 
  deriving (Eq, Ord, Show, Enum)

mysort' xs = (if length xs == 14 then reverse else id) (sort xs)
mysort xs = sort xs

main = quickCheck prop_mysort_correct

{-
-- --------------------------------------------------------------  
-- Problem 1b  

Pick any |x|.
  
Proof by induction on the list |ys| for the predicate

  P ys = length (insert x ys) === 1 + length ys

Base case |P []|:

     length (insert x [])
==  {- Def. |ins.0| -}
     length [x]
==  {- Def. |len.0| -}
     1 + length []

Case |P (y:ys)|:

Induction hypothesis |P ys| is 
  |length (insert x ys) === 1 + length ys|.

subcase |x <= y|:

     length (insert x (y:ys))
==  {- Def. |ins.1a| -}
     length (x : y : ys)
==  {- Def. |len.1| -}
     1 + length (y:ys) 

subcase |x > y|:

     length (insert x (y:ys))
==  {- Def. |ins.1b| -}
     length (y : insert x ys)
==  {- Def. |len.1| -}
     1 + length (insert x ys) 
==  {- Induction hypothesis -}
     1 + (1 + length ys)
==  {- Def. |len.1| -}
     1 + length (y:ys)

-}