fix: make theorems opaque to the kernel as well - #14896
Draft
nomeata wants to merge 3 commits into
Draft
Conversation
nomeata
marked this pull request as ready for review
August 23, 2026 07:43
nomeata
added
the
awaiting-mathlib
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 23, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 23, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Aug 23, 2026
mathlib-lean-pr-testing
Bot
added
builds-mathlib
|
nomeata
enabled auto-merge
August 23, 2026 13:00
nomeata
disabled auto-merge
August 23, 2026 13:27
nomeata
marked this pull request as draft
August 23, 2026 17:36
Collaborator
Author
|
This is ready to go and painless, it seems. But I’m inclined to bundle it with other kernel logic changes, else the coordination on the arena becomes a mess. |
Collaborator
Author
|
!perf |
This PR completes #12973: theorems are now also opaque to the kernel, which until now would still delta-reduce them. So the value of a theorem no longer affects whether a declaration type-checks, and conflicting theorem declarations with the same type can no longer make type checking depend on import order. The `Lean`-side `ConstantInfo.hasValue` was already adjusted in #12973, but the kernel uses the C++ `constant_info::has_value`, which was missed. That is what `type_checker::is_delta` consults, so `Acc.rec` applications, for instance, still reduced through theorem proofs in the kernel even though the elaborator refused to. Also switches `has_constructor` in `src/library/util.cpp` to an explicit `is_constructor` check, so it no longer piggybacks on `has_value`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XzL163q5FYpbZmT8EHQb3j
Passed inline, these proofs are abstracted into theorems, which the kernel no longer unfolds, so `Acc.rec` gets stuck on them and the test's defeq gate fails before it reaches its actual assertion. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M5jcJjLLjxhiAueieK4KEj
nomeata
force-pushed
the
joachim/kernel-thms-opaque
branch
from
August 25, 2026 09:55
8da35e5 to
cec8033
Compare
nomeata
changed the base branch from
master
to
joachim/prop-casesOn-projections
August 25, 2026 09:55
Collaborator
Author
|
!bench |
|
Benchmark results for cec8033 against 8f5e057 are in. No significant results found. @nomeata
Small changes (2✅, 1🟥)
|
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
3 participants
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.
This PR completes #12973: theorems are now opaque to the kernel as well, which until now would still delta-reduce them. The value of a theorem no longer affects whether a declaration type-checks, so conflicting theorem declarations of the same type can no longer make type checking depend on import order.
The
Lean-sideConstantInfo.hasValuewas already adjusted in #12973, but the kernel consults the C++constant_info::has_value, which was missed. That is whattype_checker::is_deltalooks at, soAcc.recapplications, for instance, still reduced through theorem proofs in the kernel even though the elaborator refused to.has_constructorinsrc/library/util.cppswitches to an explicitis_constructorcheck, so it no longer piggybacks onhas_value.Stacked on #14925, which makes
casesOnof a proposition reduce without unfolding the proof. Without it, a proof thatabstractNestedProofshas moved into an auxiliary theorem can no longer be eliminated into data.