Как я доказал математическую теорему с помощью haskell

В твиттере есть замечательный ресурс 1HaskellADay. Каждый день (или почти каждый) там предлагается решить какую-нибудь интересную задачу на языке haskell. Недавно решал такую задачку. Нужно найти непрерывную последовательность из 17 целых чисел, для каждого из которых существует другое число из этой же последовательности, такое, что эти два числа не являются взаимно простыми. Взаимно простыми (co-prime) называются такие два числа, у которых наибольший общий делитель (НОД или по-английски greatest common divisor (GCD)) больше 1. Так, числа 5 и 9 являются взаимно простыми, а все четные числа — нет, поскольку их НОД как минимум равен 2. Не взаимно простые числа называются по-английски co-composed (по крайней мере в этой задаче). Решение в haskell выглядит очень лаконично.

import Data.List

coComposedSet :: Integer -> [[Integer]]
coComposedSet s =
    [r | a <- [1 .. ], let r = [a .. a + s - 1],
     (== s) $ genericLength $ group [x | x <- r, y <- r, y /= x, gcd x y > 1]]

Функция coComposedSet состоит из двух строк и представляет собой генератор таких последовательностей длиной s на всем множестве целых чисел (поэтому типом множества выбран Integer, который не имеет ограничений). Чтобы получить первые 10 последовательностей длиной 17, нужно передать генератор функции take 10.

main :: IO ()
main = print $ take 10 $ coComposedSet 17

Считается эта штука достаточно быстро. Если скомпилировать программу с флагом -O2, то на моей машине Intel Core i5 время расчета составит чуть больше четырех секунд.

ghc --make -O2 coComposedSet.hs
[1 of 1] Compiling Main             ( coComposedSet.hs, coComposedSet.o )
Linking coComposedSet ...
time ./coComposedSet 
[[2184,2185,2186,2187,2188,2189,2190,2191,2192,2193,2194,2195,2196,2197,2198,2199,2200],
[27830,27831,27832,27833,27834,27835,27836,27837,27838,27839,27840,27841,27842,27843,27844,27845,27846],
[32214,32215,32216,32217,32218,32219,32220,32221,32222,32223,32224,32225,32226,32227,32228,32229,32230],
[57860,57861,57862,57863,57864,57865,57866,57867,57868,57869,57870,57871,57872,57873,57874,57875,57876],
[62244,62245,62246,62247,62248,62249,62250,62251,62252,62253,62254,62255,62256,62257,62258,62259,62260],
[87890,87891,87892,87893,87894,87895,87896,87897,87898,87899,87900,87901,87902,87903,87904,87905,87906],
[92274,92275,92276,92277,92278,92279,92280,92281,92282,92283,92284,92285,92286,92287,92288,92289,92290],
[117920,117921,117922,117923,117924,117925,117926,117927,117928,117929,117930,117931,117932,117933,117934,117935,117936],
[122304,122305,122306,122307,122308,122309,122310,122311,122312,122313,122314,122315,122316,122317,122318,122319,122320],
[147950,147951,147952,147953,147954,147955,147956,147957,147958,147959,147960,147961,147962,147963,147964,147965,147966]]

real    0m4.161s
user    0m4.147s
sys     0m0.013s

Я перенес все подсписки в отдельные строки для удобочитаемости, программа выводит всё в одну строку. А теперь переходим к теореме. Автор задачи попросил доказать, что не существует последовательностей длиной меньше 17, которые удовлетворяют условиям задачи. С короткими последовательностями длиной от 2 до 5 всё просто. Я приведу теоретические доказательства для этих случаев.

• Длина 2. Легко показать, что все соседние числа являются взаимно простыми. В самом деле, пусть k является НОД двух соседних чисел n и n + 1. Тогда $$k \cdot l = n$$ $$k \cdot m = n + 1$$ , где l и m — произведения остальных делителей чисел n и n + 1. Отсюда следует, что $$k \cdot (m - l) = 1$$ , а это значит, что k может быть равным только 1, то есть числа n и n + 1 — взаимно простые.
• Длина 3. Число в середине последовательности является соседним для обоих крайних чисел, а значит взаимно простым с ними.
• Длина 4. Возможны две зеркальные ситуации: последовательность начинается с четного числа или с нечетного. В обоих случаях нечетное число, находящееся между двумя четными, не может быть не взаимно простым ни с этими четными числами, так как они для него являются соседними, ни с крайним нечетным числом, поскольку для двух последовательных нечетных чисел должно выполняться равенство $$k \cdot (m - l) = 2$$ , то есть k как НОД должен быть равен 2, однако это противоречит условию, что эти два числа нечетные.
• Длина 5. Возможны два случая.
  • Четные числа по краям и в середине, нечетные - второе и четвертое. В этом случае, следуя ограничениям, выведенным в предыдущих случаях, второе число может быть не взаимно простым только с пятым, а четвертое — с первым. При этом их НОД должен удовлетворять условию $$k \cdot (m - l) = 3$$ , следовательно он равен 3 для обоих нечетных чисел — второго и четвертого. Это противоречит нашему выводу о том, что два последовательных нечетных числа могут быть только взаимно простыми.
  • Нечетные числа по краям и в середине, четные - второе и четвертое. Среднее нечетное число является всегда взаимно простым с другими четырьмя — это также следует из уже доказанных свойств соседних чисел.

