-- part 1
data Nat = Z | S Nat deriving (Eq, Ord, Show);
num 0 = Z
num n = S (num (n-1))
seven = num 7
inf = S inf
-- part 2
-- not-equal (!=) is still semidecidable
-- seven != infinity => True
-- inf /= inf => no answer
-- equal (==) is *not* semidecidable
-- inf == inf => no answer
-- less-than-infinity *is* semidecidable
-- seven < inf => True
-- inf < seven => False
-- part 3
instance Num Nat where
Z + b = b
(S a) + b = S (a + b)
Z * b = Z
(S a) * b = b + (a * b)
abs n = n
signum Z = Z
signum (S _) = S Z
fromInteger = num
-- now we can do some arithmetic
-- notice in particular that we can calculate inf + seven
-- or inf * seven
-- and it delivers the right answer
-- we can also answer questions like
-- inf * seven > two -- returns True
-- part 4
-- caution: DOES NOT WORK PROPERLY
example p =
if p Z then Z
else S (example(p.S))
-- caution: DOES NOT WORK PROPERLY
counterexample p = example (not . p)
-- so for example
-- very good
isBig x = x > seven
-- very good
isSeven x = x == seven
-- very good
isSolution x = x*x + x == num 6
-- totally wrong
isSolution' x = x*x + x == num 7
-- part 5
-- caution: DOES NOT WORK PROPERLY
example p =
if p Z then Z
else S (example(p.S))
example p = tryFrom p Z
tryFrom p x = if p x then x
else tryFrom p (S x)
-- caution: DOES NOT WORK PROPERLY
counterexample p = example (not . p)
-- so for example
-- very good
isBig x = x > seven
-- very good
isSeven x = x == seven
-- very good
isSolution x = x*x + x == num 6
-- totally wrong
isSolution' x = x*x + x == num 7
-- this, however, works flawlessly
exists p = p x
where x = example p
-- likewise
forall p = p c
where c = counterexample p
isNotOneHalf x = x + x /= num 1
-- forall (\x -> not (x * x + x == num 7))