refactor: use match compilation to generate splitter #11220

nomeata · 2025-11-17T17:40:04Z

This PR changes how match splitters are generated: Rather than rewriting the match statement, the match compilation pipeline is used again.

The benefits are:

Re-doing the match compilation means we can do more intelligent book keeping, e.g. prove overlap assumptions only once and re-use the proof, or prune the context of the MVar to speed up contradiction. This may have allowed a different solution than perf: use Nat-based bitmask in sparse cases construction #11200.
It would unblock feat: experiment: dividing match compilation #11105, as the existing splitter implementation would have trouble dealing with the matchers produced that way.
It provides the necessary machinery also for source-exposed “none of the above” bindings, a feature that we probably want at some point (and we mostly need to find good syntax for, see RFC: Overlapping matches and termination proofs #3136, although maybe I should open a dedicated RFC).
It allows us to skip costly things during matcher creation that would only be useful for the splitter, and thus allows performance improvements like perf: when matching on values, avoid generating hyps when not needed #11508.
We can drop the existing implementation.

It’s not entirely free:

We have to run simpH twice, once for the match equations and once for the splitter.

This PRs lets `realizeConst` use `withDeclNameForAuxNaming` so that auxilary definitions created there get non-clashing names.

nomeata · 2025-11-17T17:50:59Z

!radar

leanprover-radar · 2025-11-17T17:51:05Z

Benchmark results for 04c56b3 against ef1dc21 are in! @nomeata

Major changes (3)

big_match//instructions changed by +18.2% (🟥).
mut_rec_wf//instructions changed by +2.6% (🟥).
tests/compiler//sum binary sizes changed by +0.9% (🟥).

Minor changes (2)

Init.Data.List.Sublist async//instructions changed by +0.6% (🟥).
omega_stress.lean async//instructions changed by +0.6% (🟥).

…chim/splitter-via-match

leanprover-bot · 2025-11-17T19:49:48Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-16 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. (2025-11-17 19:49:47)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-17 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. (2025-11-18 11:41:12)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 03eb2f73ac1ee83e720b80081c6c1b4580d2a914 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-19 09:53:31)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-20 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. (2025-11-20 10:43:56)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-04 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. (2025-12-04 09:43:24)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e548fa414cb74db21a31afe6c26cb0c51310f1db --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-04 11:38:23)

leanprover-community-bot · 2025-11-17T20:48:22Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-11220 has successfully built against this PR. (2025-11-17 20:48:20) View Log
✅ Mathlib branch lean-pr-testing-11220 has successfully built against this PR. (2025-11-18 12:44:13) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 03eb2f73ac1ee83e720b80081c6c1b4580d2a914 --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-19 09:53:29)
❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-11-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 10:43:55)
✅ Mathlib branch lean-pr-testing-11220 has successfully built against this PR. (2025-11-21 12:21:26) View Log
❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-12-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 09:43:23)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e548fa414cb74db21a31afe6c26cb0c51310f1db --onto 0173444d24df9253d7947cfe82519e4a6caffd3a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 11:38:21)

…lean4 into joachim/splitter-via-match

This PR extracts two modules from `Match.MatchEqs`, in preparation of #11220 and to use the module system to draw clear boundaries between concerns here.

This PR allows setting reducibilityCoreExt in async contexts (e.g. when using `mkSparseCasesOn` in a realizable definition)

…match

nomeata · 2025-11-21T09:32:23Z

!radar

leanprover-radar · 2025-11-21T09:32:26Z

Benchmark results for 9bb4009 against a106ea0 are in! @nomeata

Major changes (1)

big_match_partial//instructions changed by -2.0% (✅).

Minor changes (2)

Init.Data.List.Sublist async//instructions changed by +0.5% (🟥).
omega_stress.lean async//instructions changed by +0.6% (🟥).

This PR adds two benchmarks for elaborating match statements of many `Nat` literals, one without and one with splitter generation.

…chim/bench-nat-match

nomeata · 2025-12-04T08:05:25Z

!radar

