Узкое место переехало четвёртый раз: теперь мешает индукция, которую негде объявить

После правила меры списка (right-edge-alone-closes-nothing) отвергнутых утверждений в flang/stdlib осталось 77 из 114. Разложение их по причинам показывает не новую слабость ядра, а дыру в путях доступа к тому, что у ядра уже есть.

Чем подтверждено. Прогон по всем flang/stdlib/*.flang тем же вызовом, каким спрашивает flang/src/proofterm.mjs (подстановка тела на место результат плюс свести с объявлениями подписи и определениями модуля), ветка work/pravyy-kray, коммит 6a6effd1:

Двенадцать «не меньше 0» — это ОДНА беда, и она не про правило. Все двенадцать — рекурсивные функции («Длина», «Высота», «Индекс», «Двоичный поиск», «Хеш числа», «Хеш ключа», «Позиция где», «Номер строки», «День недели», «В кольцо», «Считать символ», «Хеш строки»). Тело у каждой — разбор или если, и в ветви стоит рекурсивный вызов. Чтобы закрыть шаг, нужно ДОПУЩЕНИЕ о нём — то есть само доказываемое постусловие, применённое к части значения. Это и есть индукция, и принцип индукции у ядра давно есть и доказан (flang/proof/initial.mjs, 26 утверждений корпуса закрыты им).

Дыра в том, что зовут его только из написанной ТЕОРЕМЫ. А в flang/stdlib теорему писать нельзя: у восьми слов слоя доказательства нет продукции в flang/self/parser.flang, и теорема у библиотечной функции роняет побайтовую сверку самоприменения (proof-words-live-on-two-surfaces-of-four). Автоматический путь поОбъявленномуТипу индукции не делает вовсе.

Проверено вызовом, а не рассуждением. Оракул доказательств (flang/scripts/proof-search.mjs) на двух из этих двенадцати — lists.flang «длина списка неотрицательна» и numtree.flang «высота дерева неотрицательна» — находит теорему сам, и ядро её принимает. То есть доказательство существует, ядро его берёт, а вписать некуда. Проверка на это стоит исполняемой в flang/test/proof-search.test.mjs списком, а не нулём.

Отсюда следующий заказ, числом. Дешевле и полезнее всего — не новое правило, а автоматическая индукция по разбору на пути объявления: там, где тело разбирает параметр квантора и зовёт себя на части, ядро вправе взять своё же постусловие допущением. Это закрыло бы 12 из 77 без единого нового слова поверхности и без единой новой аксиомы — принцип уже написан и уже стережётся.

Второй по величине кусок — 26 целей «равно», и он другой природы: тождество сличает стороны СИНТАКСИЧЕСКИ после нормализации, а нужно равенство длин свёртки и списка (длина(свёртка …) равно длина(L)). Это симметричный близнец уже сделанного правила роста («растёт не быстрее» → «растёт ровно на один»), и он тоже теорема, а не аксиома. Оценка — 6 целей из 26; остальные 20 говорят о значениях, а не о длинах.

Чем ограничено. Числа сняты на flang/stdlib (114 утверждений). По всему корпусу открытых обязательств 111, и разложение там другое: библиотека — самая «длинная» его часть.

Связано: right-edge-alone-closes-nothing, bottleneck-moved-to-claim-shape, proof-words-live-on-two-surfaces-of-four, rule-one-does-not-read-calls-and-fields