Снова о статической типизации

Но это условие далеко не равносильно проверке количества итераций. Первое число, для которого f вернёт 0, равно 2684647.

Я не прошу функцию, я прошу её тип.

Был вопрос, сможет ли Coq скомпилировать такую функцию. С учётом того, что ему для компиляции надо доказать завершимость.

Здесь всего 100000000000 состояний. То есть можно гарантированно считать функцию не завершающейся, если она не завершилась за 100000000000 итераций, даже если не запоминать предыдущие.

Причём, если проверять снизу вверх, то любое падение ниже того, из которого началась рекурсия, завершает доказательство. Также как и любой вылет выше 100000000000. То есть две трети диапазона проверяются тривиально.

понял спасибо. в таком случае просто передаём число итераций и говорим что по нему завершаемся.

Fixpoint f (k : Z) fuel {struct fuel} : Z :=
  match fuel with
  | O => 0
  | S fuel =>
    if k =? 1 then 1
    else if k >? 100000000000 then 0
    else if k mod 2 =? 0 then f (k/2) fuel
    else f (3*k+1) fuel
  end.

Compute f 3 100000000000.

понял спасибо. в таком случае просто передаём число итераций и говорим что по нему завершаемся.

Так наоборот же надо. Если дошли до неё, то ошибка типизации.

будет ли работать (в браузере точно нет) - числа большие.

ну вот. суровый каток математики споткнулся о флопсы и свалился в пропасть.

Так наоборот же надо. Если дошли до неё, то ошибка типизации.

предлагаю доказать завершимость алгоритма вычисления очередного биткоена. ну или любого заданного наперед биткоена. :)

Так наоборот же надо. Если дошли до неё, то ошибка типизации.

Задумался.

Кажется я начинаю что-то смутно понимать.

Т.е. мы хотим чтобы кок проанализировал функцию f, и построил алгоритм который бы видя аргументы функции f на этапе компиляции определял, завершиться ли наша f с ошибкой или с результатом. И если завершиться с ошибкой, то выдавал ошибку компиляции.

Или опять не то?

Есть уже готовый примитив синхронизации о котором я писал

... «Монитор Хоара», но я не помню точно, расставляет ли он что-то на этапе компиляции или нет.

Справедливости ради, речь ведь именно об этапе компиляции с самого начала. Ну, в поисковик просто никто не полез..

Критично отсутствие необходимости переписывать алгоритм лишь ради удовлетворения типов.

Как бы, когда пишешь на хаскеле и ракете, вряд ли ты пользуешься алгоритмами из c++. Тут уж ничего по моему не сделаешь.

Раз в coq есть гетерогенные списки, можно ли написать тип mapcar, полностью соответствующий его документации (а не обрубать под типизацию)? ...

Остальные аргументы должны быть гетерогенными списками.

На сколько я понимаю, всё таки гомогенными, иначе я не уловил, как функция будет принимать n-ный аргумент разных типов?

