refactor: structural recursion: prove .eq_def directly

[nomeata]

This PR changes how Lean proves the equational theorems for structural recursion. The core idea is to let-bind the f argument to brecOn and rewriting .brecOn with an unfolding theorem. This means no extra case split for the .rec in .brecOn is needed, and simp doesn't change the f argument which can break the definitional equality with the defined function. With this, we can prove the unfolding theorem first, and derive the equational theorems from that, like for all other ways of defining recursive functions.

Backs out the changes from #10415, the old strategy works well with the new goals.

Fixes #5667
Fixes #10431
Fixes #10195
Fixes #2962

[nomeata]

Still getting two failures with functions that have match statements that don’t split well with too much stuff in the context.

Possible fix: Undo the changes in #10415, unfold both sides (now that we know how to keep f out of view) and relate the two sides in lockstep, without accumulating unnecessary terms from if-then-else or match splitting in the context.

[nomeata]

Possible fix: Undo the changes in #10415, unfold both sides (now that we know how to keep f out of view) and relate the two sides in lockstep, without accumulating unnecessary terms from if-then-else or match splitting in the context.

Just undoing #10415 alone does not help, the same two test cases still fail

Got confused juggling stages, seems to help with one but not the other failing test.

I still wonder if we need a way to relate two instances of the same match, with different motives, more directly than splitting one and rewriting the other one.

dumping some partial thought experiments here, gotta go now

def foo (n : Nat) := match  n with
  | 0 => 0
  | 1 => 1
  | _ => 3

theorem foo.match_1.app {α : Nat → Sort u} {β : Nat → Sort u}
  (alt1 : Unit → α 0) (alt2 : Unit → α 1) (alt3 : ∀ n, α n)
 (f : ∀ n, α n → β n) (n : Nat) :
  f n (foo.match_1 (motive := fun n => α n) n alt1 alt2 alt3) =
    foo.match_1 (motive := fun n => β n) n
      (fun _ => f 0 (alt1 ())) (fun _ => f 1 (alt2 ())) (fun n => f n (alt3 n)) := by
  split <;> rfl

theorem foo.match_1.cases {α : Nat → Sort u}
  (alt1 : Unit → α 0) (alt2 : Unit → α 1) (alt3 : ∀ n, α n)
  (P : ∀ {n}, α n → Prop) (n : Nat)
  (halt1 : P (alt1 ())) (halt2 : P (alt2 ())) (halt3 : P (alt3 n)) :
  P (foo.match_1 (motive := fun n => α n) n alt1 alt2 alt3) := by
  split <;> assumption

theorem foo.match_1.app' {α : Nat → Sort u} {β : Nat → Sort u}
  (alt1 : Unit → α 0) (alt2 : Unit → α 1) (alt3 : ∀ n, α n)
 (f : ∀ n, α n → β n) (n : Nat) :
  f n (foo.match_1 (motive := fun n => α n) n alt1 alt2 alt3) =
    foo.match_1 (motive := fun n => β n) n
      (fun _ => f 0 (alt1 ())) (fun _ => f 1 (alt2 ())) (fun n => f n (alt3 n)) := by
 show
    foo.match_1 (motive := fun n => (α n → β n → Prop) → Prop) n
      (fun _ k => k (alt1 ()) (f 0 (alt1 ())))
      (fun _ k => k (alt2 ()) (f 1 (alt2 ())))
      (fun n k => k (alt3 n) (f n (alt3 n)))
      (fun lhs rhs => f n lhs = rhs)
 apply foo.match_1.cases

[nomeata]

Actually, the remaining test that fails seems to be related to module system issues:

[split.failure] `split` tactic failed at
      match x✝¹, x✝, h with
      | L.nil, L.nil, ⋯ => true
      | L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && instBEqL.beq a_1 a'_1
    Unknown constant `_private.external:file:///home/joachim/lean4/tests/lean/run/structuralEqns5.lean.0.L.match_on_same_ctor.splitter✝`
    
    Note: A private declaration `L.match_on_same_ctor.splitter✝` (from the current module) exists but would need to be public to access here.

so maybe this is a good direction here.

---

