Как доказать АГДЕ, что существует число, которое имеет больше делителей, чем данное.

Вопрос или проблема

natRange : Nat → List Nat
natRange zero = []
natRange (suc n) = n ∷ natRange n

numberOfDivisors : Nat → Nat
numberOfDivisors n = (length ∘₂ filterᵇ) (λ {zero → false ; x@(suc _) → n % x == zero}) (natRange (suc n))

-- получить треугольное число
triangleNumber : Nat → Nat
triangleNumber zero = zero
triangleNumber (suc n) = suc n + triangleNumber n

-- рекурсивный алгоритм
findTriangleNumberRecursively : (trNum : Nat) .{{_ : NonZero trNum}} → Nat
findTriangleNumberRecursively n = 
    if ((numberOfDivisors ∘ triangleNumber) n) < 500
        then findTriangleNumberRecursively (suc n)
    else triangleNumber n

main : IO ⊤
main = (putStrLn ∘ show) (findTriangleNumberRecursively (suc zero))

Проверка завершения не удалась для следующих функций:
  findTriangleNumberRecursively
Проблемные вызовы:
  findTriangleNumberRecursively (suc n)

Ответ или решение

Вам требуется доказать, что для любого натурального числа ( n ) существует такое число ( m ), что количество делителей числа ( m ) больше, чем количество делителей числа ( n ). Это можно сделать, проанализировав поведение функции, вычисляющей количество делителей, и соответствующий алгоритм в Agda.

Доказательство существования числа с большим количеством делителей

Количество делителей числа ( n ) можно определить через его разложение на простые множители. Если ( n = p_1^{e_1} p_2^{e_2} \ldots p_k^{e_k} ), то количество делителей можно вычислить по формуле:
[
d(n) = (e_1 + 1)(e_2 + 1) \cdots (e_k + 1)
]
Чтобы доказать, что для любого ( n ) существует ( m ) с ( d(m) > d(n) ), достаточно заметить, что увеличивая ( n ) на 1, мы большую вероятность дадим нам большее количество делителей. Например, если ( m = n + 1 ), то для простых ( n ) мы имеем больше возможностей для разложения.

Пример в Agda

1. Использование количества делителей: Ваша реализация функции numberOfDivisors корректна, но можно улучшить понятие о делителях.
2. Проблема с терминальностью: Ошибка "Termination checking failed" возникает из-за того, что Agda не может гарантировать, что ваш рекурсивный вызов всегда приведет к базовому случаю.

Вы можете переписать функцию с использованием механизма, который бы зафиксировал максимум для ( n ), например так:

findTriangleNumberRecursively : (trNum : Nat) .{{ _ : NonZero trNum }} → Nat
findTriangleNumberRecursively n = 
    let d = numberOfDivisors (triangleNumber n)
    in if d < 500 then
        findTriangleNumberRecursively (suc n)
    else
        triangleNumber n

Изменение условия рекурсии

Чтобы убедиться в том, что рекурсивный вызов может завершиться, вы можете добавить доказательство, что количество делителей будет расти. Например, вы можете использовать индукцию для того, чтобы показать, что:

• При увеличении ( n ), количество делителей ( d(n) ) будет либо не уменьшаться, либо возрастать. Просто добавьте дополнительное следствие:

  {R : Nat → Set} → (∀ n → R n → R (suc n)) → R zero → (n : Nat) → R n

  Это поможет доказать, что количество делителей будет изменяться при переходе к ( n + 1 ).

Заключение

Ваша основная проблема заключается в том, что Agda не может проверить, что функция вызывается на меньших значениях достаточное количество раз для завершения. Обеспечив сильное основание индукции и параллельно контролируя количество делителей, вы сможете обеспечить корректность вашей функции.