feat: adjust instances in inferInstanceAs and def ... deriving#12897
Merged
nomeata merged 3 commits intoleanprover:masterfrom Mar 22, 2026
Merged
feat: adjust instances in inferInstanceAs and def ... deriving#12897nomeata merged 3 commits intoleanprover:masterfrom
inferInstanceAs and def ... deriving#12897nomeata merged 3 commits intoleanprover:masterfrom
Conversation
github-actions
Bot
added
the
toolchain-available
Collaborator
|
Reference manual CI status:
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 12, 2026
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 12, 2026
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 17, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 17, 2026
|
Mathlib CI status (docs):
|
kim-em
force-pushed
the
push-vqmkmnsnsrvl
branch
2 times, most recently
from
468f21d to
4547327
Compare
kim-em
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 18, 2026
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 18, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 18, 2026
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 18, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 18, 2026
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 18, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 18, 2026
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 18, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 18, 2026
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 18, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 18, 2026
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
kim-em
changed the title
inferInstanceAs and deriving
kim-em
requested review from
TwoFX,
datokrat,
hargoniX,
kim-em,
leodemoura and
tydeu
as code owners
kim-em
added
backport releases/v4.29.0
changelog-language
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 22, 2026
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
Member
Author
|
!bench |
|
Benchmark results for 30e3a09 against 90b5e31 are in. Significant changes detected! @Kha
Large changes (5🟥)
Medium changes (3✅, 4🟥)
Small changes (142✅, 127🟥) Too many entries to display here. View the full report on radar instead. |
|
Mathlib CI status (docs):
|
This PR adjusts the results of `inferInstanceAs` and the `def` `deriving` handler to conform to recently strengthened restrictions on reducibility. This change ensures that when deriving or inferring an instance for a semireducible type definition, the definition's RHS is not leaked when the instance is reduced at lower than semireducible transparency. More specifically, given the "source type" and "target type" (the given and expected type for `inferInstanceAs`, the right-hand side and applied left-hand side of the `def` for `deriving`), we synthesize an instance for the source type and then unfold and rewrap its components (fields, nested instances) as necessary to make them compatible with the target type. The individual steps are represented by the following options, which all default to enabled and can be disabled to help with porting: - `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs` and the default `deriving` handler - `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type for sub-instance fields to avoid non-defeq instance diamonds - `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions - `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are always wrapped) This PR is an extension and rewrite of prior work in Mathlib: leanprover-community/mathlib4#36420 Last(?) part of fix for leanprover#9077 🤖 Prepared with Claude Code # Breaking changes Proofs that relied on the prior "defeq abuse" of these instance or that depended on their specific structure may need adjustments. As `inferInstanceAs A` now needs to know the source and target types exactly before it can continue, it cannot be used anymore as a synonym for `(inferInstance : A)`, use the latter instead when source and target type are identical.
Contributor
|
The backport to To backport manually, run these commands in your terminal: # Fetch latest updates from GitHub
git fetch
# Create a new working tree
git worktree add .worktrees/backport-releases/v4.29.0 releases/v4.29.0
# Navigate to the new working tree
cd .worktrees/backport-releases/v4.29.0
# Create a new branch
git switch --create backport-12897-to-releases/v4.29.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7
# Push it to GitHub
git push --set-upstream origin backport-12897-to-releases/v4.29.0
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-releases/v4.29.0Then, create a pull request where the |
This was referenced Mar 22, 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
5 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 adjusts the results of
inferInstanceAsand thedefderivinghandler to conform to recently strengthened restrictions on reducibility. This change ensures that when deriving or inferring an instance for a semireducible type definition, the definition's RHS is not leaked when the instance is reduced at lower than semireducible transparency.More specifically, given the "source type" and "target type" (the given and expected type for
inferInstanceAs, the right-hand side and applied left-hand side of thedefforderiving), we synthesize an instance for the source type and then unfold and rewrap its components (fields, nested instances) as necessary to make them compatible with the target type. The individual steps are represented by the following options, which all default to enabled and can be disabled to help with porting:backward.inferInstanceAs.wrap: master switch for instance adjustment in bothinferInstanceAsand the defaultderivinghandlerbackward.inferInstanceAs.wrap.reuseSubInstances: reuse existing instances for the target type for sub-instance fields to avoid non-defeq instance diamondsbackward.inferInstanceAs.wrap.instances: wrap non-reducible instances in auxiliary definitionsbackward.inferInstanceAs.wrap.data: wrap data fields in auxiliary definitions (proof fields are always wrapped)This PR is an extension and rewrite of prior work in Mathlib: leanprover-community/mathlib4#36420
Last(?) part of fix for #9077
🤖 Prepared with Claude Code
Breaking changes
Proofs that relied on the prior "defeq abuse" of these instance or that depended on their specific structure may need adjustments. As
inferInstanceAs Anow needs to know the source and target types exactly before it can continue, it cannot be used anymore as a synonym for(inferInstance : A), use the latter instead when source and target type are identical.