Lean должен знать, что рекурсивный def завершается, прежде чем принять его как определение. Структурную рекурсию он находит сам. Иначе пробует фундированную рекурсию, а вы помогаете ему через termination_by, называя меру, и через decreasing_by, доказывая, что каждый вызов её уменьшает.
Для числа шагов Коллатца известной меры нет. Никто не доказал, что эта функция завершается на любом входе. Поэтому пишем partial def. Lean её компилирует и выполняет. Он требует, чтобы тип результата был населён, а в доказательствах определение непрозрачно. Вычислять можно. Рассуждать о её развёртке нельзя.
Мне этот обмен нравится. Ключевое слово здесь и есть спецификация, которая говорит правду. Тотальный def утверждает, что функция возвращает результат на каждом входе, и проверка заставляет за это отвечать. partial ничего такого не утверждает.
Любая проверка, которая всегда даёт ответ, обязана отвергать и некоторые завершающиеся функции. Пусть. Цена отказа одно честное ключевое слово, а программа всё равно работает.
