feat: support for lambda expressions in discr trees

[Rob23oba]

This PR adds support for lambda expressions in discrimination trees (Lean.Meta.DiscrTree). This means that a lot more specialization can be applied in discrimination trees than before. Examples:

-- previously
#discr_tree_key fun x => x -- `<other>`
#discr_tree_simp_key bind_pure_comp -- @bind _ _ _ _ _ <other>
#discr_tree_simp_key List.foldlM_pure -- @List.foldlM _ _ _ _ <other> _ _
#discr_tree_simp_key List.foldr_cons_eq_append -- @List.foldr _ (List _) <other> _ _
-- now
#discr_tree_key fun x => x -- fun _
#discr_tree_simp_key bind_pure_comp -- @bind _ _ _ _ _ (fun @pure _ _ _ _)
#discr_tree_simp_key List.foldlM_pure -- @List.foldlM _ _ _ _ (fun fun @pure _ _ _ _) _ _
#discr_tree_simp_key List.foldr_cons_eq_append -- @List.foldr _ (List _) (fun @List.cons _ _) _ _

[nomeata]

NB that there is related work in mathlib, in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.html#Lean.Meta.RefinedDiscrTree

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-8395 build failed against this PR. (2025-05-19 12:51:35) View Log
• 💥 Mathlib branch lean-pr-testing-8395 build failed against this PR. (2025-05-19 15:36:46) View Log
• 💥 Mathlib branch lean-pr-testing-8395 build failed against this PR. (2025-05-19 15:57:12) View Log
• 💥 Mathlib branch lean-pr-testing-8395 build failed against this PR. (2025-05-19 16:04:57) View Log
• 💥 Mathlib branch lean-pr-testing-8395 build failed against this PR. (2025-05-19 16:47:50) View Log

[leodemoura]

We have decided to not support lambda in the DiscrTree type in core. Please consider contributing this PR to RefinedDiscrTree in Mathlib.

[Rob23oba]

What was the particular reason for this decision? The impact on downstream projects?

[leodemoura]

What was the particular reason for this decision? The impact on downstream projects?

There are several reasons for my decision:

• This is a performance-critical file that is used by multiple core modules in Lean.
• I currently maintain this file, and I’m not satisfied with its performance. I plan to make further changes to it.
• In my experience, files modified by many different authors tend to accumulate subtle bugs.
• Discrimination trees are inherently syntactic, but Lean relies on dependent type theory and definitional equality. We've found a compromise that isn't perfect but works reasonably well. Supporting lambdas would introduce additional complexity and potential issues. I've had to debug similar changes in the past.
• I'm currently overwhelmed with responsibilities and don’t have the bandwidth to context-switch when external contributors modify core components. I’m happy to support contributions that are self-contained or affect less critical parts of the system.
• We don't yet have a strong benchmark suite. While Mathlib is an important use case, it's not the only one we need to support.
• Finally, there's another module called LazyDiscrTree, and we aim to keep it in sync with this one.

I appreciate your interest and contributions to Lean. If you're looking for areas where help is especially welcome, I’d be happy to suggest something.