perf: sparse case splitting in match compilation

[nomeata]

This PR lets the match compilation procedure use sparse case analysis when the patterns only match on some but not all constructors of an inductive type. This way, less code is produce. Before, code handling each of the other cases was then optimized and commoned-up by later compilation pipeline, but that is wasteful to do.

In some cases this will prevent Lean from noticing that a match statement is complete
because it performs less case-splitting for the unreachable case. In this case, give explicit
patterns to perform the deeper split with by contradiction as the right-hand side.

At least temporarily, there is also the option to disable this behaviour with

set_option backwards.match.sparseCases false

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-13 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-10-17 16:00:47)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c7f57d6a0ba345296085ce3eceeb1430eefe1984 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-30 22:20:00)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-02 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-03 17:25:46)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0cb79868f4b80a8018a7737bf53e54760443f906 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-05 18:43:01)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-06 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-06 10:19:40)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7459304e98cedfa25f7e1e1774a7bbe84ae65c00 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-06 13:42:15)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-10823 build failed against this PR. (2025-10-17 16:13:47) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7f57d6a0ba345296085ce3eceeb1430eefe1984 --onto 705084d9ba258dec704af428d7ce2444525f9ffb. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-30 22:19:58)
• 💥 Mathlib branch lean-pr-testing-10823 build failed against this PR. (2025-11-03 18:24:29) View Log
• ✅ Mathlib branch lean-pr-testing-10823 has successfully built against this PR. (2025-11-03 19:37:28) View Log
• ✅ Mathlib branch lean-pr-testing-10823 has successfully built against this PR. (2025-11-04 02:01:38) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0cb79868f4b80a8018a7737bf53e54760443f906 --onto e7f4f98071c001e11adfabbea1b277782c7bb3a4. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-05 18:42:59)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-06 10:19:38)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7459304e98cedfa25f7e1e1774a7bbe84ae65c00 --onto e6b1f1984c27d26d2b9dd29fc7c24129a4ba99da. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-06 13:42:13)

[nomeata]

!radar

[leanprover-radar]

Benchmark results for bf1254a against 0cb7986 are in! @nomeata

Major changes (3)

• reduceMatch//instructions changed by +4.8% (🟥).
• stdlib size//bytes .olean.private changed by +1.2% (🟥).
• workspaceSymbols//instructions changed by +3.8% (🟥).

Minor changes (5)

• rbmap_library//instructions changed by -1.5% (✅).
• stdlib size//bytes .olean changed by +0.4% (🟥).
• stdlib size//bytes .olean.server changed by -0.3% (✅).
• stdlib size//lines C changed by +0.2% (🟥).
• stdlib//number of imported entries changed by +0.7% (🟥).

[nomeata]

!radar

[leanprover-radar]

Benchmark results for e3dcf75 against 7459304 are in! @nomeata

Major changes (3)

• rbmap_library//instructions changed by -1.5% (✅).
• reduceMatch//instructions changed by +4.9% (🟥).
• stdlib size//bytes .olean.private changed by +1.2% (🟥).

Minor changes (4)

• stdlib size//bytes .olean changed by +0.4% (🟥).
• stdlib size//bytes .olean.server changed by -0.3% (✅).
• stdlib size//lines C changed by +0.2% (🟥).
• stdlib//number of imported entries changed by +0.7% (🟥).