fix: set implicitReducible on grandparent subobject projections#12701
Merged
kim-em merged 3 commits intoleanprover:masterfrom Mar 1, 2026
Merged
fix: set implicitReducible on grandparent subobject projections#12701kim-em merged 3 commits intoleanprover:masterfrom
kim-em merged 3 commits intoleanprover:masterfrom
Conversation
When a class `C extends P₁, P₂` has diamond inheritance, some ancestor structures become constructor subobject fields even though they aren't direct parents. For example, in `Monoid extends Semigroup, MulOneClass`, `One` becomes a constructor subobject because its field (`one`) doesn't overlap with `Semigroup`'s fields and `inSubobject?` is `none` during `MulOneClass` flattening. `mkProjections` creates the projection (e.g., `Monoid.toOne`) but defers reducibility to `addParentInstances`. However, `addParentInstances` only processes direct parents from the `extends` clause. Grandparent subobject projections fall through the gap — they're never registered as instances and never get `implicitReducible`. This causes defeq failures when `backward.isDefEq.respectTransparency` is enabled: at `.instances` transparency, the semireducible grandparent projection can't unfold, so two paths to the same ancestor structure aren't recognized as definitionally equal. Fix: before `addParentInstances`, iterate over all `.subobject` fields and set `implicitReducible` on those whose parent is a class. This is idempotent with `addParentInstances` for direct parents and fills the gap for grandparent subobjects. Co-Authored-By: Claude Opus 4.6 <[email protected]>
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
The #guard_msgs + #print approach failed because #print includes the definition body, which is hard to predict exactly. Use #eval with getReducibilityStatus instead. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Move `import Lean` before module doc, use `#guard_msgs` with `getReducibilityStatus` + `repr` to check reducibility programmatically. The previous test used `guard` (no `Alternative` for `CommandElabM`) and the wrong `getReducibilityStatus` signature. Co-Authored-By: Claude Opus 4.6 <[email protected]>
|
Mathlib CI status (docs):
|
mathlib-lean-pr-testing
bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
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-12701-to-releases/v4.29.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 3ea59e15b8ebd9b0b6fc2ccc9bf64eaeb0ba6499
# Push it to GitHub
git push --set-upstream origin backport-12701-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 |
kim-em
added a commit
that referenced
this pull request
Mar 1, 2026
This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent projections during structure elaboration. When `class C extends P₁, P₂` has diamond inheritance, some ancestor structures become constructor subobject fields even though they aren't direct parents. For example, in `Monoid extends Semigroup, MulOneClass`, `One` becomes a constructor subobject of `Monoid` — its field `one` doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none` during `MulOneClass` flattening. `mkProjections` creates the projection `Monoid.toOne` but defers reducibility to `addParentInstances` (guarded by `if !instImplicit`). However, `addParentInstances` only processes direct parents from the `extends` clause. Grandparent subobject projections fall through the gap and stay `semireducible`. This causes defeq failures when `backward.isDefEq.respectTransparency` is enabled (#12179): at `.instances` transparency, the semireducible grandparent projection can't unfold, so two paths to the same ancestor structure aren't recognized as definitionally equal. Fix: before `addParentInstances`, iterate over all `.subobject` fields and set `implicitReducible` on those whose parent is a class. 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 <[email protected]>
github-merge-queue bot
pushed a commit
that referenced
this pull request
Mar 3, 2026
…ns (#12778) This PR fixes an inconsistency in `getStuckMVar?` where the instance argument to class projection functions and auxiliary parent projections was not whnf-normalized before checking for stuck metavariables. Every other case in `getStuckMVar?` (recursors, quotient recursors, `.proj` nodes) normalizes the major argument via `whnf` before recursing — class projection functions and aux parent projections were the exception. This bug was identified by Matthew Jasper. When the instance parameter to a class projection is not normalized, `getStuckMVar?` may fail to detect stuck metavariables that would be revealed by whnf, or conversely may report stuckness for expressions that would reduce to constructors. This caused issues with `OfNat` and `Zero` at `with_reducible_and_instances` transparency. Note: PR #12701 (already merged) is also required to fix the original Mathlib examples.
kim-em
pushed a commit
that referenced
this pull request
Mar 4, 2026
…ns (#12778) This PR fixes an inconsistency in `getStuckMVar?` where the instance argument to class projection functions and auxiliary parent projections was not whnf-normalized before checking for stuck metavariables. Every other case in `getStuckMVar?` (recursors, quotient recursors, `.proj` nodes) normalizes the major argument via `whnf` before recursing — class projection functions and aux parent projections were the exception. This bug was identified by Matthew Jasper. When the instance parameter to a class projection is not normalized, `getStuckMVar?` may fail to detect stuck metavariables that would be revealed by whnf, or conversely may report stuckness for expressions that would reduce to constructors. This caused issues with `OfNat` and `Zero` at `with_reducible_and_instances` transparency. Note: PR #12701 (already merged) is also required to fix the original Mathlib examples.
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
2 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 fixes a gap in how
@[implicit_reducible]is assigned to parent projections during structure elaboration.When
class C extends P₁, P₂has diamond inheritance, some ancestor structures become constructor subobject fields even though they aren't direct parents. For example, inMonoid extends Semigroup, MulOneClass,Onebecomes a constructor subobject ofMonoid— its fieldonedoesn't overlap withSemigroup's fields, andinSubobject?isnoneduringMulOneClassflattening.mkProjectionscreates the projectionMonoid.toOnebut defers reducibility toaddParentInstances(guarded byif !instImplicit). However,addParentInstancesonly processes direct parents from theextendsclause. Grandparent subobject projections fall through the gap and staysemireducible.This causes defeq failures when
backward.isDefEq.respectTransparencyis enabled (#12179): at.instancestransparency, the semireducible grandparent projection can't unfold, so two paths to the same ancestor structure aren't recognized as definitionally equal.Fix: before
addParentInstances, iterate over all.subobjectfields and setimplicitReducibleon those whose parent is a class.🤖 Prepared with Claude Code