leanprover-radar · 2025-12-04T08:05:40Z

Benchmark results for 4988c6e against dd28f00 are in! @nomeata

Major changes (1)

✅ big_match_partial//instructions: -381.3M (-2.1%)

Minor changes (5)

🟥 Init.Data.List.Sublist async//instructions: +72.3M (+0.6%)
🟥 Init.Prelude async//instructions: +68.7M (+0.5%)
🟥 channel.lean//instructions: +276.5M (+0.7%)
🟥 lake config elab//instructions: +17.7M (+0.5%)
🟥 omega_stress.lean async//instructions: +32.2M (+0.6%)

…chim/splitter-via-match

nomeata · 2025-12-04T10:17:06Z

!radar

leanprover-radar · 2025-12-04T10:17:12Z

Benchmark results for 4988c6e against dd28f00 are in! @nomeata

Major changes (1)

✅ big_match_partial//instructions: -381.3M (-2.1%)

Minor changes (5)

🟥 Init.Data.List.Sublist async//instructions: +72.3M (+0.6%)
🟥 Init.Prelude async//instructions: +68.7M (+0.5%)
🟥 channel.lean//instructions: +276.5M (+0.7%)
🟥 lake config elab//instructions: +17.7M (+0.5%)
🟥 omega_stress.lean async//instructions: +32.2M (+0.6%)

nomeata · 2025-12-04T10:17:14Z

!radar

leanprover-radar · 2025-12-04T10:17:19Z

Benchmark results for 035b886 against e548fa4 are in! @nomeata

Major changes (2)

✅ big_match_nat_split//instructions: -2.2G (-6.4%)
✅ big_match_partial//instructions: -377.0M (-2.1%)

Minor changes (3)

🟥 Init.Data.List.Sublist async//instructions: +70.0M (+0.5%)
🟥 lake config elab//instructions: +16.9M (+0.5%)
🟥 omega_stress.lean async//instructions: +33.2M (+0.6%)

This PR avoids generating hyps when not needed (i.e. if there is a catch-all so no completeness checking needed) during matching on values. This tweak was made possible by #11220.

…11508) This PR avoids generating hyps when not needed (i.e. if there is a catch-all so no completeness checking needed) during matching on values. This tweak was made possible by #11220.

This PR changes how match splitters are generated: Rather than rewriting the match statement, the match compilation pipeline is used again. The benefits are: * Re-doing the match compilation means we can do more intelligent book keeping, e.g. prove overlap assumptions only once and re-use the proof, or prune the context of the MVar to speed up `contradiction`. This may have allowed a different solution than #11200. * It would unblock #11105, as the existing splitter implementation would have trouble dealing with the matchers produced that way. * It provides the necessary machinery also for source-exposed “none of the above” bindings, a feature that we probably want at some point (and we mostly need to find good syntax for, see #3136, although maybe I should open a dedicated RFC). * It allows us to skip costly things during matcher creation that would only be useful for the splitter, and thus allows performance improvements like #11508. * We can drop the existing implementation. It’s not entirely free: * We have to run `simpH` twice, once for the match equations and once for the splitter.

…11508) This PR avoids generating hyps when not needed (i.e. if there is a catch-all so no completeness checking needed) during matching on values. This tweak was made possible by #11220.

nomeata added 7 commits November 17, 2025 14:39

Stash

a1155de

stash

6b29b12

Add file

e8d867b

progress

1cb7527

Seems to work

05521de

Remove dead code

04c56b3

fix: let realizeConst run withDeclNameForAuxNaming

9efa483

This PRs lets `realizeConst` use `withDeclNameForAuxNaming` so that auxilary definitions created there get non-clashing names.

nomeata changed the base branch from master to nightly-with-mathlib November 17, 2025 17:50

nomeata changed the title ~~refactor: Use match compilation to generate splitter~~ refactor: use match compilation to generate splitter Nov 17, 2025

nomeata added 5 commits November 17, 2025 18:56

Add test case

577fb91

Merge branch 'joachim/realizeConst_withDeclNameForAuxNaming' into joa…

