Принципа индукции нет ни у одного встроенного типа — вот настоящее узкое место

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

Индукция читается только с объявленного тип … вариант …. У списка, у строки, у числа, у признак принципа индукции нет. Отказ дословно:

FLANG_PROOF_INDUCTION_TYPE: индукция теоремы «…» идёт по «элементы»,
а это не объявленная сумма. Принцип индукции читается с объявления суммы —
у типа без объявления его взять неоткуда.

Почему это переворачивает картину. Раньше было записано, что узкое место — число правил в ядре (the-bottleneck-is-rule-strength). Замер уточняет: дело не в количестве правил, а в том, что правила не достают до типов, на которых написан настоящий код. Библиотека написана про списки и строки, а индукция умеет только про то, что автор объявил сам.

Что это открывает, в числах из отчёта. Индукция по списку сама по себе даёт 2 функции из двадцати — потому что мешает ещё и форма тела: у многих оно не разбор по параметру, с которого читается индукция. С разбором формы тела — до 7 из 20. Индукция по признак (два значения, конечное исчерпание) — ещё 1, и это тот же принцип, что уже работает у объявленных сумм, примерно 40 строк.

Порядок работ отсюда: сначала принцип индукции для встроенных типов, потом чтение формы тела, и только потом новые правила.

Поправка от 16 августа: половина этого уже неверна. На origin/main = 17d6853 принцип индукции есть у двух встроенных типов — у списка (из двух образцов, которыми язык исчерпывает его разбор) и у отрезка нат (из двух границ). Отказ FLANG_PROOF_INDUCTION_TYPE в прежнем виде больше не встречается; вместо него приходит FLANG_PROOF_INDUCTION_BRANCH — про форму тела. У строка и у признак принципа по-прежнему нет, и оба отказа сняты пробой, а не памятью (замеры 12, 19, 20 в docs/benchmark2/).

Порядок работ, записанный последней строкой, выдержал проверку: первый пункт сделан, второй («чтение формы тела») замером подтверждён как самый отдачный — bottleneck-moved-to-body-shape.

Перепроверено 18 августа на github/main = db43fb4a, ветка work/zhurnal-wal: у строка принципа по-прежнему нет, отказ дословно тот же и теперь называет все три места, откуда принцип читается:

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

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

Связано: proof-cost-0-of-20, the-bottleneck-is-rule-strength, coq-strength-is-in-its-lemmas, bottleneck-moved-to-body-shape, rule-one-does-not-read-calls-and-fields