Случай с последовательностью из 16 чисел я теоретически доказывать не хочу, на мой взгляд это сложно, хотя, возможно, я упускаю какие-то простые факты, которые можно было бы использовать в доказательстве. Но я не буду этого делать еще по одной простой причине — доказательство можно легко провести с помощью простой программы на haskell! Идея такова. Внутри любой непрерывной последовательности из s чисел не существует числа, являющегося взаимно простым по отношению к остальным числам последовательности только в том случае, если ни одна из всевозможных комбинаций НОД-соседних чисел внутри заданной последовательности, включающая 2 и более элементов для всех НОД, соответствующих простым числам меньшим s, не задействует все элементы последовательности одновременно. НОД-соседними числами я называю идущие подряд четные числа, идущие подряд числа, кратные трем и так далее. Так, в случае последовательности длиной 16 нужно доказать, что ни одна из взаимных комбинаций НОД-соседних чисел для НОД равных 2, 3, 5, 7, 11 и 13 длиной от двух элементов не покрывает все 16 чисел последовательности одновременно. Следующая функция coComposedLayouts возвращает всевозможные комбинации НОД-соседних чисел внутри произвольной последовательности длиной s для заданного значения НОД m.

-- get all possible layouts of numbers with common factor m inside
-- an arbitrary contiguous range of s numbers; each layout must contain
-- at least 2 elements
coComposedLayouts :: Int -> Int -> [[Int]]
coComposedLayouts m s =
    filter ((> 1) . length . take 2) $
    map (takeWhile (<= s) . iterate (+ m)) [1 .. m]

Загрузим исходную программу (файл coComposedSet.hs) в ghci и проверим, как она работает.

:l coComposedSet.hs
[1 of 1] Compiling Main             ( coComposedSet.hs, interpreted )
Ok, modules loaded: Main.
coComposedLayouts 2 16
[[1,3,5,7,9,11,13,15],[2,4,6,8,10,12,14,16]]
coComposedLayouts 3 16
[[1,4,7,10,13,16],[2,5,8,11,14],[3,6,9,12,15]]

Числа внутри подсписков — индексы элементов внутри произвольной непрерывной последовательности чисел (от 1 до s), которые будут заняты НОД-соседними числами. В первом тесте мы проверили возможные варианты расположения четных чисел внутри последовательности длиной 16, во втором — варианты расположения чисел, кратных трем в такой же последовательности чисел. Выглядит разумно. А теперь напишем функцию coComposedPrimeLayouts13, которая соберет все возможные комбинации НОД-соседних чисел для всех простых НОД от 2 до 13, сортируя все элементы внутри каждой комбинации.

-- get union of all possible combinations of numbers with common prime factors
-- 2, 3, 5, 7, 11 and 13 inside an arbitrary contiguous range of s numbers
coComposedPrimeLayouts13 :: Int -> [[Int]]
coComposedPrimeLayouts13 s =
    map (sort . concat)
    [a:b:c:d:e:[f] | a <- coComposedLayouts 2  s, b <- coComposedLayouts 3  s,
                     c <- coComposedLayouts 5  s, d <- coComposedLayouts 7  s,
                     e <- coComposedLayouts 11 s, f <- coComposedLayouts 13 s]

Выглядит не очень красиво (в идеале хотелось бы обобщенную реализацию для всех простых НОД меньших s), но работает правильно: можете проверить в ghci, но вывод будет очень длинный! А вот и функция, которая находит, существует ли последовательность длиной s, удовлетворяющая условию задачи.

-- test if an arbitrary contiguous range of s numbers may have full co-composed
-- set of numbers, maximum tested prime layout is 13: this is enough for ranges
-- up to 17 numbers
hasCoComposedSet13 :: Int -> Bool
hasCoComposedSet13 s =
    elem s $ map (length . group) $ coComposedPrimeLayouts13 s

С помощью функции hasCoComposedSet13 можно доказать, что на всем множестве целых чисел не существует непрерывной последовательности длиной меньше 17, в которой для каждого числа найдется хотя бы одно другое число, не взаимно простое с исходным. А также доказать, что имеются последовательности длиной 17 чисел, для которых это условие удовлетворяется: мы находили такие последовательности с помощью функции coComposedSet 17.

map hasCoComposedSet13 [2 .. 17]
[False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,True]

Теорема доказана! Исходный код программы можно найти здесь. Комментарии в строках 28–43 не верны, я не удалил их по историческим причинам. Update. Написал обобщенные версии функций coComposedPrimeLayouts и hasCoComposedSet, которые вычисляют список простых чисел, укладывающихся в заданную длину s последовательности чисел и, следовательно, подходящих для проверки существования последовательностей с искомыми свойствами произвольной длины, во время выполнения программы.

-- generalized coComposedPrimeLayouts13 with run-time calculation of
-- prime factors, requires import Data.Numbers.Primes
coComposedPrimeLayouts :: Int -> [[Int]]
coComposedPrimeLayouts s =
    map (sort . concat) $ mapM (`coComposedLayouts` s) $ takeWhile (< s) primes

--- same as hasCoComposedSet13 but uses generalized coComposedPrimeLayouts
hasCoComposedSet :: Int -> Bool
hasCoComposedSet s =
    elem s $ map (length . group) $ coComposedPrimeLayouts s

Для использования функции primes нужно подключить модуль Data.Numbers.Primes.