Классика Coq и Lean: что из неё берёт наше ядро

Эта страница — не обзор Coq и не пересказ Mathlib. Это замер: семьдесят пять классических лемм, выписанные дословно из исходников Coq и Lean, переписанные на flang настоящими функциями с обещаниями и прогнанные нашим ядром. У каждой леммы стоит вердикт, снятый прогоном, и у каждой недоказанной названа причина.

Отрицательный результат тут ценнее положительного. Раздел, где написано «доказано семьдесят пять из семидесяти пяти», читатель опроверг бы первым же прогоном и больше нам не поверил бы.

Итог одной строкой

flang/stdlib/math-classics.flang
  утверждений 67: доказано 29 (из них без теоремы 29, объявленным типом 12), сетка 38, объявлено, не доказано 0

flang/stdlib/math-classics-lists.flang
  утверждений 37: доказано 16 (из них без теоремы 16), сетка 21, объявлено, не доказано 0

Всего 104 утверждения, доказано 45. Из семидесяти пяти классических лемм ядро берёт двадцать пять целиком; сорок девять остаются сеткой, и каждой названа причина ниже; ещё одну — завершение алгоритма Евклида — на flang записать нечем вовсе.

Ни одной аксиомы в этих файлах нет: столбец «принято на веру» в обоих отчётах пуст (принято на веру: ничего).

Что изменилось с прошлого замера. Было 73 утверждения и 29 доказанных, лемм сорок семь, взятых целиком тринадцать. Прибавку дали не переписи старых обещаний, а новые леммы и две измеренные границы правил ядра: монотонность сложения берётся при прибавке-литерале и не берётся при прибавке-терме (ровно как граница остатка), а границы минимума и максимума берутся охраной, списанной из тела дословно.

Откуда взяты имена

Имена лемм выписаны из исходников, а не из памяти. Каждое, что стоит в таблице, найдено в выкачанном файле; чего найти не удалось — в таблице стоит прочерк.

Две подробности, которые сберегут читателю время. Первая: у Coq стандартная библиотека с master уехала в отдельный репозиторий (rocq-prover/stdlib), и по пути coq/coq/master/theories/… сегодня приходит 404 — файлы выше брались по тегу V8.19.2. Вторая: Mathlib/Data/Nat/Defs.lean больше не существует, почти вся классика про Nat переехала в ядро Lean 4 (src/Init/Data/Nat/…), и в Mathlib остались только надстройки.

Три имени подтверждены применением, а не объявлением, и это надо сказать прямо. Nat.le_add_r, Nat.le_0_l и Nat.sub_add в выкачанных файлах вызываются (theories/Arith/PeanoNat.v:411, theories/Lists/List.v:506 и :1701, theories/Numbers/Natural/Abstract/NOrder.v:25, theories/Numbers/Natural/Abstract/NParity.v:41), а объявлены в файлах, которые в этот замер не выкачивались (NBase.v, NSub.v). Имя существует, строка объявления не проверена.

Как читать вердикт

Ровно четыре исхода, и различать их обязательно:

В этих двух файлах исходов встретилось два: доказано и сетка.

Как переводился nat

У Coq и Lean все леммы ниже сформулированы над nat — точным типом без «не числа», без бесконечностей и без дробей. число в flang — это IEEE-754, и над ним половина классики попросту ложна:

5 не больше (5 плюс (0 минус 1))                    →  false
(9007199254740994 минус 1) плюс 1                   →  9007199254740992
(0 делить на 0) не больше (0 делить на 0)           →  false

Поэтому всюду, где у них nat, у нас стоит нат — точный отрезок [0, 2⁵³−1]. Это не косметика, а условие честности перевода; тот же довод записан в flang/test/fixtures/poddelka-order-arithmetic.flang.

Замер попутно, стоивший одного прогона. В исходниках компилятора и в flang/SPEC.md тот же тип называется неотрицательное, и flang/stdlib/strlists.flang пользуется этим именем. В напечатанном двоичном такого имени нет: flang check на стоковом strlists.flang отвечает FLANG_UNKNOWN_NAME … неизвестный тип «неотрицательное», а само ядро в тексте своих отказов зовёт этот тип нат. Двоичный отстаёт от исходников до перепечатки семени; писать надо нат.

