Узкое место прувера — сила правил, а не ненаписанные доказательства

Два независимых замера за один день пришли к одному выводу с разных сторон.

Замер первый — поиск доказательств. Написан оракул, который сам ищет доказательство. На контрольной задаче он снимает написанную рукой теорему и находит её заново: 11 из 11. На недоказанных утверждениях корпуса он нашёл ноль из двадцати. Причины разложены:

Замер второй — чтение условий если. См. reading-if-conditions-closed-zero-goals.

Вывод. Автоматизация не поможет, пока искать нечем: правил в ядре на день замера было три (сегодня одиннадцать — grep -c 'тотальная функция «Правило' flang/self/proof-kernel.flang). Расширять их наугад тоже перестало работать — оба заказа на новые правила оказались либо ложными, либо закрывающими ноль целей.

Чего этот вывод не значит. Он не значит, что недоказанное некому доказать руками: язык доказательств у flang есть (теорема со структурными шагами, 160 теорем в дереве, 53 в flang/stdlib). Узкое место здесь — сила ПОИСКА, а не отсутствие способа записать вывод.

Уточнение, которое пришло позже и переворачивает вывод. Замер цены доказательства показал, что дело не в числе правил, а в том, что правила не достают до встроенных типов: принципа индукции нет ни у списка, ни у строки, ни у числа. См. no-induction-for-builtin-types — это причина 13 случаев из 15.

Что делать вместо. Мерить, какие правила корпусу реально нужны, а не угадывать. Плюс набирать библиотеку лемм — см. coq-strength-is-in-its-lemmas.

Ценность отрицательного результата. Замер стоил своей цены не потому, что что-то улучшил, а потому что сэкономил работу, которую делали бы не туда — см. a-measured-zero-is-valuable.

Связано: unstatable-costs-more-than-unprovable, proof-search-must-trust-nothing