Свёртка в flang левая, поэтому индукцию по списку к ней прицепить нельзя — и это свойство свёртки, а не пробел ядра

Тело свёртка с начиная с И как а и э → Т — самая частая форма настоящего кода после разбор (38 функций flang/stdlib из 208 сворачивают прямо параметр). Заманчиво доказывать о ней индукцией по списку. Не выйдет, и причина арифметическая, а не инженерная.

У левой свёртки два определяющих уравнения:

свёртка пусто   начиная с И как а и э → Т  =  И
свёртка (г : х) начиная с И как а и э → Т  =  свёртка х начиная с Т[а:=И, э:=г] …

Второе меняет начало, а не только список. Значит допущение индукции по списку говорит о «свёртке хвоста при том же начале», а заключение — о «свёртке хвоста при ДРУГОМ начале». Это разные термы, и синтаксическое сличение их не сведёт никогда. Свести их можно только обобщив утверждение по накопителю — а это поиск инварианта, то есть ровно то, чего у ядра нет и не будет.

Чем подтверждено. Ветка work/indukciya-vstroennyh содержит оба уравнения как переписки — и этого не хватает: развернуть свёртку они позволяют, сойтись допущению с заключением нет. Проверено на ветке work/formy-tela замером docs/body-shapes.md.

Что работает вместо этого. Принцип по числу ВИТКОВ: P(И) и «для любых а и э из P(а) следует P(Т)» дают P(свёртка …), потому что витков ровно столько, сколько ячеек в списке (длина снимается один раз, до первого витка). Он сделан (flang/proof/initial.mjs, принципПоСвёртке), и им доказано «высота построенного дерева неотрицательна» — одно из двух новых утверждений замера.

Чем ограничен. Инвариантом накопителя доказывается только то, что говорит о результате. Утверждение, связывающее результат со входом («длина результата равна длине входа плюс один»), им не берётся: при пустом списке оно о начале ложно. Из шести функций замера, написанных свёрткой, такую форму имеют пять — то есть форма тела перестала быть помехой, а форма УТВЕРЖДЕНИЯ ею стала.

Связано: bottleneck-moved-to-claim-shape, no-induction-for-builtin-types, two-cores-do-not-merge-as-text, coq-strength-is-in-its-lemmas

Поправка (20 августа, ветка vypusk/dvadcat). Заметка верна про ИНДУКЦИЮ и неверно читалась как «про левую свёртку доказать связь результата со списком нельзя». Можно, и без всякой индукции: утверждение «длина результата равна длине входа плюс один» закрывается СИНТАКСИЧЕСКИМ правилом «свёртка, растущая ровно на один» — начало обязано совпасть с основанием правой стороны, шаг прибавлять к мере накопителя ровно единицу, а список свёртки быть тем же, чья длина стоит справа. Замер двадцати функций считал эту форму главной своей помехой и называл её «вопросом, на который у проекта нет ответа даже в теории»; на деле её имели четыре файла (06, 07, 09, 18), и все четыре закрыты. Обобщения по накопителю и поиска инварианта для этого не понадобилось — ровно потому, что правило не обобщает, а сличает.