Одно и то же действие, записанное вызовом и встроенной формой, доказывалось по-разному — и виновата была не сила правила, а МОМЕНТ переписки

Две записи одного тела. Обе рекурсивны по хвосту, обе удлиняют список ровно на один, утверждение при них дословно одно:

то «Приписать в начало» от голова и («Сам» от хвост)   доказано индукцией
то приписать голова к («Сам» от хвост)                 сетка

«Приписать в начало» — обёртка в одну строку над той же встроенной формой приписать. Разница в вердикте выглядела как разница в силе правила и ею не была.

Что происходило на самом деле

Ядро переписывало цель известными равенствами ОДИН РАЗ и ДО того, как развернуть меру списка («Развернуть длину звена» читает добавить, приписать и выписанный список и заменяет длина(…) равным выражением).

• С обёрткой переписка нужна ПЕРВОЙ: постусловие вызванной превращает длина(«Приписать в начало» от г и Y) в длина(Y) плюс 1, и лишь после этого в терме появляется длина(Y), к которому применимо допущение индукции. Повторный проход у переписки уже был, поэтому оба равенства успевали сработать.
• Со встроенной формой порядок обратный: длина(«Сам» от хвост) появляется в терме ТОЛЬКО ПОСЛЕ разворачивания меры (1 плюс длина(«Сам» от хвост)). К моменту единственной переписки этого терма в цели ещё не было, и допущение индукции до своего места не доживало.

То есть доказуемость зависела от того, вызовом или встроенной формой автор записал одно и то же действие.

Починка и её цена

«Переписанное после меры» в flang/self/proof-kernel.flang: переписать — развернуть меру — переписать — развернуть меру. Прежний ход целиком стоит первыми двумя шагами, третий и четвёртый дописаны сверху, поэтому потерять уже закрытое правка не может. Подана она обоим правилам, которые читают меру, — тождеству и порядку. Время flang check --proof на flang/stdlib/lists.flang: 2,06 с до, 2,00 с после (три замера, разброс меньше 3 %) — то есть не изменилось.

ЧЕГО ЭТО НЕ ДАЛО, И ЭТО ГЛАВНОЕ ЧИСЛО ЗАМЕТКИ

Ноль. В flang/stdlib не закрылось ни одного утверждения: доказано ядром 65 и до этой правки, и после (списки доказанных сверены diff-ом целиком). Причина видна прямо: библиотека НИГДЕ не пишет шаг встроенной формой в рекурсивной ветви — везде стоит вызов «Приписать в начало» или «Дописать строку». Расхождение было настоящим, но библиотека на него не наступала.

Держится правка одной программой — flang/test/fixtures/poddelka-svyortka-shagom.flang, функция «Дописать нуль встроенным»: сторож node flang/scripts/poddelki-yadra.mjs требует у её утверждения вердикта «доказано», и без правки оно «сетка».

Урок про оценку сверху. Гипотеза звучала как «встроенное приписать рвёт индукцию — дешёвая правка, снимающая часть левой свёртки». Первая половина верна, вторая нет: это соседний дефект, а не частный случай, и левой свёртки он не касается вовсе. Стену левой свёртки снимает другая правка, при другом правиле (см. left-fold-is-blocked-because-the-fold-rule-does-not-read-the-callee-postcondition).

Чем подтверждено. Ветка u/svyortka, основание ff8ad5d0. Пробы «А», «В» и «Г» в одном файле: «В» (обёртка) доказана, «А» и «Г» (встроенная форма, с если и без) — сетка; после правки все три доказаны. Замер библиотеки — node benchmarks/proof-cost/count-library.mjs.

Чем ограничено. Речь только про меру «длина» и про равенства. Сколько эта правка стоит на дереве целиком, меряет node flang/scripts/proof-ledger.mjs.

Связано: left-fold-is-blocked-because-the-fold-rule-does-not-read-the-callee-postcondition, equality-goals-hit-summand-order-not-missing-induction, callee-postcondition-is-a-fact-only-after-it-is-proved