a-conjecture-of-mine

An exercise on polyglossy: the same problem solved on multiple languages
Main.idr (1632B)

 1 -- The following program is a simple test for the following conjecture:
 2 
 3 -- Let S: N -> N be the sum of the digits of a positive integer.
 4 -- For all A and B in N, S(A + B) = S(A) + S(B) - 9k, where k is an integer.
 5 
 6 module Main where
 7 
 8 import Numeric (readDec)
 9 import Numeric.Natural
10 import System.Environment
11 import System.Exit
12 import Control.Monad (foldM)
13 import Data.Vector (Vector, unsafeIndex, generate)
14 
15 main : IO Int
16 main = do
17     args <- getArgs
18         
19     case readDec <$> head' args of
20         Just [(max, "")] =>
21             if counterexempl max then exitFailure else exitSuccess
22 
23         _ => exitInvalidInput
24     
25     where head' [] = Nothing
26           head' xs = Just (head xs)
27 
28 -- Calculates the sum of the digits of `n`.
29 sumDigits : Int -> Int
30 sumDigits = sumDigitsTail 0
31     where sumDigitsTail acc n
32               | n == 0 = acc
33               | otherwise = sumDigitsTail (acc + (n `mod` 10)) (n `div` 10)
34 
35 -- Returns `True` if the if the conjecture holds for pair.
36 -- Otherwise returns `False`.
37 test' : Vector Int -> (Int, Int) -> Bool
38 test' sums (a, b) = diff `mod` 9 == 0
39     where diff = sums ! (a + b) - sums ! a - sums ! b
40           (!) = unsafeIndex
41 
42 -- Checks if there is any counterexample in
43 -- [(a, b) | a <- [0..max], b <- [a..max]].
44 --
45 -- Returns `True` if a counter example was found.
46 -- Otherwise returns `False`.
47 counterexempl : Int -> Bool
48 counterexempl max =
49     all (test' sums) [(a, b) | a <- [0..max], b <- [a..max]]
50     where sums = generate (2 * max + 1) sumDigits
51 
52 exitInvalidInput : IO Int
53 exitInvalidInput = exitWith $ ExitFailure 2
54