ah, yes, “forgetting withoutExporting” is the new “forgetting to instantiateMVars”. Let’s see now…

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-29 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-09-30 13:16:09)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 24c86fc05d5abeb147be04275fe6945d39f6b8c3 --onto d88e417cda0f7afb1e15c806c6bfdbbb09ba7eef. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-02 13:15:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5a2e46b0211ad353399b21af4be9edbe65c32b72 --onto 0b2193c7715a55246d0596a4db548c1b5b81562a. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-02 15:46:01)
• 💥 Mathlib branch lean-pr-testing-10606 build failed against this PR. (2025-10-06 15:19:02) View Log
• ✅ Mathlib branch lean-pr-testing-10606 has successfully built against this PR. (2025-10-06 17:47:41) View Log
• ✅ Mathlib branch lean-pr-testing-10606 has successfully built against this PR. (2025-10-07 12:32:54) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-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-09-30 13:16:11)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 24c86fc05d5abeb147be04275fe6945d39f6b8c3 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-02 13:15:46)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5a2e46b0211ad353399b21af4be9edbe65c32b72 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-02 15:46:03)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-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-10-06 15:13:10)
• 🟡 Reference manual branch lean-pr-testing-10606 build against this PR didn't complete normally. (2025-10-07 11:40:43) View Log
• ✅ Reference manual branch lean-pr-testing-10606 has successfully built against this PR. (2025-10-07 11:40:45) View Log

[nomeata]

How could switching to the default equation generation break splitting this match with this error message 😕

[Elab.definition.eqns] cannot split on match k, ⋯, hk with
    | k.succ, x, hk => if h : i % 2 = 0 then trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1) else acc
    AppBuilder for `eq_of_heq`, heterogeneous equality types are not definitionally equal
      k_2.succ = 0 → False
    is not definitionally equal to
      k_2.succ ≠ 0 

[leanprover-radar]

Benchmark results for 81874c9 against fbfb075 are in! @nomeata

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 7785875 against fbfb075 are in! @nomeata

[leanprover-bot]

Here are the benchmark results for commit 81874c9.
There were significant changes against commit fbfb075:

  Benchmark                 Metric                     Change
  =====================================================================
- Init size                 bytes .olean                 5.6%
- big_beq_rec               branches                     4.5% (304.9 σ)
- big_beq_rec               instructions                 4.9% (335.2 σ)
- big_deceq_rec             branches                     1.2% (155.2 σ)
- big_deceq_rec             instructions                 1.3% (142.3 σ)
- iterators (interpreted)   maxrss                       1.0%  (35.3 σ)
- lake config elab          maxrss                       1.3%  (54.7 σ)
- lake config import        maxrss                       1.2%  (30.8 σ)
- lake config tree          maxrss                       1.3%  (87.5 σ)
- lake env                  maxrss                       1.2%  (40.0 σ)
- mut_rec_wf                branches                     4.0% (731.1 σ)
- mut_rec_wf                instructions                 4.3% (558.0 σ)
+ reduceMatch               instructions                -1.8% (-80.7 σ)
+ stdlib                    grind ring                 -19.6% (-28.6 σ)
- stdlib                    number of imported bytes     4.9%
- stdlib size               bytes .olean                 4.1%

[leanprover-bot]

Here are the benchmark results for commit 7785875.
There were significant changes against commit fbfb075:

  Benchmark            Metric                     Change
  ================================================================
- Init size            bytes .olean                 5.6%
- big_beq_rec          branches                     2.4%  (74.5 σ)
- big_beq_rec          instructions                 2.6%  (77.4 σ)
+ grind_ring_5.lean    task-clock                  -2.5% (-22.1 σ)
+ grind_ring_5.lean    wall-clock                  -2.4% (-32.4 σ)
- lake config elab     maxrss                       1.2%  (28.6 σ)
- lake config import   maxrss                       1.1%  (22.8 σ)
- lake config tree     maxrss                       1.1%  (44.7 σ)
- lake env             maxrss                       1.1%  (31.2 σ)
- mut_rec_wf           branches                     2.2%  (84.7 σ)
- mut_rec_wf           instructions                 2.3%  (80.8 σ)
+ reduceMatch          instructions                -1.8% (-35.1 σ)
- riscv-ast.lean       wall-clock                   1.2%  (92.3 σ)
- stdlib               blocked (unaccounted)        4.7%  (25.0 σ)
+ stdlib               grind ac                   -10.5% (-23.8 σ)
+ stdlib               grind ring                 -23.6% (-28.6 σ)
- stdlib               number of imported bytes     4.9%
- stdlib size          bytes .olean                 4.1%