Таблица: арифметика

Файл — flang/stdlib/math-classics.flang, 45 функций, 67 утверждений. Номер в скобках — строка в выкачанном файле.

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

Таблица: списки

Файл — flang/stdlib/math-classics-lists.flang, 25 функций, 37 утверждений. Номер в скобках — строка в theories/Lists/List.v тега V8.19.2 либо в названном файле Lean.

Двадцать одна лемма, взято целиком шесть.

Ослабления, названные вслух. У девяти лемм, где полное равенство списков не взялось, рядом стоит то же утверждение только про длину, и восемь из девяти доказаны. Это не замена лемме — это слабее её, и в таблице вердикт стоит у полной формы, а не у ослабленной.

Почему не берётся: причины поимённо

Сорок девять недоказанных лемм распадаются на восемь названных причин, и ни одна из них не «ядро слабое вообще».

1. Ассоциативность и дистрибутивность: ядро сличает СИНТАКСИЧЕСКИ

Отказ ядра назван дословно, и это не догадка:

тождество после переписки допущением не проходит: после переписки допущениями стороны равенства остались разными термами. Ядро сличает синтаксически и равенства вычислений не решает. Сличение при этом читает плюс и умножить С ТОЧНОСТЬЮ ДО ПОРЯДКА СОСЕДЕЙ (перестановка двух операндов ОДНОГО узла — теорема IEEE-754; переставлять через скобки нельзя, ассоциативность в IEEE-754 ложна, и ядро этого не делает).

Отсюда ровно то, что мы и намерили: коммутативность берётся, ассоциативность — нет, и обе для сложения и для умножения. Это не пробел, а честность: над плавающими ассоциативность действительно ложна, и правило, которое взяло бы её, доказывало бы ложь.

Тем же одним правилом объясняются: Nat.add_assoc, Nat.mul_assoc, Nat.mul_add_distr_l, Nat.mul_add_distr_r — четыре леммы.

2. Нейтральный элемент и поглощение: а плюс 0 и а — разные термы

Nat.add_0_r, Nat.add_0_l, Nat.mul_1_r, Nat.mul_1_l, Nat.mul_0_r, Nat.sub_0_r, Nat.div_1_r — семь лемм, и все семь упираются в то же синтаксическое сличение: подстановка тела даёт (а плюс 0) равен а, а это два разных дерева. Правила «свернуть нейтральный элемент» у ядра на голом теле нет.

А вот на пути через обещание вызванного оно есть — и только с одной стороны. Это объясняет асимметрию, которая в прошлой редакции этой страницы стояла неразгаданной: List.app_nil_l («склейка с пустым СЛЕВА не меняет длину») — доказано, а зеркальная List.app_nil_r — сетка. Проба, снятая прогоном:

«Склеить с пустым справа», тело «Склеить» от элементы и пустой список:
  (длина результат) равен ((длина элементы) плюс (длина пустой список))  — ДОКАЗАНО
  (длина результат) равен ((длина элементы) плюс 0)                      — ДОКАЗАНО
  (длина результат) равен (длина элементы)                               — сетка

«Склеить с пустым слева», тело «Склеить» от пустой список и элементы:
  (длина результат) равен (0 плюс (длина элементы))                      — ДОКАЗАНО
  (длина результат) равен (длина элементы)                               — ДОКАЗАНО

Составная форма берётся с обеих сторон. Разница ровно одна: ведущий ноль ядро свёртывает, замыкающий — нет. Куда именно оно при этом ходит, из отказа не видно; измеримо только это.

Замер, который стоит знать рядом: в файле списков обещание «удвоение есть сумма с самим собой» при теле х умножить на 2 — тоже сетка, а «прибавление единицы есть сумма с единицей» при теле х плюс 1 — доказано. Разница ровно в том, совпало ли дерево цели с деревом тела.

3. Неравенства над термом: правило есть под ноль, под тип и под ЛИТЕРАЛ

Nat.le_add_r (прибавка-терм), Nat.le_trans, Nat.le_antisymm, Nat.le_ge_cases, Nat.add_cancel_l, Nat.div_mod_eq, Nat.sub_add, Nat.add_le_add_left, Nat.mod_bound_pos (делитель-терм) — девять лемм.

