Skip to content

feat: add @[reducible_proj] for selective projection unfolding#13562

Draft
kim-em wants to merge 5 commits into
leanprover:masterfrom
kim-em:reducible-proj-attr
Draft

feat: add @[reducible_proj] for selective projection unfolding#13562
kim-em wants to merge 5 commits into
leanprover:masterfrom
kim-em:reducible-proj-attr

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Apr 29, 2026 •
edited
Loading

When whnfCore reduces a projection s.field at low transparency (e.g. .instances, used during implicit-arg isDefEq when backward.isDefEq.respectTransparency = true), it can get stuck if s is produced by a [semireducible] definition.

Concrete case in Mathlib (CategoryTheory.Whiskering, CategoryTheory.EssentialImage, and ~588 other CategoryTheory files):

-- Func.comp is [semireducible]; doesn't unfold at .instances.
example (X : C) : (F ⋙ G).obj X = G.obj (F.obj X) := by
  with_reducible_and_instances rfl  -- fails

Currently the only workarounds are:

  • Mark the producing definition (e.g. Functor.comp) [implicit_reducible] — heavy hammer; affects all uses.
  • Set backward.isDefEq.respectTransparency false locally — restores old globally permissive behavior.

@[reducible_proj] opts a single projection function (e.g. Functor.obj) into a one-time transparency bump for the structure-argument WHNF when the configured projection strategy fails to expose a constructor. The bump is local to the projection reduction; it does not change the transparency of surrounding isDefEq work.

This is the structure-projection analogue of the existing class-field machinery (unfoldProjInst? / backward.whnf.reducibleClassField), which does exactly the same thing for [reducible] class fields whose underlying instance is [implicit_reducible].

🤖 Prepared with Claude Code

@kim-em kim-em changed the title RFC: feat: add @[reducible_proj] for selective projection unfolding feat: add @[reducible_proj] for selective projection unfolding Apr 29, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 29, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 29, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-29 01:42:16)
  • ✅ Reference manual branch lean-pr-testing-13562 has successfully built against this PR. (2026-05-08 07:00:51) View Log
  • 🟡 Reference manual branch lean-pr-testing-13562 build against this PR didn't complete normally. (2026-05-08 07:01:48) View Log
  • 🟡 Reference manual branch lean-pr-testing-13562 build against this PR didn't complete normally. (2026-05-12 05:15:12) View Log
  • ✅ Reference manual branch lean-pr-testing-13562 has successfully built against this PR. (2026-05-12 05:15:20) View Log

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 29, 2026
@kim-em kim-em added the changelog-language Language features and metaprograms label Apr 29, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 29, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Apr 29, 2026 •
edited
Loading

Mathlib CI status (docs):

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 29, 2026
Update lean-toolchain for leanprover/lean4#13562
fb2bddf
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 29, 2026
Update lean-toolchain for leanprover/lean4#13562
2d1e2f3
@kim-em kim-em force-pushed the reducible-proj-attr branch from 6f8f160 to 8f03161 Compare May 8, 2026 06:01
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 8, 2026
Update lean-toolchain for leanprover/lean4#13562
0af38a3
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 8, 2026
Update lean-toolchain for leanprover/lean4#13562
c1edf69
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label May 8, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels May 8, 2026
kim-em and others added 5 commits May 11, 2026 17:06
@kim-em @claude
RFC: feat: add @[reducible_proj] for selective projection unfolding
d510e3e 
When `whnfCore` reduces a projection `s.field` at low transparency (e.g.
`.instances`, used during implicit-arg `isDefEq` when
`backward.isDefEq.respectTransparency = true`), it can get stuck if the
structure argument `s` is produced by a `[semireducible]` definition.

`@[reducible_proj]` opts in a single projection function to trigger a
one-time bump to `.default` transparency for the structure-argument
WHNF when the configured projection strategy fails to expose a
constructor. This mirrors the existing class-field bump machinery
(`unfoldProjInst?` / `backward.whnf.reducibleClassField`).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@kim-em @claude
test: add elab test for @[reducible_proj]
752c43b 
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@kim-em @claude
fix: route [reducible_proj] bump through reduceProj?
eebfd38 
The original PR placed the transparency bump only in `whnfCore`'s `.proj` arm.
Callers that reduce projection-function applications via `reduceProj?` (grind's
`Sym.canon`, `simp`, `cbv`, vcgen, and `unfoldProjInst?` itself) bypass that arm
and so never see the bump. Concretely, `attribute [reducible_proj] Functor.obj`
in mathlib's CategoryTheory breaks many `grind` proofs because canon
short-circuits `whnfCore.proj` and the bump never fires.

This commit extracts a `tryReducibleProjBump?` helper next to `reduceProj?` and
calls it from both `reduceProj?` and `whnfCore`'s `.proj` arm, so every
projection-reduction site honors the attribute uniformly.

Three secondary improvements ride along:

- Use `withAtLeastTransparency .default` instead of `withTransparency .default`,
  so the bump only raises transparency. The old code would downgrade from
  `.all` to `.default`.
- The attribute validator now rejects class-field projections, which already
  have orthogonal support via `unfoldProjInst?` /
  `backward.whnf.reducibleClassField`.
- The `reducibleProjAttr` docstring points at the shared helper.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@kim-em @claude
fix: beta-reduce result of projection-function reduction in Sym.canon
657226c 
`Sym.canon.reduceProjFn?` unfolds the projection function, then re-applies
arguments after reducing the kernel projection. The re-application used
`mkAppN` without subsequent `.headBeta`. When the structure is a concrete
constructor (so the projected field is a lambda), the result was an
unbeta'd `(fun x => body) y`, which is a distinct term from `body[y]` in the
e-graph.

This was latent: before `[reducible_proj]`, `reduceProj?` would only return
`Some` for fully evaluated constructors that rarely appear in canon's input,
so the bug had no observable effect. With the bump in `reduceProj?` (previous
commit), projection-function applications like `Functor.obj (F⋙G) X` now
reduce to `(fun X => G.obj (F.obj X)) X` and the missing `.headBeta` becomes
visible — `grind`'s ematch fails to recognize the term.

Mirrors the `.headBeta` already used in `unfoldProjInst?`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@kim-em @claude
test: add regression coverage for [reducible_proj] via reduceProj?
b5854c5 
Extends `tests/elab/reducibleProj.lean` with:

- A `grind`-driven natural-transformation `hcomp` regression. Without the
  preceding two fixes, ematch fires `Functor.comp_obj` but canon collapses
  the asserted equality without recording an eqc edge, and
  `NatTrans.naturality` never fires on `(F ⋙ H).map f ≫ β.app (F.obj Y)`.
  With the fixes, `grind` discharges naturality.

- A validator test rejecting class-field projections.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@kim-em kim-em force-pushed the reducible-proj-attr branch from 8f03161 to b5854c5 Compare May 12, 2026 04:05
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 12, 2026
Update lean-toolchain for leanprover/lean4#13562
31695a8
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 12, 2026
Update lean-toolchain for leanprover/lean4#13562
c72a9ad
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request May 12, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13562
457c60c
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em @leanprover-bot