Встроенное приписать в рекурсивной ветви разбора рвёт индукцию, а тот же шаг через функцию с доказанным постусловием — не рвёт

Разница выделена до одного слова. Две вставки в упорядоченный список, одно и то же утверждение (длина результат) равен ((длина элементы) плюс 1), одна и та же структурная рекурсия:

случай голова и хвост
  если значение не больше голова
    то приписать значение к элементы
    иначе приписать голова к («Вставить» от значение и хвост)      ⇒ СЕТКА

случай голова и хвост
  если значение не больше голова
    то «Приписать в начало» от значение и элементы
    иначе «Приписать в начало» от голова и («Вставить» от значение и хвост)  ⇒ ДОКАЗАНО индукцией

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

Мешает только ВТОРАЯ ветвь, та, где стоит рекурсивный вызов. Проверено подстановкой по одной: встроенная форма в первой ветви и функция во второй — доказано; функция в первой и встроенная во второй — сетка. То есть ядро умеет переписывать длина (приписать Э к С) (проба приписать 0 к элементы с тем же утверждением доказана сведением с телом), но не умеет сделать это ПОВЕРХ допущения индукции: под встроенной формой стоит рекурсивный вызов, длина которого известна только из допущения, и до него переписка не доходит.

Практический вывод, пока это не починено: если хотите индукцию по списку, шаг пишите вызовом функции с доказанным постусловием о длине, а не встроенной формой. Ровно так и написана «Вставить по порядку» в flang/stdlib/lists.flang — и она единственная в файле, чьё утверждение о длине ядро закрывает индукцией.

Стоит это дёшево и понятно: «Приписать в начало» — одна свёртка, её собственное постусловие ядро доказывает даром.

Чем подтверждено. Четыре пробы по одному файлу, bootstrap/flang 0.5.1, ветка u/steny-peremer, основание ff8ad5d0; вердикт из check … --proof, раздел «что высказано». Тексты вердиктов: «доказано индукцией по «список»: база 1 случай, шаг при допущении на частях (1 случай), правила сведения: тождество после переписки допущением; разбор цели по условию» против «сетка 1 значение».

Чем ограничено. Мерено только на приписать и только на цели о длине. Про добавить в рекурсивной ветви и про другие виды цели не мерено.

Связано: left-fold-gives-no-list-induction, callee-postcondition-is-a-fact-only-after-it-is-proved, an-induction-hypothesis-must-be-instantiated-at-the-call-site, a-hand-copied-wall-list-goes-stale-in-silence