Правило неотрицательности читает объявленное ИМЯ, но не вызов и не поле — и на этом обрывается цепочка лемм

Правило «неотрицательность по построению» (flang/proof/reduce.mjs) закрывает цель X не меньше 0, когда X собран из: литерала не меньше нуля, терма с допущением, имени, объявленного типом с дном (нат, вес), встроенной формы с объявленным от нуля результатом (длина, код символа), их суммы, выбора и свёртки.

Чего в этом списке нет, хотя выглядит так, будто есть:

• вызова функции, объявленной возвращает нат. «Номер записи» от пункт для правила не является неотрицательным, хотя её подпись это обещает;
• доступа к полю объекта, объявленному нат: пункт.«номер» — тоже нет.

Чем подтверждено. Ветка work/zhurnal-wal, три пробных модуля. Функция «Наибольший номер», написанная свёрткой если («Номер пункта» от пункт) больше набрано то («Номер пункта» от пункт) иначе набрано, с теоремой по свёртке отвергается:

FLANG_PROOF_INDUCTION_STEP: шаг «шаг свёртки» не сведён к допущениям
на части «набрано»: неотрицательность по построению не проходит:
выражение случая собрано не только из неотрицательного

и это при том, что «Номер пункта» объявлена возвращает нат и имеет собственное постусловие «номер не отрицателен». Обход через по свойству «номер не отрицателен» вместо по предположению тоже отвергается (FLANG_PROOF_STEP): сличение по вызову даёт факт о вызове, но соединить его с допущением индукции в одном шаге нечем.

Почему это важнее, чем выглядит. Ровно здесь обрывается то, чем сильны Coq и Isabelle: доказанное один раз работает дальше (coq-strength-is-in-its-lemmas). Лемма о вызываемой функции у нас есть — и не доезжает до вызывающей, потому что правило не умеет прочесть вызов как неотрицательный. Пока это так, цепочка лемм длиной два не собирается, и каждое утверждение доказывается с нуля или не доказывается вовсе.

Числом, на живом модуле. Журнал упреждающей записи: 12 утверждений высказано, 1 закрыто ядром, 11 посчитано на сетке примеров, на веру 0. Единственное закрытое — длина итог.«записи» не меньше 0, и закрыто оно потому, что снаружи стоит встроенная длина, а не потому, что поле объявлено списком. Убери длина — и оно тоже уйдёт в сетку.

Чем ограничено. Это не утверждение, что правило неверно: оно верно и закрыто списком нарочно (zero-axioms — расширять список значит расширять доверенное). Утверждение в другом: список закрыт по СИНТАКСИСУ выражения, а настоящий код написан вызовами и полями, и потому доля закрытого ядром на прикладном модуле оказывается около одной двенадцатой, а не около половины. Тот же по форме вывод уже записан про формы тела (bottleneck-moved-to-body-shape) и про формы утверждения (bottleneck-moved-to-claim-shape); это третий его случай, и признак у класса один — правило смотрит на то, КАК написано, а не на то, ЧТО объявлено.

Связано: bottleneck-moved-to-claim-shape, coq-strength-is-in-its-lemmas, nat-counter-in-a-record-is-unwritable, the-bottleneck-is-rule-strength, tautologies-close-for-free

Поправка (ветка work/po-vyzovu). Здесь стояло: «Лемма о вызываемой функции у нас есть — и не доезжает до вызывающей… цепочка лемм длиной два не собирается». Первая половина по-прежнему верна для правила неотрицательности: оно так и не читает вызов. Вторая половина перестала быть верной целиком: ядро научено брать постусловие вызванной функции как ФАКТ на месте вызова и подавать его сведению обычным допущением, так что цепочка длиной два собирается — но только когда постусловие вызванной уже ДОКАЗАНО ядром. Разбор условия, цена и оставшиеся узкие места — callee-postcondition-is-a-fact-only-after-it-is-proved.