Охрана меняет истинность и не меняет доказуемость: стена стоит до неё

Утверждение «ключ есть в дереве ровно тогда, когда он среди ключей» было ложью — на Узел("а", слева = Узел("б")) поиск отвечает «нет», а обход ключей отдаёт ["б", "а"]. Записанное охраной

обеспечивает «в дереве поиска ключ есть ровно тогда, когда он среди ключей»
  если («Это дерево поиска» от дерево) то (результат равен ((«Ключи дерева» от дерево) содержит искомый)) иначе да

оно ложью быть перестаёт. Посчитано вычислителем на том же значении: неохраняемое даёт false, охраняемое — true, а сама охрана не пуста (нет на кривом дереве, да на настоящем). Правки языка для этого не нужно — предикат стоил 29 строк в flang/stdlib/tree.flang.

Доказуемости это не прибавляет ни на шаг, и это измерено. То же утверждение БЕЗ охраны — то есть ЛОЖНОЕ — отвергается ядром в тех же двух местах и теми же словами, что и охраняемое (истинное):

шаг «Узел» не сведён к допущениям на частях «л», «п»: тождество после переписки
допущением не проходит: после переписки допущениями стороны равенства остались
разными термами. Ядро сличает синтаксически и равенства вычислений не решает.

Вывод, который стоит запомнить: одинаковый отказ на истинном и на ложном утверждении означает, что отказ не про них. Стена стоит раньше охраны.

Чем охрана мешала ядру — три упора, каждый пробой:

Первые два сняты. Разбор цели по условию теперь кладёт условие в допущения — но только в половину «условие истинно»: из ложности условия не следует ничего, и ловушка не число тут ни при чём (перевода отрицания нет вовсе). Конъюнкция расщепляется — язык пишет A и притом B узлом если A то B иначе нет, и из истинности целого следует истинность обеих половин разбором ОДНОГО вычисления. Дизъюнкция (если A то да иначе B) не расщепляется, и на это стоит подделка.

Замеренный ноль: на библиотеке правила не закрывают ничего. 455 утверждений flang/stdlib, доказано 62 до и 62 после, файл в файл. Охраняемых утверждений в stdlib 55 — и ни одному из них конъюнкт охраны не нужен. Ноль тут ценен: правило работает (лемма «часть дерева поиска — тоже дерево поиска», прежде отвергавшаяся, доказана индукцией), но сегодняшняя библиотека упирается не в него.

Что осталось между этой леммой и утверждением о дереве поиска — названо, а не оценено: разбор случая по условию, стоящему ВНУТРИ равенства (искомый равен кл); теория содержит над списком, собранным свёрткой (keys(л) ++ [кл] ++ keys(п)); и порядковые факты о «Строка раньше» (транзитивность и трихотомия), без которых «в правом поддереве искомого нет» не вывести. Это не одно правило, а три разных, и два последних — библиотека лемм, а не правило ядра.

Цена охраны при работе растёт, и это довод в соседнюю сторону. Дерево из 10 ключей 2,13 → 2,92 с (1,37×), из 20 — 16,39 → 31,29 (1,91×), из 40 — 104,72 → 382,96 (3,66×): охрана считается на каждом возврате охраняемой функции, а стоит она обхода всего дерева. Для сравнения, отложенная заплата «инвариант у типа» (требует «Проверка» строкой в теле типа; работает, проверена, лежит в /srv/tmp/u-invariant-rabota/forma-tipa/) на том же замере даёт 1,31× / 1,31× / 1,36× — цена плоская, потому что проверка стоит при ПОСТРОЕНИИ, а не при каждом утверждении. Цена самой заплаты: три файла компилятора (parser.flang, link.flang, bootstrap/compiler.flang), ноль правок у восьми целей печати, вычислителя, слоя типов и анализа завершаемости.

Чем подтверждено. Ветка u/invariant, коммит поверх ff8ad5d0. Подделки — poddelka-lozhnaya-polovina.flang и poddelka-razdvoenie-diz.flang, обе ложны вычислением и обе остались недоказанными; node flang/scripts/poddelki-yadra.mjs — 10 файлов, аксиом ноль, нарушений 0. flang test flang/stdlib — 1219 из 1219. sh scripts/raskrutka.sh --check — совпадает с печатью, 7 файлов, 24 489 999 байт.

Связано: the-type-holds-no-invariant-so-obvious-claims-about-a-search-tree-are-false, reading-if-conditions-closed-zero-goals, a-measured-zero-is-valuable, unstatable-costs-more-than-unprovable