feat: virtual one-field structures

[datokrat]

This PR introduces type aliases that behave like one-field structures, except that they allow for isolated defeq abuses.

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#59.

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-15066 has successfully built against this PR. (2026-09-08 15:39:33) View Log
• 🟡 Reference manual branch lean-pr-testing-15066 build against this PR didn't complete normally. (2026-09-08 15:43:52) View Log
• ✅ Reference manual branch lean-pr-testing-15066 has successfully built against this PR. (2026-09-09 08:10:49) View Log
• 🟡 Reference manual branch lean-pr-testing-15066 build against this PR didn't complete normally. (2026-09-09 08:11:46) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-15066 build failed against this PR. (2026-09-08 16:19:04) View Log
• 💥 Mathlib branch lean-pr-testing-15066 build failed against this PR. (2026-09-09 09:21:23) View Log
• 💥 Mathlib branch lean-pr-testing-15066 build failed against this PR. (2026-09-09 13:05:44) View Log

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for 0c8bed4 against c155094 are in. There are significant results. @Rob23oba

• 🟥 build//instructions: +79.8G (+0.73%)

Large changes (3🟥)

• 🟥 elab/simp_local//instructions: +2.6G (+8.86%)
• 🟥 elab/simp_local//task-clock: +172ms (+7.55%)
• 🟥 elab/simp_local//wall-clock: +172ms (+7.55%)

Medium changes (3🟥)

• 🟥 elab/simp_bubblesort_256//instructions: +239.8M (+2.57%)
• 🟥 elab/simp_subexpr//instructions: +240.6M (+2.49%)
• 🟥 elab/whnfMatcherImplicitTransparencyCaching//instructions: +138.9M (+0.58%)

Small changes (436🟥)

• 🟥 build/module/Init.Control.Basic//instructions: +14.7M (+0.71%)
• 🟥 build/module/Init.Control.Lawful.Instances//instructions: +61.9M (+0.96%)
• 🟥 build/module/Init.Core//instructions: +73.5M (+0.77%)
• 🟥 build/module/Init.Data.Array.Attach//instructions: +113.4M (+1.15%)
• 🟥 build/module/Init.Data.Array.Basic//instructions: +80.8M (+0.77%)
• 🟥 build/module/Init.Data.Array.BinSearch//instructions: +29.6M (+0.51%)
• 🟥 build/module/Init.Data.Array.Count//instructions: +26.0M (+0.99%)
• 🟥 build/module/Init.Data.Array.Erase//instructions: +76.8M (+1.12%)
• 🟥 build/module/Init.Data.Array.Extract//instructions: +203.6M (+0.62%)
• 🟥 build/module/Init.Data.Array.Find//instructions: +116.8M (+1.25%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Array.InsertIdx//instructions: +19.7M (+0.77%)
• 🟥 build/module/Init.Data.Array.Lemmas//instructions: +566.8M (+1.11%)
• 🟥 build/module/Init.Data.Array.Lex.Lemmas//instructions: +139.7M (+1.52%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Array.MapIdx//instructions: +91.9M (+1.09%)
• 🟥 build/module/Init.Data.Array.MinMax//instructions: +30.0M (+1.10%)
• 🟥 build/module/Init.Data.Array.Monadic//instructions: +63.1M (+1.09%)
• 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +109.9M (+1.13%)
• 🟥 build/module/Init.Data.Array.Range//instructions: +38.6M (+1.01%)
• 🟥 build/module/Init.Data.Array.Sort.Lemmas//instructions: +23.8M (+0.78%)
• 🟥 build/module/Init.Data.Array.Zip//instructions: +53.6M (+1.22%)
• and 416 more

[datokrat]

@Rob23oba I'm aware that it's significantly slower right now; if this turns out to be a good idea, I'll invest into the performance :)

[Rob23oba]

Can you help me understand what this is for? My first thought would be all those type defs that we have in mathlib and use with inferInstanceAs but if we really make these @[irreducible] defs, then even inferInstanceAs (and compilation!) would have trouble with this, no? So for this case, this would not have any advantage over just using one-field structures. But then, what would be the use in proofs?

[datokrat]

@Rob23oba Mathlib currently has many semireducible or implicit-reducible definitions. These are footguns. They make forms of defeq abuse all to easy that interfere with automation, unificaiton and instance synthesis. Not all of them are easily/nicely converted into one-field structures. The idea here is to provide something similar to a one-field structure, but with an escape hatch inside of tactic blocks (unsealing_newtype ... => rfl).

Of course, it would be best if no defeq abuse was present at all, but having a newtype in the sense of this PR and a few proof-local abuses is still much better than a semireducible def, where it's much too easy to accidentally introduce abuse, even into the public API. If the presence of such an escape hatch will help form a consensus that we work to get rid of the semireducible/implicit-reducible type aliases, then this would be a big win.

If unsealing_newtype isn't used, using a one-field structure would be just as good (with the minor exception that newtypes make it possible to safely define a computable, zero-cost cast from List a to List (Wrapper a), for example, because a = Wrapper a.

Does that make sense to you?

[Rob23oba]

Well my question is I guess: what does newtype provide that one-field structures don't? A safe cast from List a to List (Wrapper a), fair, but that's probably not what mathlib needs, right?

[datokrat]

It allows you to do defeq abuse in tactic blocks, identifying a with Wrapper a definitionally. That's not possible with one-field structures, right? Are we talking past each other?

[Rob23oba]

Oh no I totally understand that this is how these work. I'm just not sure why you would need that? Do you have an example?
Edit: like when I look at the tests, most of them just demonstrate that newtype behaves like one-field structures and the only real case of unsealing_newtype that's being presented is a type equality which is certainly not something we should need in mathlib, right?

[datokrat]

I'm thinking, for example, of OrderDual. My understanding is that people are hesitant to migrate it to a one-field structure because it would, while definitely possible, introduce a lot of duplication. I don't have a strong opinion on whether preserving this defeq abuse in order to get shorter proofs is the right way to go, but if making this possible allows us to get rid of type aliases, I'm ready to enable it.

You can see how this plays out for OrderDual in the downstream adaptation branch to this PR. I deliberately chose the extreme of preserving as many of the old proofs with unsealing_newtype for this spike; it doesn't mean this is the optimal way to do the migration.

Link: leanprover/downstream-lean4#59