Цель-конъюнкция ядру не по зубам, но стоит это шести утверждений, а не шестидесяти четырёх

Утверждение вида A и притом B ядро не доказывает НИКОГДА — даже когда обе половины оно доказывает порознь. Механизм точный: и притом разбирается в если A то B иначе нет, и ход «разбор цели по условию» делит цель по значению A. Половина «условие ложно» при этом становится литералом нет, и ядро говорит о ней дословно:

разбор цели по условию не прошёл: половина «условие ложно» не сведена: она стала литералом «нет», то есть ЛОЖНА — доказывать нечего, надо чинить

Ход прав по букве: если A ложно, то и A и притом B ложно. Неверно то, что конъюнкция вообще попадает в этот ход: её надо доказывать двумя посылками, а не разбирать по случаям первого конъюнкта. Отдельного правила у ядра нет.

Чем подтверждено. Проба из двух строк: у функции с телом отобразить элементы как эл → эл утверждение ((длина результат) равен (длина элементы)) и притом ((длина результат) не меньше 0) получает вердикт «сетка», а (длина результат) равен (длина элементы) тем же прогоном — «доказано». Дословный отказ снят предусловием-конъюнкцией ((длина сп) не меньше 0) и притом ((длина сп) не меньше 0), у которой обе половины доказуемы. Ветка u/dokazat-bibl, компилятор bootstrap/flang 0.5.1.

Сколько это стоит библиотеке: шесть, а не шестьдесят четыре

Соблазн прочитать это как «правило конъюнкции закроет 64 утверждения» — 64 цели такой формы в flang/stdlib. Замер говорит другое. Механическое разъятие ВСЕХ конъюнкций (прогон по двадцати модулям, каждое A и притом B заменено двумя именованными утверждениями) добавляет шесть доказанных: strlists три, utf8 два, strings одно. У остальных недоказуемы и половины — ровно по тем же причинам, по каким недоказуемо целое.

То есть правило конъюнкции в ядре купило бы почти ничего: узкое место не в нём.

Чем ограничено. Замер о flang/stdlib; в корпусе спек fspec/spec конъюнкций почти нет, и там число было бы другим.

Связано: substantive-claims-are-provable-when-you-pick-the-shape, the-kernel-has-no-not-less-rule-but-not-greater-proves

Поправка 24 августа: конъюнкцию ядро теперь берёт — а расщеплять её всё равно стоит, и по другой причине

Заголовок этой заметки устарел. В ядре появился ход «КОНЪЮНКЦИЯ: ПОЛОВИНА „УСЛОВИЕ ЛОЖНО“ ЕСТЬ ЛОЖЬ» (flang/self/proof-kernel.flang, «Вторая по форме»): вместо недоказуемой лжи он спрашивает само условие. Целей-конъюнкций, доказанных как есть, в flang/self/bounded.flang на стволе три, среди них трёхчленная «шаг хранит витки, рекурсии и состояние, как их дали».

Расщеплять их всё равно выгодно, но выгода не там, где искали. Составное постусловие ВЫЗВАННОЙ функции наверх целиком не поднимается: «Дописать факт вызванного» кладёт вызывающему один факт, а не его половины. Расщепив постусловие «Шагом» на три обещания, вызывающие получили три отдельных факта:

до расщепления   «Шагом» доказано (1 обещание),  вызывающие — 0
после            «Шагом» доказано (3 обещания),  вызывающие — +8

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

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

Чем подтверждено. Ветка b/self-bounded над 462a24cf, парные прогоны flang check flang/self/bounded.flang --proof --json (1 мин 55 с — 2 мин 2 с).