perf: experiment: abstract recursors in recursor's RHSs

[nomeata]

This PR experiments with a slightly different representation of a
recursor's rules. Instead of having a rules

fun α motive rec cons {n} x xs => cons x xs (Vec.rec α motive rec cons n xs)

we leave a hole for Vec.rec α motive rec and abstract over this

fun α motive rec nil cons {n} x xs => cons x xs (rec n xs)

This could be beneficial if the recursor has many arguments (e.g. many
minor premises from an inductive with many constructors). Note that the
subexpression Vec.rec α motive rec is exactly a subterm of the
expression we are reducing. So instead of substituting every single
argument, we can substitute this subexpression as a whole, increasing
sharing and reducing the cost.

It also simplifies the kernel code for nested inductives a bit, as
recursor names don't have to be changed in the rules rhs, only in the
list of mutual recursors.

This refactoring is also in anticipation of maybe treating more
functions as primitively recursive, instead of always going all the way
to .rec.

[nomeata]

!bench

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 39bdfc6.
There were significant changes against commit 9fc18b8:

  Benchmark                 Metric          Change
  ===========================================================
+ big_beq_rec               branch-misses    -3.4%  (-57.5 σ)
+ big_beq_rec               branches         -3.1% (-205.4 σ)
+ big_beq_rec               instructions     -3.3% (-235.0 σ)
+ bv_decide_rewriter.lean   branch-misses    -1.9%  (-23.0 σ)
+ channel.lean              unbounded_seq    -1.4%
+ grind_ring_5.lean         branches        -10.6% (-824.8 σ)
+ grind_ring_5.lean         instructions    -11.2% (-831.8 σ)
+ grind_ring_5.lean         maxrss           -4.7%  (-64.0 σ)
+ mut_rec_wf                branches         -2.8% (-283.8 σ)
+ mut_rec_wf                instructions     -2.9% (-287.2 σ)
+ stdlib                    grind ac        -18.6%  (-26.8 σ)
+ stdlib                    grind dsimp     -20.3%  (-20.6 σ)
- stdlib                    grind ematch      2.3%   (40.3 σ)

[leanprover-bot]

Here are the benchmark results for commit a99a153.
There were significant changes against commit 9fc18b8:

  Benchmark                            Metric          Change
  =======================================================================
+ Std.Data.Internal.List.Associative   branch-misses    -2.5%   (-32.4 σ)
+ big_beq_rec                          branch-misses    -4.0%   (-38.9 σ)
+ big_beq_rec                          branches         -3.2%  (-306.1 σ)
+ big_beq_rec                          instructions     -3.4%  (-327.5 σ)
- big_do                               task-clock        1.6%    (66.2 σ)
- big_do                               wall-clock        1.7%    (20.1 σ)
+ grind_ring_5.lean                    branch-misses    -5.7%   (-23.1 σ)
+ grind_ring_5.lean                    branches        -10.6% (-1279.4 σ)
+ grind_ring_5.lean                    instructions    -11.2% (-1424.2 σ)
+ mut_rec_wf                           branches         -2.8%  (-185.0 σ)
+ mut_rec_wf                           instructions     -2.9%  (-199.4 σ)
+ reduceMatch                          instructions     -1.1%   (-30.9 σ)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-22 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-09-24 22:14:16)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-10548 build failed against this PR. (2025-09-24 22:18:48) View Log