Coq and Lean classics: what our kernel actually proves

This page is not a survey of Coq and not a retelling of Mathlib. It is a measurement: seventy-five classical lemmas, copied verbatim from the Coq and Lean sources, rewritten in flang as real functions with postconditions, and run through our kernel. Every lemma carries a verdict taken from a run, and every unproved one carries a named reason.

A negative result is worth more here than a positive one. A page saying "75 out of 75 proved" would be refuted by the reader's first run, and after that nothing else on this site would be believed.

The bottom line

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

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

That is 104 claims, 45 proved. Of the seventy-five classical lemmas the kernel takes twenty-five outright; forty-nine stay a grid, each with a named reason below; and one more — the termination of Euclid's algorithm — cannot be written in flang at all.

There are no axioms in these files: the "taken on faith" column of both reports is empty (принято на веру: ничего).

What changed since the previous measurement. It was 73 claims and 29 proved, forty-seven lemmas of which thirteen were taken outright. The gain came not from rewriting old postconditions but from new lemmas and from two measured boundaries of the kernel's rules: monotonicity of addition is taken when the addend is a literal and refused when it is a term (exactly like the bound on a remainder), and the bounds of min and max are taken when the guard is copied from the body word for word.

Where the names come from

Every lemma name in the tables was found in a downloaded file, not recalled from memory. Where nothing was found, the table has a dash.

Two details that will save the reader time. First: on Coq's master the standard library has moved to a separate repository (rocq-prover/stdlib), so coq/coq/master/theories/… returns 404 today — the files above were taken at tag V8.19.2. Second: Mathlib/Data/Nat/Defs.lean no longer exists; nearly all of the Nat classics moved into the Lean 4 core (src/Init/Data/Nat/…), and only the superstructure stayed in Mathlib.

Three names are confirmed by use, not by declaration, and that must be said plainly. Nat.le_add_r, Nat.le_0_l and Nat.sub_add are called in the downloaded files (theories/Arith/PeanoNat.v:411, theories/Lists/List.v:506 and :1701, theories/Numbers/Natural/Abstract/NOrder.v:25, theories/Numbers/Natural/Abstract/NParity.v:41), but they are declared in files this measurement did not download (NBase.v, NSub.v). The name exists; the declaration line was not checked.

Reading a verdict

There are exactly four outcomes, and telling them apart is mandatory:

In these two files only two outcomes occurred: proved and grid.

How nat was translated

In Coq and Lean every lemma below is stated over nat — an exact type with no NaN, no infinities and no fractions. flang's число is IEEE-754, and over it half of the classics are simply false:

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

So wherever they write nat we write нат — the exact range [0, 2⁵³−1]. This is not cosmetics but a condition of an honest translation; the same argument is recorded in flang/test/fixtures/poddelka-order-arithmetic.flang.

A side measurement that cost one run. In the compiler sources and in flang/SPEC.md the same type is called неотрицательное, and flang/stdlib/strlists.flang uses that name. The printed binary does not know it: flang check on the stock strlists.flang answers FLANG_UNKNOWN_NAME … неизвестный тип «неотрицательное», while the kernel's own refusal texts call the type нат. The binary lags the sources until the seed is reprinted; write нат.

Table: arithmetic

File — flang/stdlib/math-classics.flang, 45 functions, 67 claims. The number in parentheses is the line in the downloaded file.

Fifty-four rows: fifty-three lemmas written in flang and one ("Euclid terminates") that cannot be written at all. Nineteen are taken outright. Trichotomy is split in the file into three branches, and all three are proved.

Table: lists

File — flang/stdlib/math-classics-lists.flang, 25 functions, 37 claims. The number in parentheses is the line in theories/Lists/List.v at tag V8.19.2 or in the named Lean file.

Twenty-one lemmas, six taken outright.

Weakenings, said out loud. For nine lemmas where full list equality was not taken, the same statement about length only stands next to it, and eight of the nine are proved. This does not replace the lemma — it is strictly weaker, and the verdict in the table belongs to the full form, not to the weakening.

Why it is not taken: the reasons, one by one

