Цели «равно» упёрлись в ПОРЯДОК СЛАГАЕМЫХ, а не в отсутствие индукции

Из 26 отвергнутых утверждений flang/stdlib вида «равно» два самых простых — «приписывание удлиняет список ровно на один» и «дописывание строки удлиняет список ровно на один» — не выводились не потому, что ядру нечем взяться за тело, а потому, что оно сличало 1 плюс длина(L) с длина(L) плюс 1 как разные термы. Тело у обеих функций одно действие, переписка длины у ядра уже была (мераПостроения читает добавить и приписать с 16 августа) — не хватало только перестановки двух соседей.

Это тот же класс, что bottleneck-moved-to-claim-shape называет «форма утверждения»: автор пишет «плюс один» справа, а ядро строит «один плюс» слева, и дальше сравнение синтаксическое. Ставить сюда индукцию было бы мимо цели.

Чем подтверждено. Ветка work/ravno на основании ствола f5f04f90, коммиты 24291c7d…953310cf. Прогон — прямым вызовом того же свести, каким ядро снимает постусловие без теоремы, по всем 26 целям; до правки закрывалось 0, после — 7. Ведомость node flang/scripts/proof-ledger.mjs: доказано ядром 213 → 220, сетка 101 → 94, объявлено-не-доказано 5 → 5, отвергнуто 0.

Разложение 26 целей по форме, замером, а не на глаз:

Правило-близнец, и что оно на самом деле несёт. Второй ход — «свёртка растёт РОВНО на один», близнец уже существовавшего «свёртка растёт не быстрее списка»: те же две посылки индукции по списку, но шаг несёт равенство, а не границу. Он закрыл 5 целей из 7. Ведомость называет их «тождеством», а не «индукцией» — слово здесь СЛАБЕЕ способа, и это обратная сторона того, что заметил сосед на автоматической индукции (там слово было сильнее способа). Считать надо оба случая отдельно: закрытых индукцией по свёртке 5, а в строке «из них индукцией» ведомости они не появятся.

Почему перестановка соседей — теорема, а не поблажка. равен языка есть Object.is, и на нём а плюс б и б плюс а совпадают на всех входах: точная сумма коммутативна, округление от порядка не зависит, −0 плюс 0 и 0 плюс −0 оба дают +0, +∞ плюс −∞ даёт не число с обеих сторон, а не число равно не число на Object.is ИСТИННО. Последнее и есть причина, по которой ход живёт у тождества: у порядка на не число ложны обе стороны, и там он не нужен вовсе.

Чем ограничено, и это граница жёсткая. Переставляются ДВА СОСЕДА ОДНОГО УЗЛА. Собрать цепочку а плюс б плюс в в мешок и отсортировать было бы ассоциативностью, а она в IEEE-754 ложна прямым числом: (0.1 плюс 0.1) плюс 0.6 даёт 0.8, 0.1 плюс (0.1 плюс 0.6) даёт 0.7999999999999999. Проверка на это стоит отдельной строкой в flang/test/proof-ravno.test.mjs и краснеет, если обход разрешить через скобки.

Второе ограничение: обход идёт по спине сложений ОТ КОРНЯ. «Ф» от (1 плюс х) против «Ф» от (х плюс 1) этим ходом не сличается.

Что стало новым узким местом. Из 19 незакрытых целей «равно» у 12 после нормализации в терме остаётся ВЫЗОВ ЧУЖОЙ ФУНКЦИИ, который ядро не разворачивает и постусловие которого на месте вызова не читает. У 7 из этих 12 цель закрылась бы прямо, возьми ядро постусловие вызываемого: «Сортировать» есть свёртка со шагом «Вставить по порядку», а у той написано «длина растёт ровно на один» — цепочки из двух постусловий ядро не строит. Это уже не форма цели, а отсутствие ХОДА ПО ВЫЗОВУ, и следующий замер стоит ставить туда.

Из оставшихся 7 одна цель ЛОЖНА и закрыта быть не может вовсе — см. string-reversal-keeps-length-is-false-on-a-lone-surrogate.

Связано: bottleneck-moved-to-claim-shape, claims-about-length-are-two-thirds-of-what-the-kernel-refuses, minus-zero-is-a-class, string-reversal-keeps-length-is-false-on-a-lone-surrogate