Граница прохо́дит по виду прибавки, и это новый замер. Одна и та же лемма Nat.le_add_r даёт два разных вердикта:

«Сумма», тело а плюс б, где б: нат — прибавка ТЕРМ:
  а не больше результат   — сетка
  б не больше результат   — сетка

«Следующее»,       тело а плюс 1  — прибавка ЛИТЕРАЛ:  а не больше результат — ДОКАЗАНО
«Прибавить десять», тело а плюс 10 — прибавка ЛИТЕРАЛ:  а не больше результат — ДОКАЗАНО

Вердикт у обоих литеральных — «доказано по объявленным типам аргументов: цель сведена правилом „порядок по построению“». То есть отрезок, который даёт тип нат, ядро читает, но только когда второе слагаемое — записанное число. Это та же разделительная линия, что и у остатка (Nat.mod_bound_pos): не «трудность» леммы, а вид второго довода.

Что берётся даром: Nat.le_refl и Nat.le_0_l — оба вердикта пришли с той же формулировкой про объявленные типы. А сложить два допущения а не больше б и б не больше в в третье ядро не умеет: переписка у него одноцелевая.

Границы минимума и максимума взялись, и взялись охраной. Четыре обещания — Nat.min_le_left, Nat.min_le_right, Nat.le_max_left, Nat.le_max_right — записаны охраной, списанной из тела дословно:

обеспечивает «меньшее из двух не больше первого»
  если (а не больше б) то (результат не больше а) иначе да     → ДОКАЗАНО

Под охраной тело сводится к а, цель — к рефлексивности, а её тип нат даёт. Приём 1 из «Какие обещания ядро берёт» работает и на цели не больше, а не только на цели-равенстве.

Запись-двойник тут не помогает, и это замерено трижды. Для Nat.le_trans, Nat.le_antisymm и Nat.add_le_add_left в файл дописывался двойник не (А) или (Б) (приём 6). Все три остались сеткой: знаменатель вырос, числитель — нет. Двойник у Nat.add_le_add_left откачен, у первых двух оставлен, чтобы читатель видел обе записи. Тем же нулём кончилось разложение Nat.le_total по трём исходам сравнения (приём 11) — три обещания, ноль прибавки, откачено.

Nat.sub_add — случай особый: над IEEE-754 закон ложен, контрпример (9007199254740994 минус 1) плюс 1 = 9007199254740992. Над нат он верен, но правила, которое отличало бы точную сетку целых от остальных чисел в вычитании, у ядра нет и, судя по врезке в flang/self/proof-kernel.flang, не будет («вычитания в этом списке нет и не будет»).

4. Арифметика остатков: чётность и делимость

Nat.mod_1_r (само равенство), Nat.mod_same, Nat.divide_refl, Nat.Even_or_Odd, Nat.even_add, Nat.even_mul, Nat.sub_self — семь лемм. Все просят рассуждения про остаток: «остаток по два есть ноль или один», «сумма двух чисел с нулевым остатком имеет нулевой остаток». Правил такого рода у ядра нет — есть только границы остатка, и только при делителе-литерале.

Отдельный замер, который стоит прочесть. У Nat.mod_1_r обе границы доказаны, а равенство — нет:

«Остаток по единице», тело н остаток от 1:
  результат не больше 0   — ДОКАЗАНО, правило «ограниченность точным потолком по построению»
  0 не больше результат   — ДОКАЗАНО, правило «порядок по построению»
  результат равен 0       — сетка

Два своих доказанных неравенства ядро не склеивает в равенство. Это не особенность остатка, это общее свойство: складывать два постусловия одного вызова оно не умеет (то же сказано в docs/site/kak-dokazat.ru.md), и здесь видно, что и два постусловия одной цели тоже.

Что при этом взялось: Nat.even_spec и Nat.odd_spec — «чётность есть нулевой остаток по два» и «нечётность есть единичный». Обе доказаны правилом «тождество после переписки допущением», потому что это буквально определения: дерево цели совпало с деревом тела.

5. Рекурсия по остатку: НОД