The forty-nine unproved lemmas fall into eight named reasons, and none of them is "the kernel is weak in general".

1. Associativity and distributivity: the kernel matches SYNTACTICALLY

The kernel's refusal states it verbatim: after rewriting with the premises the two sides of the equality remain different terms; the kernel matches syntactically and does not decide equalities of computations. It reads плюс and умножить up to the order of neighbours at one node (swapping two operands of the same node is an IEEE-754 theorem; swapping across parentheses is not, because associativity is false in IEEE-754, and the kernel does not do it).

Hence exactly what we measured: commutativity is taken, associativity is not, for both addition and multiplication. That is not a gap but honesty: over floats associativity really is false, and a rule that took it would be proving a falsehood.

The same single rule explains Nat.add_assoc, Nat.mul_assoc, Nat.mul_add_distr_l, Nat.mul_add_distr_r — four lemmas.

2. Neutral element and absorption: а плюс 0 and а are different terms

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 — seven lemmas, all running into the same syntactic match: substituting the body gives (а плюс 0) равен а, and those are two different trees. On a bare body the kernel has no "fold the neutral element" rule.

On the path through a callee's postcondition it does have one — on one side only. This explains an asymmetry that the previous edition of this page left unsolved: List.app_nil_l (append with empty on the LEFT, weakened to length) is proved while its mirror List.app_nil_r is a grid. Probe, taken from a run:

«Склеить с пустым справа», body «Склеить» от элементы и пустой список:
  (длина результат) равен ((длина элементы) плюс (длина пустой список))  — PROVED
  (длина результат) равен ((длина элементы) плюс 0)                      — PROVED
  (длина результат) равен (длина элементы)                               — grid

«Склеить с пустым слева», body «Склеить» от пустой список и элементы:
  (длина результат) равен (0 плюс (длина элементы))                      — PROVED
  (длина результат) равен (длина элементы)                               — PROVED

The composed form is taken on both sides. The single difference: a leading zero is folded away, a trailing one is not. Where exactly the kernel walks is not visible from the refusal; only this is measurable.

A neighbouring measurement worth knowing: in the lists file the claim "doubling is a sum with itself" over the body х умножить на 2 is also a grid, while "adding one is a sum with one" over the body х плюс 1 is proved. The difference is exactly whether the goal's tree matched the body's tree.

3. Inequalities over a term: the rule exists under zero, under the type, and under a LITERAL

Nat.le_add_r (term addend), 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 (term divisor) — nine lemmas.

The boundary runs along the kind of the addend, and this is a new measurement. One and the same lemma Nat.le_add_r yields two different verdicts:

«Сумма», body а плюс б with б: нат — addend a TERM:
  а не больше результат   — grid
  б не больше результат   — grid

«Следующее»,        body а плюс 1  — addend a LITERAL:  а не больше результат — PROVED
«Прибавить десять», body а плюс 10 — addend a LITERAL:  а не больше результат — PROVED

Both literal cases came back as "proved by the declared types of the arguments: the goal was reduced by the rule 'order by construction'". So the kernel does read the range that the type нат gives — but only when the second summand is a written number. This is the same dividing line as for the remainder (Nat.mod_bound_pos): not the "difficulty" of the lemma but the kind of the second argument.

What comes for free: Nat.le_refl and Nat.le_0_l, both with the same wording about declared types. But adding two premises а не больше б and б не больше в into a third is beyond it: its rewriting is single-goal.

The bounds of min and max were taken, and taken by a guard. Four claims — Nat.min_le_left, Nat.min_le_right, Nat.le_max_left, Nat.le_max_right — are written with a guard copied from the body word for word:

обеспечивает «меньшее из двух не больше первого»
  если (а не больше б) то (результат не больше а) иначе да     → PROVED

Under the guard the body reduces to а and the goal to reflexivity, which the type нат supplies. Technique 1 of "Which promises the kernel takes" works on a не больше goal too, not only on equalities.

