Haskell Китайская теорема об остатках

Question

Я понимаю, что для того, чтобы эта функция работала, во-первых, crtHasSolution должен быть правдой. У меня возникают проблемы с доказательством того, что n может быть решением, какие-либо идеи или советы о том, как написать или проверить это в haskell?

Я знаю, что условия для N состоят в том, что он должен быть больше или равен 0 и меньше, чем m, который является произведением всех баз модов.

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 =

код

Answer 1

Из википедии:

Легко проверить, является ли значение x является решением: достаточно вычислить остаток от евклидова деления x каждым [ m_i ].

Если x `mod` m_i /= a_i для любого i, затем x это не решение

Это отдает домашним заданием, поэтому вместо того, чтобы дать вам однострочник, который вычисляет это, я дам вам несколько наводящих вопросов для вашей реализации crtIsSolution n as ms:

• Является n решение, если ms а также as пусты?
• Если вы можете вычислить, n `mod` m_0 == a_0 и будь n это решение для ms_0 а также as_0 Можете ли вы вычислить, n это решение для m_0:ms_0 а также a_0:as_0?