Узкое место переехало: принцип индукции появился, а цепляться ему не за что

Повторный замер цены доказательства (16 августа, origin/main = 17d6853) сдвинул число с 0 из 20 до 2 из 20 — и заодно показал, что причина отказа стала другой. Раньше не хватало принципа индукции у встроенных типов. Теперь принцип есть (у списка и у отрезка нат), а не хватает способа прицепить его к телу функции.

Ядро строит заключение посылки индукции только с ветвей разбор по переменной индукции. Отказ говорит это дословно:

тело функции «Есть в множестве» не разбирает «множество» на верхнем уровне,
поэтому заключение посылки индукции построить не из чего: ядро берёт «результат»
случая с ветви `разбор` по той же переменной, а не угадывает его

Чем подтверждено, со знаменателем. Тел вида «разбор по параметру» в flang/stdlib — 58 из 208 (benchmarks/proof-cost/tela.mjs на ветке work/zamer-tseny-2). Остальные 150: свёртка 45, условие 37, арифметика 21, вызов 18, встроенная форма 9, пусть 8, отображение и отбор 8, построение 3, применение 1. То есть 72 % библиотеки написано формами, к которым индукция ядра не цепляется, и на выборке из двадцати это дало 7 отказов из 18.

Что это меняет в порядке работ. Заметка no-induction-for-builtin-types заканчивалась порядком «сначала принцип для встроенных типов, потом чтение формы тела, потом новые правила». Первый пункт сделан; замер подтверждает, что второй теперь и есть самый отдачный, и уточняет его: у правила неотрицательности ход «читать начало и шаг свёртки как две посылки индукции» в ядре уже есть (flang/proof/SPEC.md, раздел 3б-секстэ), но живёт он внутри правила, а не в построении посылки. Перенести его туда — и семь функций из двадцати открываются одной работой.

Второе число того же замера, и оно важнее первого. Там, где ядро берёт цель, доказательство стоит одну строку постусловия против 18 строк примеров, и теорема не нужна вовсе. Теорем за замер написано 14, принято ядром 0: всё доказанное доказано без теоремы. Значит цена доказательства в flang перестала быть узким местом — узким местом стал охват.

Чем ограничено. Мерилось на голом main. Ветки work/indukciya-vstroennyh (индукция по признак) и work/zamknutaya-cel (вычисление замкнутой цели) в main не влиты и в замер не входили. Пробами проверено, чего на основании нет: индукции по признак и по строка нет, вычисления замкнутой цели нет.

Отдельно измерено и сказано против ожиданий: вычисление замкнутой цели на этой выборке закрывает 0 из 20. Все базы индукции в двадцатке либо уже закрыты подходящим примером, либо содержат свободное имя, которое вычислением не убрать. Отдача этой работы лежит в леммах (docs/lemmas-report.md), а не в обычных функциях библиотеки.

Дополнение 25 августа: свёртку в построение посылки перенесли, и граница у неё одна — переменная. Работа, названная выше самой отдачной, сделана: отказ теперь называет две формы тела вместо одной, и свёртка стоит рядом с разбором. Дословно, bootstrap/flang на main от 25 августа:

тело функции «Переход разрешён» не разбирает «откуда» на верхнем уровне и не
сворачивает «откуда» свёрткой, поэтому заключение посылки индукции построить не
из чего. Ядро читает «результат» случая из ДВУХ форм тела и ниоткуда больше: с
ветви `разбор` по той же переменной (тогда посылок столько, сколько
конструкторов) и с начала и шага `свёртка` по той же переменной (тогда посылок
две — начало и виток). Тело-вызов, тело-арифметика и тело-условие заключения
посылки не дают: угадывать «результат» ядро не станет

Граница, которую этот текст называет и которую легко проглядеть: свёртка считается только по САМОЙ переменной индукции, а не по списку, из неё вычисленному. Тело свёртка («Переходы из» от откуда) … индукции по откуда не даёт, хотя свёртка в нём есть: свёрнут не откуда, а результат вызова. То же и с проекцией поля — свёртка корзина.«позиции» … не даёт индукции по корзина.

Замер: в примере маркетплейса (examples/web/marketplace/) все четыре утверждения, оставшиеся сеткой, — ровно этой формы, и ни одно не открывается ни перезаписью охраны, ни двойником, ни теоремой. Открыть их можно только разгладив тело в разбор по переменной, а для «Переход разрешён» это значит завести вторую копию таблицы переходов рядом с «Переходы из» — то есть заплатить за доказательство тем самым расхождением двух копий, от которого теорема файла и стережёт. Правку отвергли по этому доводу, а не по цене.

Улики: docs/benchmark2/ (20 файлов с настоящими текстами отказов), отчёт docs/benchmark-proof-cost-2.md, журнал с секундомером benchmarks/proof-cost/journal.md.

Связано: proof-cost-0-of-20, no-induction-for-builtin-types, tautologies-close-for-free, proven-is-not-correct, condition-for-the-revolution