Так или иначе, есть сложность: нужно заранее знать типы аргументов (или типы гомогенных массивов, что одно и то же). Это нужно чтобы вычислить тип mapcar. Иначе неоткуда взять информацию о том какой тип у mapcar должен быть. А тип терма должен быть известен на этапе компиляции. Поэтому собственно там у меня гетерогенный список вместо списка аргументов переменной длины - я на этапе компиляции из него беру информацию об аргументах функции и строю для неё тип. Из списка аргументов эту информацию в коке брать нельзя (по крайней мере без штук вроде https://github.com/LPCIC/coq-elpi, но я её глядел только краем глаза и в возможностях не уверен).

Если передать первым параметром массив типов [bool, nat, option nat] как пример, то можно сделать переменное число массивов в качестве аргументов (число аргументов будет вычисляться из данного массива типов, т.е. у нас сейчас три аргумента у ф-ции и три массива аргументов).

Дезигнатор передать должно получится, только нужно условиться где мы ищем ф-цию (т.е массив функций должен существовать на этапе компиляции).

Разная длина передаваемых массивов не должна по идее вызвать проблему.

Т.е. ограничение которое сразу бросается в глаза - надо как-то знать типы агрументов чтобы вычислить тип функции. Остальное вроде дело техники, но это конечно практикой надо подтверждать, где там споткнёшься заранее не понятно.

Но я бы что то не знаю, не взялся бы наверное. Задача интересная если в смысле разобраться с elpi, но больно работы будет много, не уверен что найду время. А без epli, т.е. с передачей массива типов - задача не очень интересная: получиться должно в принципе, но работы многовато и всё таки есть шанс споткнуться на чём то нудном типа конверсия типов при определении в модулях не сработает.. и.п.. мне кажется получается деталей многовато для такого типа задачки.

ну вот. суровый каток математики споткнулся о флопсы и свалился в пропасть.

Я думаю это потому что взрослая математика - она не только про вычисления, как в школе (ветки типа вычмата и иже с ними), а ещё и про доказательства.

Вот кок он для той части где доказательсва в первую очередь. Писать на нём числодробилки по моему никто ещё не догадался. Но не знаю точно.

Ты утверждал, что если функция может зациклиться, то кок должен выдать ошибку.

Я написал функцию, которая завершается всегда, но доказательство нетривиально (точно есть только доказательство перебором).

Далее ты пишешь, что перебором нельзя доказать не завершимость.

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

В ответ ты переписываешь функцию в ту, которая гарантированно завершается. Так вопрос же был не про это.

Интересно было бы обсудить рекурсивные алгоритмы.
Если не ошибаюсь, то на каждом шаге алгоритма производится
сохранение, используемых значений переменных, а это весьма рессурсо-ёмко.
Но зато они очень вкусные.

Как бы, когда пишешь на хаскеле и ракете, вряд ли ты пользуешься алгоритмами из c++. Тут уж ничего по моему не сделаешь.

Вообще-то пользуюсь. Если мне надо какой-нибудь LRU-cache, то беру исходник на Си++ и адаптирую. В ракет вообще что угодно запихать можно, в Haskell в IO совместимость с С++ хорошая.

Поэтому собственно там у меня гетерогенный список вместо списка аргументов переменной длины - я на этапе компиляции из него беру информацию об аргументах функции и строю для неё тип.

Мы договорились, что для кока считаем, что аргументов всего два. Первый – функция, второй – массив, заменяющий остальные аргументы.

Если передать первым параметром массив типов [bool, nat, option nat] как пример, то можно сделать переменное число массивов в качестве аргументов (число аргументов будет вычисляться из данного массива типов, т.е. у нас сейчас три аргумента у ф-ции и три массива аргументов).

Тут проблема, что сами массивы гетерогенные. То есть, если у нас первый массив имеет тип [bool, nat, option nat], второй – [nat, bool], то функция (,) должна вернуть тип [(bool, nat), (nat, bool)]. И так для любых типов массивов и функций.

Я не прошу доказывать или приводить тело такого mapcar. Меня интересует, можно ли вообще записать такой тип. Потому что если списки оставлять только только моногенные, это ограничивает применение (в Typed Racket приходится местами вручную перекрывать типизацию, чтобы работало как надо). Если делать тип [Dynamic], то применение такой функции работает как поедатель типов: любая типизация со списков-аргументов теряется и должна быть вручную восстановлена после применения функции. Для типизированного языка это очень неприятно.

Если не ошибаюсь, то на каждом шаге алгоритма производится сохранение

В данном случае рекурсия хвостовая, поэтому можно не сохранять.

Про мьютексы.

У нас есть мьютексы с M<1> по M<n>.

Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.

Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.

Для мьютекса M<0> при запуске программы мы имеем объект mRoot: Locked<M<0>>.

Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:

lock<M<i>>(mK: Locked<M<k>>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n

которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.

Если мы хотим освободить мьютекст i, для этого имеется функция:

unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>

которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.

Типы Locked<M<i>> и LockLink<M<k>, M<i>> являются линейными.

В данном случае достаточно того, чтобы система типов поддерживала линейные типы.

Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.

P.S.

Также нужна функция, которая в конце алгоритма поглотит корневой mRoot, иначе программа тайпчек не пройдет:

dropRoot(mRoot: Locked<M<0>>) -> void

Как бы, когда пишешь на хаскеле и ракете, вряд ли ты пользуешься алгоритмами из c++.

Кстати, переносимостью алгоритма между языками можно пользоваться именно как критерием для парадокса Блаба. Чтобы сравнивались не абстрактные свойства языка, а конкретные алгоритмы, дающие конкретные преимущества при компиляции и/или исполнении.

В этом смысле, для того, чтобы статический язык стал строгим надмножеством динамического, достаточно типа Dynamic.

> "Wat" <> 1 <> "!" <> Null
"Wat1!"

Ты утверждал, что если функция может зациклиться, то кок должен выдать ошибку.

Утверждение «если функция может зациклится, то кок должен выдать ошибку.» - полностью верное. Но я, очевидно, не очень удачно выразился в целом.

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

Поэтому Кок поступает очень просто: он требует доказательство того что функция завершается.

Т.е. все проверки консервативны - система просто предполагает что функции не завершаются. И бремя доказательства лежит, конечно же, на программисте. Т.е. при написании программист должен ещё и доказать завершимость своих рекурсивных функций. Если доказательство не предоставить, Кок не примет определения да и всё.

Далее ты пишешь, что перебором нельзя доказать не завершимость.

Это я не знаю. Но что до завершимости, то впринципе конечно можно, но для этого перебор надо осуществить, наверное? Т.е. это как то похоже на рекурсию. Может я чего недопонял опять.

Я сделал просто - обдумав твоё утверждение, я просто ввёл счётчик и получил эквивалентный алгоритм. Но формально завершаемся мы теперь по счётчику. Т.е. я показал что алгоритм выполняющий перебор остановится. Этого достаточно для системы чтобы принять определение функции.

https://www.ispras.ru/proceedings/all-archives.php Архив выпусков Сборника трудов ИСП РАН

https://ispranproceedings.elpub.ru/jour/article/view/1233 Автоматическое доказательство корректности программ с динамической памятью

Это я не знаю. Но что до завершимости, то впринципе конечно можно, но для этого перебор надо осуществить, наверное? Т.е. это как то похоже на рекурсию. Может я чего недопонял опять.

так я предполагал, что Кок и сделает перебор. Иначе какой смысл в этой проверке завершимости?

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

Проблема останова для конечного автомата решается тривиально: если за количество шагов, равное количеству состояний, не завершилось, значит зациклилось.

Для абстрактного автомата со счётным количеством состояний решения за конечное время уже нет.

так я предполагал, что Кок и сделает перебор. Иначе какой смысл в этой проверке завершимости?

Так у тебя алгоритм f делает перебор. И алгоритм f1 проверящий твой алгоритм f тоже должен сделать тот же перебор. Где гарантия что f1 завершится? мы ж именно эту гарантию и ищем с помощью f1.

Иначе какой смысл в этой проверке завершимости?

Смысл в том что типизированная программа гарантировано не зависнет. И утверждения доказанные о ней будут верными, а не «верными если не зависнет». Это две разные как ты понимаешь степени уверенности в результате.

Я не знаю как ты это сделал. К дискуссии твои ссылки по моему вообще никакого отношения не имеют.

Но лично мне вторая ссылка возможно очень интересна по работе (но это читать надо, конечно).

Как бы то ни было, спасибо за наводку.

Автоматическое доказательство корректности программ с динамической памятью

Аннотация

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

Звучит очень интересно.

Так у тебя алгоритм f делает перебор.

Алгоритм f делает не перебор, в возможно бесконечное рекурсивное вычисление.

Алгоритм f1 запускает f на количество итераций, равное количеству состояний f. Если f не завершилось, указывает, что f может зациклиться. Если для всех состояний f завершилось, значит она всегда завершается.

Получается, нужно доказать, что граф переходов по машине состояний не содержит циклов.

Алгоритм f1 запускает f на количество итераций, равное количеству состояний f. Если f не завершилось, указывает, что f может зациклиться. Если для всех состояний f завершилось, значит она всегда завершается.

В коке на сколько мне известно такой проверки завершаемости нет как отдельного вида. Это ведь именно то что я сделал руками.

Кроме того, если реализовать, встанет вопрос запуска этого алгоритма перебора, а он время при компиляции занимал бы большое.

Ну да. Только руками у тебя функция стала всегда завершима.

Алгоритм f1 запускает f на количество итераций, равное количеству состояний f.

на каком аргументе? на переданном? А если на переданном завершается, а на другом каком-то не завершается?

На всех. У нас же конечный автомат. У него конечное число состояний.

Именно так.

На всех. У нас же конечный автомат. У него конечное число состояний.

я не пойму как ты хочешь проверять (хоть и пытаюсь).

Вот есть твоя функция от 1 аргумента.
У нас есть стомиллиард итераций. Я ведь верно понимаю что надо делать n * стомиллиард итераций чтобы проверить завершаемость (предполагаем n натуральное, органичено сверху)?

(ну либо мемоизацию какую то организовывать, но это уже детали процесса).

Давай пойдём с другой стороны: как ты хочешь это использовать?

А то я запутался.

Т.е. вот я дал пример кода. Теперь можно про него что то доказывать. Ну например, можно доказать что если fuel больше 100000000000, то функция выдаст не аварийный результат (для наглядности можно возвращять option вместо nat) и это будет доказательство что функция завершается не по fuel, а сама по себе.
(я конечно для этой конкретной не возьмусь доказывать, очевидно, ввиду сложности, но для средненькой какой нибудь это вполне реально сделать).

Обычно это нужно чтобы убедиться в корректности кода.

Потом её можно экспортировать в окамль и знать что у код завершиться без ошибок.

Или можно пройти какую нибудь сертификацию по высокому уровню доверия.

Короче вопрос целей.

Если система сможет автоматически доказать что функция завершается (для каких то случаев), это, конечно хорошо.

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

Может пример другой взять?

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

Ну да. Переборное доказательство либо время от O(N) до О(N^2) либо память O(N). Для данной функции можно проверить примерно за полчаса.

Обычно это нужно чтобы убедиться в корректности кода.

Вот есть функция. Код корректен, но система типов убедиться в этом не даёт. Переписываем функцию с дополнительным параметром просто для ублажения компилятора?

Потом её можно экспортировать в окамль и знать что у код завершиться без ошибок.

Только это будет другая функция. И если бы она возвращала не всегда единицу при успехе, а, например, решение какого-то дифура, то возврат 0 по таймауту явно не лучший выбор.

Ну да. Переборное доказательство либо время от O(N) до О(N^2) либо память O(N). Для данной функции можно проверить примерно за полчаса.

Для число дробилки это конечно не важно. Но Кок будет строить на сколько я понимаю пруф терм и это займёт ещё O(n) * m , m - константа, может 2-3, может 10,но не знаю точно (древовидная структура на сколько я себе представляю).

Ну пусть вдвое, я думаю меньше часа вряд ли получится.

Долговпто. Но может пример просто неудачный.

Только это будет другая функция. И если бы она возвращала не всегда единицу при успехе, а, например, решение какого-то дифура, то возврат 0 по таймауту явно не лучший выбор.

Вообще, конечно, правильно ты ставишь вопрос здесь. Но я часть деталей опускаю конечно. Функция которую ты написал - исходная. Которую я - модель. Встаёт вопрос соответствия модели и исходной функции. Этот вопрос называется функциональная корректность. Решается так для данного случая: пишем код на коке максимально похожий на то что нужно (чтобы на глаз можно было проверить соответствие математической спецификации) , отключаем проверки для исходной функции на коке. Компилятор примет определение. Далее доказываем соответствие модели и исходной функции. Далее работаем с моделью.

Только это будет другая функция. И если бы она возвращала не всегда единицу при успехе, а, например, решение какого-то дифура, то возврат 0 по таймауту явно не лучший выбор.

Ну в option завернуть.

Вот есть функция. Код корректен, но система типов убедиться в этом не даёт. Переписываем функцию с дополнительным параметром просто для ублажения компилятора?

Тут есть ещё такой момент... Ты клянешься что код корректен?

Эти ухищрения во всей их полноте нужны когда клятвы не достаточно. И не достаточно даже того что писал ну очень авторитетный программист. И даже если всё тесты проходит и год работало нормально - всё равно не достаточно.

Если прям таких требований нет, частью ухищрений можно пожертвовать.

В смысле я тоже могу поклясться что алгоритм тот же, хоть ты и утверждаешь что другой.

Но алгоритмы всё таки придётся адаптировать. Просто из с++ взять не выйдет.

Тут есть ещё такой момент… Ты клянешься что код корректен?

Ага. Я его проверил:

(declaim (optimize (speed 3) (safety 0)))

(defconstant +N+ 100000000000)

(defun f (k n)
  (declare (type (integer 0 100000000000) k n))
  (cond
    ((= k 1) 1)
    ((zerop n) 'fail)
    ((zerop (rem k 2)) (f (/ k 2) (1- n)))
    (t (f (1+ (* 3 k)) (1- n)))))

(defun test ()
  (dotimes (n +N+)
    (if (eq (f n +N+) 'fail) (return n)))
  (return-from test 0))

(format t "~a" (test))

Ну, так каждый говорит. Ошибки почему то всё таки случаются. Ну напиши как есть и отключи прверки для данной конкретной ф-ции, делов то... Но это исключение, конечно, но так тоже бывает.

Эти ухищрения во всей их полноте нужны когда клятвы не достаточно. И не достаточно даже того что писал ну очень авторитетный программист. И даже если всё тесты проходит и год работало нормально - всё равно не достаточно.

Так проблема в том, что Coq считает, что функция возможно бесконечна. Если же мы любую функцию будет преобразовывать в вычисления с ограниченным числом итераций, то реально зависающая функция будет проходить проверку и пойдёт в работу как проверенная. А потом на каких-то данных обрушит систему.

Но алгоритмы всё таки придётся адаптировать. Просто из с++ взять не выйдет.

В результате проверяем одну функцию, а используем другую. Как в анекдоте «пока я успел разработать только сферическую модель лошади в вакууме».

В этом смысле Typed Racket всё-таки проверяет именно то, что работает. И если проверка не доказана, впиливает динамический контракт.

Так проблема в том, что Coq считает, что функция возможно бесконечна. Если же мы любую функцию будет преобразовывать в вычисления с ограниченным числом итераций, то реально зависающая функция будет проходить проверку и пойдёт в работу как проверенная. А потом на каких-то данных обрушит систему.

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

Ну либо пишешь и доказываешь свойства того что написал. Тогда тоже не упадёт, ты ж доказывал о том что написал.

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

Я привёл пример функции f. Ты написал, что для такой доказать нельзя, надо заменить на другую. Фактически, доказывается только для аналога цикла for (в диапазоне или в коллекции).

Вот такое (Integrate), я так понимаю, тоже доказать нельзя будет:

double IntegrateH(double a, double b, double h, const std::function<double (double)> &f) {
    double sum = 0, k = h/2;
 
    for(double r = a; r < b; r += h)
    {
        sum += k*(f(r) + f(r+h));
    }
 
    return sum;
}

double Integrate(double a, double b, double eps, const std::function<double (double)> &f)
{
    double h = (b-a) / 10;
    double prev = IntegrateH(a, b, 2 * h, f), next = IntegrateH(a, b, h, f);
    
    while (fabs(prev - next)) > eps)
    {
        h  /= 2; prev = next; next = IntegrateH(a, b, h, f);
    }
    return next;
}

Я привёл пример функции f

Ты привёл пример функции для которой никто ничего доказать не сможет кроме как перебором, кроме некоторых частных случаев. (ну или вот я приводил, может верное доказательство, но тогда мужик один из первых и немногих кто вообще для этой функции что то более-менее доказал)

И попросил меня доказать для неё что-то. Смотри: доказательства на Коке почти не отличаются от доказательств в обычной математике. Есть некоторая специфика, конечно. Может быть, пожалуй, наиболее заментая - это большая подробность - там где в математике ты просто скажешь «ну понятно», в коке придётся всё таки дать доказательство.

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

Почему реализовывать перебор на Коке странно я тоже уже постарался вроде объяснить. Перебирать лучше на чём то что более подходит для перебора.

Фактически, доказывается только для аналога цикла for (в диапазоне или в коллекции).

Отнюдь. Но это довольно простой случай. И наверное наиболее частый (в некоторых вариациях).

Вот такое (Integrate), я так понимаю, тоже доказать нельзя будет:

Всё сводится к «обычной» математике. Если можешь доказать сходимость этого интрегрирования (формально, на математическом языке), на Коке тоже скорее всего всё получится. Правда доказательств для численных методов я лично никогда не касался.


После вышесказанного. При попытке доказать функциональную корректность у меня почему то получается что f в нуле виснет. Это я что то напутал или так и задумано?

Require Import Arith.
Require Import Bool.Bool.
Open Scope nat_scope.

Variable onehmlr : nat.
Axiom onehmrl_eq : onehmlr = 100000000000.

#[bypass_check(guard=yes)]
Fixpoint f(k : nat) : nat :=
  if k =? 1 then 1
  else
    if negb (k <=? onehmlr) then 0
    else
      if k mod 2 =? 0 then f (k/2)
      else f (3*k+1).


Fixpoint model_f (k fuel : nat) {struct fuel} : option nat :=
  match fuel with
  | O => None
  | S fuel =>
    if k =? 1 then Some 1
    else if negb (k <=? onehmlr) then Some 0
    else if k mod 2 =? 0 then model_f (k/2) fuel
    else model_f (3*k+1) fuel
  end.

Locate unint.
Opaque onehmlr.

Lemma leb0true n : 0 <=? n = true.
Proof.
  destruct n; reflexivity.
Qed.

Lemma eq_f_model_f k fuel : k < onehmlr -> fuel < onehmlr -> fuel > 0 -> model_f k fuel = Some (f k).
Proof.
  induction fuel.
  intros. inversion H1.
  intros. destruct k.
  unfold model_f. cbv fix. cbv beta. cbv iota.
  fold (model_f (3 * 0 + 1) fuel).
  fold (model_f (0 / 2) fuel).
  remember (0 =? 1) as eq.
  cbv in Heqeq. rewrite Heqeq.
  rewrite leb0true. simpl negb.
  cbv iota. remember (0 mod 2) as Emod.
  cbv in HeqEmod.
  rewrite HeqEmod.
  cbv [Nat.eqb].
Admitted.

При попытке доказать функциональную корректность у меня почему то получается что f в нуле виснет. Это я что то напутал или так и задумано?

а откуда там берется нуль-то? получиться в последовательности он не может. и не может быть началом последовательности.

а откуда там берется нуль-то? получиться в последовательности он не может. и не может быть началом последовательности.

Это я не знаю. Может натуральные там с единицы имелись ввиду? Если с нуля, то может быть на входе да и всё.

(declare (type (integer 0 100000000000) k n))
(return-from test 0)

у monk таки с нуля если я верно понимаю, но он вроде клялся что не виснет...

там натуральные больше нуля должны быть.

ни деление на два и умножение на три плюс один нуля не даст. монк там умничает слишком.

ни деление на два и умножение на три плюс один нуля не даст. монк там умничает слишком.

не важно на самом деле. но там что то не сходится, если он запускал программу с нуля и она у него не зависла, то скорее всего я что то не так понял.

если он запускал программу с нуля

зачем ее с нулем пускать-то? ее пускают для больших чисел.

зачем ее с нулем пускать-то? ее пускают для больших чисел.

я не знаю, он так написал.

либо я что то не так понял, либо он написал код который не запускал (подкорреткировал), либо ещё что то.