feat: generalize `below` and `brecOn` on subsingletons by arthur-adjedj · Pull Request #12718 · leanprover/lean4

arthur-adjedj · 2026-02-26T23:14:22Z

This PR makes it so that (recursive) inductive predicate that are subsingletons, namely Acc, have below and brecOn be generated like any other non-predicate inductive type rather than treating them using IndPredBelow. This allows brecOn to eliminate to sorts instead of only Prop.

Closes #12739

leanprover-bot · 2026-02-27T00:27:38Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-23-rev2 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-02-27 00:27:38)

mathlib-lean-pr-testing · 2026-02-27T01:22:56Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12718 has successfully built against this PR. (2026-02-27 01:22:54) View Log

arthur-adjedj · 2026-02-28T12:42:49Z

!bench

leanprover-radar · 2026-02-28T12:42:55Z

Benchmark results for f03c018 against c595413 are in! @arthur-adjedj

🟥 build//instructions: +2.1G (+0.02%)

Small changes (4🟥)

🟥 build/module/Init.WF//instructions: +17.0M (+0.89%)
🟥 build/module/Lean.Meta.AbstractNestedProofs//instructions: +45.8M (+1.97%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Meta.Basic//instructions: +111.5M (+0.43%)
🟥 build/module/Lean.Meta.Constructions.BRecOn//instructions: +518.1M (+8.98%) (reduced significance based on *//lines)

nomeata · 2026-02-28T16:07:04Z

BTW, if you need the stage0 update only to get the test suite to pass, but not because of actual bootstrapping issues, you don't need the stage0 update on this branch. It suffices to leave a comment in stage0/src/stdlib_flags.h and the CI will run the test suite with stage2.

arthur-adjedj · 2026-02-28T16:12:33Z

changelog-language

src/Lean/Meta/Constructions/BRecOn.lean

nomeata · 2026-02-28T16:17:21Z

src/Lean/Meta/Basic.lean

+That is, `inductive` type in `Prop` and cannot eliminate to any `Sort u`.
+-/
+def isInductivePredicateNotSubsingleton? (declName : Name) : MetaM Bool := do
+  match (← getEnv).find? (declName ++ `rec) with


I think ++ can do the wrong thing for names with macro scopes, or something. Do we not have a mkRecName function somewhere?

We do. ++ 'rec is already used in a few other places, it might be worth fixing those too.

Let's use it here to not make things worse, but leave that cleanup elsewhere for another PR. Fixing inductives in macros maybe a larger task.

nomeata · 2026-02-28T16:18:46Z

src/Lean/Meta/Basic.lean

+Return `some info` if `declName` is an non-subsingleton inductive predicate where `info : InductiveVal`.
+That is, `inductive` type in `Prop` and cannot eliminate to any `Sort u`.
+-/
+def isInductivePredicateNotSubsingleton? (declName : Name) : MetaM Bool := do


Is this different from ”rec eliminates not into Sort”?

It's not. Is there an existing function for this ? If not, should this function be named something else ? it definitely should not end with a ?, that's a typo. Since it replaces isInductivePredicate?, I thought I would extend the naming to specifically mention non-singleton predicates, but something better is probably more sensible

Since this construction is really based off the recursor, and simply eliminates into whatever the recursor supports, that seems the more natural phrasing. Imagine people generating “recursors” in libraries at some point. Then this construction would still work and only care about the shape of the recursor.

In other places in the Lean code we do this check simply by checking if the recursor has one level parameter more than its inductive, IIRC. Not sure which check is better or it it makes a difference. It would be nice to unify these checks in one place. I'm not expecting you to do that in this PR, but if you feel like it I'll happily review that.

In other places in the Lean code we do this check simply by checking if the recursor has one level parameter more than its inductive.

I will adapt this function to do the same then.

It would be nice to unify these checks in one place

Would adding a "does its recursor eliminate to sort" field to RecursorVal be worth anything for this ? Since this is already computed when the recursor is generated initially, the changes would be minimal (similarly to your past numNested refactoring), and with that implemented, fixing #3213 would now be a one-line change .

I'm wary of changing RecursorVal, it may break meta code downstream, and things like the export format. Not worth it given that it is easy to recalculate and not on any hot path.

Rob23oba · 2026-02-28T21:03:18Z

tests/lean/run/brecOnAcc.lean

Can you test that eq_def and induct_unfolding work properly here?

mathlib-lean-pr-testing · 2026-03-01T01:05:14Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12718 has successfully built against this PR. (2026-03-01 01:05:13) View Log

nomeata · 2026-03-02T10:18:48Z

As discussed: This change is welcome in principle, but runs into existing issues in abstractNestedProof that are not straight-forward to fix (#12740). Let's revisit this when and if the issue for abstractNestedProof disappears anyways.

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 27, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 27, 2026

Update lean-toolchain for testing leanprover/lean4#12718

0c9634a

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 Feb 27, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 27, 2026

Update lean-toolchain for testing leanprover/lean4#12718

427f4a6

mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 27, 2026

feat: generalize below and brecOn on subsingletons

cf38184

arthur-adjedj force-pushed the below_subsingletons branch from 4a1dcf4 to cf38184 Compare February 28, 2026 16:10

arthur-adjedj marked this pull request as ready for review February 28, 2026 16:11

github-actions bot added the changelog-language Language features and metaprograms label Feb 28, 2026

empty commit to trigger CI again

cb7466a

nomeata reviewed Feb 28, 2026

View reviewed changes

arthur-adjedj added 4 commits February 28, 2026 17:30

use mkRecName instead of ++ 'rec

3314e98

better wording in comment

674cac9

add an assertion

e538f6d

rename and simplify isInductivePredicateNotSubsingleton

64a244b

arthur-adjedj mentioned this pull request Feb 28, 2026

fix: make sure AbstracNestedProofs.visit doesn't fail due to transparency issues #12740

Closed

Rob23oba reviewed Feb 28, 2026

View reviewed changes

test that auxiliary lemmas are generated correctly

8af067c

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 1, 2026

Update lean-toolchain for leanprover/lean4#12718

7c36484

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 1, 2026

Update lean-toolchain for leanprover/lean4#12718

cb2ad47

nomeata added the P-low We are not planning to work on this issue label Mar 2, 2026

Conversation

arthur-adjedj commented Feb 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Feb 27, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Feb 27, 2026

Uh oh!

arthur-adjedj commented Feb 28, 2026

Uh oh!

leanprover-radar commented Feb 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Feb 28, 2026

Uh oh!

arthur-adjedj commented Feb 28, 2026

Uh oh!

Uh oh!

nomeata Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

arthur-adjedj Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

nomeata Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

nomeata Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

arthur-adjedj Feb 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nomeata Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

arthur-adjedj Feb 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nomeata Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

Rob23oba Feb 28, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-lean-pr-testing bot commented Mar 1, 2026

Uh oh!

nomeata commented Mar 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

arthur-adjedj commented Feb 26, 2026 •

edited

Loading

leanprover-radar commented Feb 28, 2026 •

edited

Loading

arthur-adjedj Feb 28, 2026 •

edited

Loading

arthur-adjedj Feb 28, 2026 •

edited

Loading