Nat.gcd_comm, Nat.gcd_divide_l, Nat.gcd_divide_r, Nat.gcd_self, Nat.gcd_1_r — пять лемм, и у всех причина одна: «НОД по Евклиду» — единственная не тотальная функция в обоих файлах (без доказанного завершения: «НОД по Евклиду»). Пара (a, b) строго убывает по второму доводу, но шаг у неё — остаток, а не постоянная разность, и анализ убывания у flang такого шага не читает.

Что при этом взялось — обе ветви рекуррентного уравнения, и обе охраной, списанной из тела дословно:

обеспечивает «НОД с нулём есть само число»
  если второе равен 0 то (результат равен первое) иначе да                  → ДОКАЗАНО
обеспечивает «НОД сводится к остатку»
  если не (второе равен 0)
    то (результат равен («НОД по Евклиду» от второе и (первое остаток от второе)))
    иначе да                                                                → ДОКАЗАНО

Это Nat.gcd_zero_right и Nat.gcd_rec — то есть само определение Евклида доказано как пара обещаний, хотя ни одно следствие из него не берётся. Правило у обоих одно: «разбор цели по условию».

И отдельно: обещания «Евклид завершается» на flang записать нечем. Убывание меры — свойство определения, а не постусловие результата; у Coq это Fix/well-founded рекурсия, у Lean — decreasing_by, а у нас признак тотальная, который здесь просто не ставится.

6. Переставимость минимума и максимума

Nat.min_comm, Nat.max_comm — две леммы. Цель у них — равенство результата вызову той же функции с переставленными доводами, а внутрь вызванной функции ядро не заглядывает: оно берёт только её обещания, а обещания «Меньшего из двух» записаны под охраной и о перестановке не говорят ничего. Это тот же обрыв цепочки, что описан приёмом 7 в «Какие обещания ядро берёт».

7. Свёртка: стена проходит по её границе

List.app_nil_r, List.app_nil_l, List.app_assoc, List.app_comm_cons, List.rev_involutive, List.rev_app_distr, List.map_app, List.map_map, List.map_id, List.fold_left_app, List.fold_right_app — одиннадцать лемм, и это самая крупная группа.

Тела «Склеить» и «Обратить» — свёртки. Принцип свёртки у ядра есть, и это перемерено соседней работой (задача 0050, коммит b96826d7): он читается, когда свёртка идёт по самому доводу, названному именем, и на верхнем уровне тела, а у шага стоит безохранное обещание о росте накопителя ровно на один. Обе наши свёртки этим условиям отвечают, шаг вынесен и такое обещание у него есть — и принцип всё равно не сработал ни разу: в отчёте обоих прогонов, с вынесенным шагом и с лямбдой, стоит доказано 16 (из них без теоремы 16) и доказано 15 (из них без теоремы 15), ни одного «из них индукцией».

Длину свёртки ядро считает другим правилом — «тождество после переписки допущением», — и его хватает на все обещания про меру и не хватает ни на одно обещание про содержимое. Правила «свёртка над пустым списком есть основа» у ядра по-прежнему нет: оба обещания «на пустом списке свёртка есть само основание» (левая и правая) остались сеткой.

Приём 8 проверен и дал минус один — это надо сказать прямо. Шаг свёртки «Склеить» вынесен в обычную функцию «Шаг склейки», и на ней обещание (длина результат) равен ((длина акк) плюс 1) (List.last_length) доказано. Но когда сама свёртка стала звать вынесенный шаг вместо лямбды, файл дал 16 → 15 доказанных: пропало List.app_nil_l в ослаблении до длины. Правка откачена, «Шаг склейки» оставлен рядом со свёрткой. Предупреждение из методички («вынос шага может уронить доказательство, которое стояло») подтверждено числом.

Что при этом взялось, и взялось у всех: длина. «длина склейки есть сумма длин», «обращение сохраняет длину», «отображение сохраняет длину», «приписывание удлиняет список ровно на один», «у пустого списка длина ноль» — доказаны. То есть про списки ядро умеет считать, но не умеет отождествлять.

8. Вхождение и доступ по номеру

