fix: avoid unnecessary branching in match compilation

[nomeata]

This PR improves match compilation: Branch on variables in the order
suggested by the first remaining alternative, and do not branch when the
first remaining alternative does not require it. This fixes #10749. With set_option backwards.match.rowMajor false the old behavior can be turned on.

(For now this is an experiment to get familiar with the code and the whole
problem domain. It is likely overly naive.)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-12 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-13 16:42:25)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-21 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-21 12:34:16)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-29 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-29 13:44:19)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e2f5938e74276a12dbfe235b280e3ff38e4533c2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-30 03:05:07)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-30 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-30 20:14:28)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-10763 build failed against this PR. (2025-10-13 17:33:10) View Log
• ✅ Mathlib branch lean-pr-testing-10763 has successfully built against this PR. (2025-10-14 13:06:25) View Log
• ✅ Mathlib branch lean-pr-testing-10763 has successfully built against this PR. (2025-10-21 13:29:54) View Log
• ✅ Mathlib branch lean-pr-testing-10763 has successfully built against this PR. (2025-10-21 14:42:10) View Log
• ✅ Mathlib branch lean-pr-testing-10763 has successfully built against this PR. (2025-10-29 14:45:25) View Log
• ✅ Mathlib branch lean-pr-testing-10763 has successfully built against this PR. (2025-10-29 22:31:23) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2f5938e74276a12dbfe235b280e3ff38e4533c2 --onto 106b0fa661d96fd1fa6ff96e2ee5f55f23f307f2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-30 03:05:06)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-10-30 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-10-30 20:14:26)

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 41f4465 against efbbb0b are in! @nomeata

[leanprover-bot]

Here are the benchmark results for commit d16a7bf.
There were significant changes against commit efbbb0b:

  Benchmark                            Metric          Change
  =======================================================================
+ Init.Data.List.Sublist re-elab -j4   maxrss           -1.1%   (-61.7 σ)
+ channel.lean                         unbounded_seq    -4.0%
+ const_fold                           instructions     -8.1%  (-112.4 σ)
+ omega_stress.lean async              branch-misses   -11.9%   (-47.3 σ)
+ omega_stress.lean async              branches        -12.4% (-1142.0 σ)
+ omega_stress.lean async              instructions    -12.9% (-1001.0 σ)
+ omega_stress.lean async              task-clock      -13.0%   (-27.7 σ)
+ omega_stress.lean async              wall-clock      -13.7%   (-43.6 σ)
- stdlib                               type checking     2.0%    (22.2 σ)

[nomeata]

That’s neat:

+ const_fold                           instructions     -8.1%  (-112.4 σ)
+ omega_stress.lean async              instructions    -12.9% (-1001.0 σ)

[nomeata]

!radar

[leanprover-radar]

Benchmark results for c993f9b against efbbb0b are in! @nomeata

[nomeata]

I’m inclined to merge this, with test suite and mathlib passing and performance gains to be gained. I expect that there are tricky matches that may break with this, but probably for any of these one can construct one that works only with this change. There is a backwards option in place.

[nomeata]

!radar

[leanprover-radar]

Benchmark results for 2dc3d5a against 705084d are in! @nomeata

Major changes (3)

• const_fold//instructions changed by -8.1% (✅).
• omega_stress.lean async//instructions changed by -13.0% (✅).
• workspaceSymbols with new ranges//instructions changed by +2.3% (🟥).

Minor changes (1)

• deriv//instructions changed by -0.7% (✅).