6d7b71e

…chim/splitter-via-match

Not needed

c8d1b46

More dead code

ab44217

Spurious newline

0b9db11

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 17, 2025

Update lean-toolchain for testing leanprover/lean4#11220

68933c0

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 17, 2025

Update lean-toolchain for testing leanprover/lean4#11220

dc56b80

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 17, 2025

nomeata added 2 commits November 18, 2025 10:34

Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…

e69c1da

…lean4 into joachim/splitter-via-match

refactor: extract functionality from Match.MatchEqs

6ebb738

This PR extracts two modules from `Match.MatchEqs`, in preparation of #11220 and to use the module system to draw clear boundaries between concerns here.

nomeata mentioned this pull request Nov 18, 2025

refactor: extract functionality from Match.MatchEqs #11236

Merged

Merge branch 'joachim/splitter-refactor' into joachim/splitter-via-match

73be069

nomeata mentioned this pull request Nov 18, 2025

splitter does not thunk argument-less alternatives #11211

Closed

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 18, 2025

Update lean-toolchain for leanprover/lean4#11220

f80f38d

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 18, 2025

Update lean-toolchain for leanprover/lean4#11220

c062e48

nomeata added 6 commits November 20, 2025 10:02

Avoid needsSplitter field

a1854d1

Reduce diff

230fb8b

Don’t add splitter to matcherExt

5aebd96

feat: allow setting reducibilityCoreExt in async contexts

f828fd5

This PR allows setting reducibilityCoreExt in async contexts (e.g. when using `mkSparseCasesOn` in a realizable definition)

Merge branch 'joachim/reducibility-replay' into joachim/splitter-via-…

2247c98

…match

Remove unused code, move common code to helper modules

9bb4009

nomeata marked this pull request as ready for review November 21, 2025 10:38

nomeata requested a review from leodemoura as a code owner November 21, 2025 10:38

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 21, 2025

Update lean-toolchain for leanprover/lean4#11220

46d7506

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 21, 2025

Update lean-toolchain for leanprover/lean4#11220

05ae79c

nomeata added 3 commits December 4, 2025 08:58

test: add big match on nat lit benchmarks

d1d23b8

This PR adds two benchmarks for elaborating match statements of many `Nat` literals, one without and one with splitter generation.

Merge branch 'master' of https://github.com/leanprover/lean4 into joa…

caf137c

…chim/bench-nat-match

Merge branch 'joachim/bench-nat-match' into joachim/splitter-via-match

4988c6e

Merge branch 'master' of https://github.com/leanprover/lean4 into joa…

035b886

…chim/splitter-via-match

nomeata mentioned this pull request Dec 4, 2025

perf: when matching on values, avoid generating hyps when not needed #11508

Merged

nomeata added this pull request to the merge queue Dec 4, 2025

Merged via the queue into master with commit af6d207 Dec 4, 2025
18 checks passed

refactor: use match compilation to generate splitter #11220

refactor: use match compilation to generate splitter #11220

Uh oh!

Conversation

nomeata commented Nov 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Nov 17, 2025

Uh oh!

leanprover-radar commented Nov 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Nov 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-community-bot commented Nov 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Nov 21, 2025

Uh oh!

leanprover-radar commented Nov 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Dec 4, 2025

Uh oh!

leanprover-radar commented Dec 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Dec 4, 2025

Uh oh!

leanprover-radar commented Dec 4, 2025

Uh oh!

nomeata commented Dec 4, 2025

Uh oh!

leanprover-radar commented Dec 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

nomeata commented Nov 17, 2025 •

edited

Loading

leanprover-radar commented Nov 17, 2025 •

edited

Loading

leanprover-bot commented Nov 17, 2025 •

edited

Loading

leanprover-community-bot commented Nov 17, 2025 •

edited

Loading

leanprover-radar commented Nov 21, 2025 •

edited

Loading

leanprover-radar commented Dec 4, 2025 •

edited

Loading

leanprover-radar commented Dec 4, 2025 •

edited

Loading