«Результат сортировки не убывает» — утверждение ЛОЖНОЕ, и ложно оно ровно на «не числе»

Самое желанное утверждение библиотеки о «Сортировать» из flang/stdlib/lists.flang доказать нельзя не потому, что ядру не хватает правил, а потому, что оно неверно. Контрпример найден прогоном, а не рассуждением:

«Сортировать» от [0 делить на 0, 1]        →  [не число, 1]
(элемент 1 в том списке) не больше (элемент 2)  →  нет

Разбор, почему так, и почему это свойство самой сортировки вставками, а не ошибки в ней. Тело «Вставить по порядку» идёт в ветвь иначе, когда значение не больше голова ЛОЖНО. При обычных числах это значит «значение больше головы», и порядок сохраняется. При «не числе» ложны ОБЕ стороны сравнения: не число не больше 1 ложно и 1 не больше не число тоже. Значит вставка ставит не число впереди, и пара соседей оказывается нарушенной.

Следствие для ядра, и оно важнее самого контрпримера. Правило «порядок соседних по построению» обязано отказать этому утверждению — и отказывает. Если бы правило читало ложную ветвь если фактом (то есть выводило «б не больше а» из «не (а не больше б)»), оно бы это утверждение ДОКАЗАЛО, то есть доказало бы ложь. Ровно поэтому ветвь иначе фактов не получает вовсе; закрывается она только противоречием — когда то же условие уже стоит среди допущений.

Подделка стоит в дереве: flang/test/fixtures/poddelka-sortirovka-ne-ubyvaet.flang (и рядом трёхстрочная poddelka-porjadok-sosednih.flang, которая бьёт в ту же ветвь напрямую). Сторож — node flang/scripts/poddelki-yadra.mjs.

Что вместо этого доказано о настоящей сортировке. Условное утверждение о её сердце — «Вставить по порядку»: «если приписать значение к списку и это не убывает, то и результат не убывает». Условие сказано ОДНИМ выражением, а не двумя: (приписать значение к элементы) не убывает означает разом «элементы упорядочены» и «значение не больше их головы», и на пустом списке истинно само собой — сторожить элемент 1 в пусто не приходится.

Связано: proven-is-not-correct, reading-if-conditions-closed-zero-goals, chto-nelzya-napisat-v-obespechivaet