List.in_app_iff, List.in_eq, List.in_cons, List.nth_In — четыре леммы, и это та самая дыра, названная третьей в списке известных: «элемент N в списке». Моста между содержит и элемент … в … у ядра нет ни в одну сторону. Дописанные в этот заход List.in_eq («приписанное впереди принадлежит списку») и List.in_cons («приписывание не теряет вошедшего») подтвердили это ещё дважды: обе сетка, обе на настоящих телах приписать первый к элементы.

Проверка на пустое обещание: четыре заглушки, а не две

Обещание, верное при любом теле, ничего не проверяет. Все 45 доказанных обещаний обоих файлов прогнаны через подмену тела заглушками. Итог короткий: пустых нет. Но чтобы это узнать, канонической пары заглушек не хватило, и вот числа.

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

Правило, которое из этого следует: у обещания-границы и у обещания «результат — одно из трёх» каноническая пара 0 и 1 бессильна, потому что обе заглушки сами лежат внутри границы. Такому обещанию нужна заглушка снаружи: больше потолка или меньше нуля. Это дополнение к канону, а не опровержение его: две заглушки по-прежнему нужны, просто их иногда мало.

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

Что этот замер говорит о ядре

Четыре вывода, которые не были очевидны до прогона.

Первое: граница проходит не по «трудности» леммы, а по виду второго довода. Одна и та же лемма даёт разные вердикты в зависимости от того, терм там или литерал, — и это померено дважды и порознь: у остатка (Nat.mod_bound_pos) и у монотонности сложения (Nat.le_add_r). Для человека а ≤ а + б и а ≤ а + 10 — одно утверждение; для ядра первое требует отрезка у б, а второе читает отрезок прямо из числа.

Второе: точный тип работает и работает даром. Двенадцать обещаний из двадцати девяти доказанных в арифметике пришли объявленным типом (объявленным типом 12 в отчёте) — втрое больше, чем в прошлом замере. нат даёт и дно, и потолок; на нём взялись рефлексивность, неотрицательность, обе границы остатка по литералу, обе границы минимума и максимума и монотонность сложения на литеральной прибавке. Это самый дешёвый приём во всём файле.

Третье: определение доказывается, следствия — нет. Обе ветви Евклида (Nat.gcd_zero_right и Nat.gcd_rec) доказаны, а Nat.gcd_comm, Nat.gcd_dvd_left, Nat.gcd_dvd_right — нет. То же с чётностью: Nat.even_spec и Nat.odd_spec доказаны, Nat.even_add и Nat.even_mul — нет. Ядро берёт то, что записано в теле, и почти ничего из того, что из тела следует.

Четвёртое: про списки ядро считает, но не отождествляет. Из шестнадцати доказанных в файле списков четырнадцать — про длину, а оставшиеся два — про вспомогательные числовые функции, которыми кормятся примеры. Ни одного равенства двух списков не взялось. Стена ровная и проходит по одному месту.

Как повторить замер

PAMYAT=45G /srv/flang-rabota/vorota/flang-vorota -- \
  ./bootstrap/flang check flang/stdlib/math-classics.flang --proof
PAMYAT=45G /srv/flang-rabota/vorota/flang-vorota -- \
  ./bootstrap/flang check flang/stdlib/math-classics-lists.flang --proof

Строка, которую надо смотреть, — последняя в отчёте о доказательствах:

утверждений N: доказано M (из них без теоремы L), сетка S

Считать надо только доказано. сетка — это конечный набор значений, и про остальные входы она не говорит ничего.

Замер снят двоичным /srv/flang-rabota/w-predely/bootstrap/flang (собран 23 августа 2026, с поднятым пределом шагов). Двоичный, собранный из семени этого дерева, может отвечать иначе: часть правил ядра дописана в исходники позже семени и доедет следующей перепечаткой. Если ваши числа разошлись с этой страницей — первым делом сверьте, каким двоичным вы считали.

Куда идти дальше

• «Какие обещания ядро берёт» — формы записи, про каждую сказано прогоном, берёт её ядро или нет.
• «Ядро отказало: чья это ошибка» — тринадцать кодов отказа и что каждый значит.
• «Что доказано, а что нет» — та же честность по всей стандартной библиотеке.