The mirrored spelling does not help here, measured three times. For Nat.le_trans, Nat.le_antisymm and Nat.add_le_add_left the alternative spelling не (А) или (Б) was added (technique 6). All three stayed grids: the denominator grew, the numerator did not. The one for Nat.add_le_add_left was rolled back; the first two were kept so the reader can see both spellings. Splitting Nat.le_total by the three outcomes of a comparison (technique 11) ended in the same zero — three claims, no gain, rolled back.

Nat.sub_add is a special case: over IEEE-754 the law is false, with the counterexample (9007199254740994 минус 1) плюс 1 = 9007199254740992. Over нат it holds, but the kernel has no rule that would tell the exact integer grid apart from the rest of the numbers in a subtraction, and by the note in flang/self/proof-kernel.flang it will not get one.

4. Arithmetic of remainders: parity and divisibility

Nat.mod_1_r (the equality itself), Nat.mod_same, Nat.divide_refl, Nat.Even_or_Odd, Nat.even_add, Nat.even_mul, Nat.sub_self — seven lemmas. All of them ask for reasoning about remainders. The kernel has no such rules — only bounds on a remainder, and only with a literal divisor.

A separate measurement worth reading. For Nat.mod_1_r both bounds are proved and the equality is not:

«Остаток по единице», body н остаток от 1:
  результат не больше 0   — PROVED, rule "bounded by an exact ceiling by construction"
  0 не больше результат   — PROVED, rule "order by construction"
  результат равен 0       — grid

The kernel does not glue two of its own proved inequalities into an equality. This is not a quirk of the remainder: it cannot add two postconditions of one call together either, and here we see it cannot add two postconditions of one goal.

What was taken: Nat.even_spec and Nat.odd_spec, both by the rule "identity after rewriting with a premise", because they are literally definitions — the goal's tree coincided with the body's.

5. Recursion by remainder: gcd

Nat.gcd_comm, Nat.gcd_divide_l, Nat.gcd_divide_r, Nat.gcd_self, Nat.gcd_1_r — five lemmas with one shared cause: «НОД по Евклиду» is the only non-total function in both files. The pair (a, b) does decrease strictly in the second argument, but the step is a remainder rather than a constant difference, and flang's termination analysis does not read such a step.

What was taken — both branches of the recurrence, each by a guard copied from the body word for word:

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

Those are Nat.gcd_zero_right and Nat.gcd_rec: the definition of Euclid's algorithm is proved as a pair of postconditions, while not a single consequence of it is. Both go through the rule "split the goal by the condition".

And separately: the claim "Euclid terminates" cannot be written in flang. A decreasing measure is a property of the definition, not a postcondition of the result; Coq uses Fix/well-founded recursion, Lean uses decreasing_by, and we have the marker тотальная, which simply is not placed here.

6. Commutativity of min and max

Nat.min_comm, Nat.max_comm — two lemmas. Their goal is an equality between the result and a call of the same function with swapped arguments, and the kernel does not look inside a callee: it takes only its postconditions, and those of «Меньшее из двух» are written under guards and say nothing about swapping. This is the same broken chain that technique 7 describes in "Which promises the kernel takes".

7. Folds: the wall runs along their boundary

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 — eleven lemmas, the largest group.

The bodies of «Склеить» and «Обратить» are folds. The kernel does have a fold principle, as re-measured by neighbouring work (task 0050, commit b96826d7): it applies when the fold runs over the argument itself, named, at the top level of the body, and when the step carries a guard-free claim that the accumulator grows by exactly one. Both of our folds meet those conditions, the step has been lifted and does carry such a claim — and the principle still never fired: both runs, with the lifted step and with the lambda, report доказано 16 (из них без теоремы 16) and доказано 15 (из них без теоремы 15), with no "of them by induction" at all.

The length of a fold is computed by a different rule — "identity after rewriting with a premise" — and that rule suffices for every claim about the measure and for not a single claim about the contents. There is still no rule "a fold over the empty list is the base": both claims "over the empty list the fold is the base itself" (left and right) stayed grids.

