coq(CorePhi): replace proofs that were never checked by a compiler - #3343
Open
gHashTag wants to merge 2 commits into
Open
coq(CorePhi): replace proofs that were never checked by a compiler#3343gHashTag wants to merge 2 commits into
gHashTag wants to merge 2 commits into
Conversation
added 2 commits
September 6, 2026 09:01
…rror Refs #3328 `coqc ... || exit 1` thirteen times stops at the first failure. One CI run therefore yields exactly one error, and finding out how many of the 13 files compile costs one run per file at roughly four minutes each. That was harmless while the job could not start at all. It became the binding constraint the moment it could: this workflow had never got past `opam install`, so coqc had never run on these proofs, and the first thing it said was that file 1 of 13 does not compile. The state of the other twelve was UNKNOWN -- not passing -- and a stop-at-first-error loop cannot answer that question cheaply or at all. The step now attempts every file and prints a table with a count. Failures after the first are tagged FAIL*, because these compile in dependency order and a missing .vo cascades: only the first failure is certainly its own defect. The full coqc output for each failing file goes into a collapsed `::group::` so the table stays readable and nothing is lost. Exit behaviour is unchanged -- any failure still fails the job. Controls, run locally against a stub `coqc`: - stub fails on files 1 and 5 -> "11 of 13 compiled", FAIL on CorePhi.v, FAIL* on Bounds_Mixing.v, exit 1 - stub passes everything -> "All files compiled successfully!", exit 0 Checked with `sh -n` as well as `bash -n`: the container runs `sh -e {0}`, so a bashism would have been a runtime failure and not a syntax error here.
Refs #3328 The first full reading, from the report added in the commit below: 0 of 13 files compile. The twelve after CorePhi.v all fail at their `Require Import` line, so they are cascades -- the real state of files 2-13 is still unknown, and CorePhi.v is what gates it. CorePhi.v is not one missing lemma. It has never been seen by coqc, and it shows: - `lra` is used eleven times and `Lra` is never imported. - `apply Rmult_lt_pos_pos` (line 14) names a lemma that does not exist. This is the error the job reported, and it is the least of them. - `apply phi_quadratic; ring` (line 38) applies `phi^2 - phi - 1 = 0` to the goal `phi^2 = phi + 1`. `apply` unifies conclusions; these do not unify. The same idiom appears five times. - `Rlt_lt_1` (line 94) and `sqrt_lt_cancel` (line 97) do not exist. - `field` (line 32) cannot prove `phi^2 - phi - 1 = 0`: `sqrt 5` is an opaque constant to it, so an identity resting on sqrt 5 * sqrt 5 = 5 is not an identity it can see. Every STATEMENT is true and every statement is kept byte-identical -- verified by diffing the sorted `Lemma`/`Definition` lines against master. Only the proofs change. Two helper lemmas are added, `sqrt5_sq` and `sqrt5_nonneg`, carrying the one fact `ring` and `field` cannot discover. Nothing is removed, so no downstream file can break on a missing name. Unverified locally: there is no Coq toolchain on this machine and installing one would take several GB on a disk that is at 99%. This PR runs the workflow on itself (#3324 added the file to its own `pull_request` paths), so its own run is the check. If a proof still fails, the report now names which files got further, which is the reading that was missing.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Sep 6, 2026
This was referenced Sep 6, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Refs #3328 · stacked on #3342 (the all-files report), which this needs in order to read its own result
The reading
With #3324 and #3326 merged,
coqcran on these files for the first time. With#3342's report, here is what it says:
Zero of thirteen. The twelve after
CorePhi.vfail at theirRequire Importline, so they are cascades — the real state of files 2–13 is still unknown, and
CorePhi.vis what gates it.CorePhi.v is not one missing lemma
Require Import Reals.Reals.onlylrais used eleven times andLrais never importedapply Rmult_lt_pos_posfieldforphi^2 - phi - 1 = 0sqrt 5is opaque tofield; an identity resting on√5·√5 = 5is not one it can seeapply phi_quadratic; ringphi^2 - phi - 1 = 0to goalphi^2 = phi + 1;applyunifies conclusions, and these do not. The same idiom appears five times (38, 44, 50, 57)apply Rlt_lt_1apply sqrt_lt_cancelThe mathematics is all correct — φ² = φ+1, φ⁻² = 2−φ, φ⁵ = 5√5+8 are true. Essentially none of it is proved.
What this changes
Statements: none. Verified by diffing the sorted
Lemma/Definitionlinesagainst master — every original statement is byte-identical, nothing removed, so
no downstream file can break on a missing name.
Proofs: all of them, plus two helpers (
sqrt5_sq,sqrt5_nonneg) carryingthe one fact
ringandfieldcannot discover.Honesty about verification
There is no Coq toolchain on this machine, and installing one would take several
GB on a disk sitting at 99%. These proofs are not verified locally. This PR
runs the workflow on itself (#3324 added the file to its own
pull_requestpaths), so its own run is the check — and thanks to #3342, a partial success is
still informative: the report names which files got further.