{-
--------------------------------------------------------------
-- 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)
-}