Technique 8 was tried and cost minus one — that has to be said plainly. The fold step of «Склеить» was lifted into an ordinary function «Шаг склейки», and on it the claim (длина результат) равен ((длина акк) плюс 1) (List.last_length) is proved. But once the fold itself started calling the lifted step instead of the lambda, the file went 16 → 15 proved: List.app_nil_l in its weakening to length was lost. The change was rolled back and «Шаг склейки» left standing beside the fold. The warning in the manual ("lifting the step may drop a proof that stood") is now confirmed by a number.

What was taken, and taken everywhere: length. "length of an append is the sum of lengths", "reversing preserves length", "mapping preserves length", "a cons lengthens the list by exactly one", "the empty list has length zero" are all proved. About lists the kernel can count, but it cannot identify.

8. Membership and access by index

List.in_app_iff, List.in_eq, List.in_cons, List.nth_In — four lemmas, and this is the hole named third among the known ones: "element N of a list". The kernel has no bridge between содержит and элемент … в … in either direction. The two lemmas added in this pass — List.in_eq and List.in_cons — confirmed it twice more: both grids, both over real bodies приписать первый к элементы.

The empty-promise check: four stubs, not two

A promise that holds for any body checks nothing. All 45 proved claims of both files were run with their bodies replaced by stubs. The short answer: none is empty. But finding that out took more than the canonical pair of stubs, and here are the numbers.

For lists the canonical pair sufficed: none of the sixteen proved claims survived both. In arithmetic five claims survived both — and none of them is empty; they are caught only by a stub placed outside the bound:

The rule that follows: for a bound-shaped claim, and for a "the result is one of three" claim, the canonical pair 0 and 1 is powerless, because both stubs lie inside the bound themselves. Such a claim needs a stub from outside: above the ceiling or below zero. This extends the canon rather than refuting it — two stubs are still necessary, they are simply sometimes not enough.

A caveat about the honesty of the measurement: stubbing a whole file at once yields false "empties" wherever a goal refers to a neighbouring stubbed function. Those places are discarded in the tables above; in the real file they stand as grids anyway.

What this measurement says about the kernel

Four conclusions that were not obvious before the run.

First: the boundary runs along the kind of the second argument, not the "difficulty" of the lemma. The same lemma yields different verdicts depending on whether a term or a literal stands there — measured twice, independently: for the remainder (Nat.mod_bound_pos) and for monotonicity of addition (Nat.le_add_r). To a human а ≤ а + б and а ≤ а + 10 are one statement; to the kernel the first needs a range for б while the second reads the range straight off the number.

Second: an exact type works, and works for free. Twelve of the twenty-nine proved claims in arithmetic came by declared type (объявленным типом 12 in the report) — three times more than in the previous measurement. нат gives both a floor and a ceiling; on it we got reflexivity, non-negativity, both bounds of a remainder by a literal, both bounds of min and max, and monotonicity of addition with a literal addend. It is the cheapest technique in the whole file.

Third: the definition gets proved, its consequences do not. Both branches of Euclid (Nat.gcd_zero_right and Nat.gcd_rec) are proved while Nat.gcd_comm, Nat.gcd_dvd_left and Nat.gcd_dvd_right are not. The same with parity: Nat.even_spec and Nat.odd_spec are proved, Nat.even_add and Nat.even_mul are not. The kernel takes what is written in the body and almost nothing that follows from it.

Fourth: about lists the kernel counts but does not identify. Of the sixteen proved claims in the lists file fourteen are about length, and the remaining two are about the small numeric helpers that feed the examples. Not a single equality of two lists was taken. The wall is flat and runs through one place.

Reproducing the measurement

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

The line to look at is the last one of the proof report:

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

Count only доказано. сетка is a finite set of values and says nothing about the rest of the inputs.

The measurement was taken with the binary /srv/flang-rabota/w-predely/bootstrap/flang (built 23 August 2026, with a raised step limit). A binary built from this tree's seed may answer differently: some kernel rules were written into the sources after the seed and will only arrive with the next reprint. If your numbers disagree with this page, first check which binary you counted with.

Where to go next

• "Which promises the kernel takes" — spelling forms, each with a run saying whether the kernel takes it.
• "The kernel refused: whose fault is it" — thirteen refusal codes and what each means.
• "What is proved and what is not" — the same honesty across the whole standard library.