Haskell Chinese Remainder theorem

Question

I understand that in order for this function to work crtHasSolution has to be true first I'm having trouble proving that n could be a solution any ideas or tips in how to write or check that in haskell?

I know that the conditions for N are that it has to be bigger or equal to 0 and smaller then m which is the product of all the mod bases.

crtHasSolution :: [Integer] -> [Integer] -> Bool
crtHasSolution as ms = length as > 0 &&
                       length ms > 0 &&
                       length as == length ms &&
                       all (>=0) as &&
                       all (>=2) ms &&
                       pairwise_coprime ms

-- Is a given number a solution to a CRT problem?
-- usage: crtIsSolution n as ms = ans
-- assures: ans == True, if crtHasSolution as ms == True and n is a solution
--          ans == False, otherwise

crtIsSolution :: Integer -> [Integer] -> [Integer] -> Bool
crtIsSolution n as ms = crtHasSolution as ms &&
                        n >= 0 &&
                        n < m
                        where m =

code

Answer 1

From wikipedia:

It is easy to check whether a value of x is a solution: it suffices to compute the remainder of the Euclidean division of x by each [m_i].

If x `mod` m_i /= a_i for any i, then x is not a solution.

This smacks of homework, so rather than give you a one-liner that computes this, I'm going to give you some leading questions for your implementation of crtIsSolution n as ms:

• Is n a solution if ms and as are empty?
• If you can compute whether n `mod` m_0 == a_0 and whether n is a solution for ms_0 and as_0, can you compute whether n is a solution for m_0:ms_0 and a_0:as_0?