feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures

[wkrozowski]

This PR adds a cbv_simproc system for the cbv tactic, mirroring simp's simproc infrastructure but tailored to cbv's three-phase pipeline (↓ pre, cbv_eval eval, ↑ post). User-defined simplification procedures are indexed by discrimination tree patterns and dispatched during cbv normalization.

New syntax:

• cbv_simproc [↓|↑|cbv_eval] name (pattern) := body — define and register a cbv simproc
• cbv_simproc_decl name (pattern) := body — define without registering
• attribute [cbv_simproc [↓|↑|cbv_eval]] name — register an existing declaration
• builtin_cbv_simproc variants for the internal use

New files:

• src/Init/CbvSimproc.lean — syntax and macros
• src/Lean/Meta/Tactic/Cbv/CbvSimproc.lean — types, env extensions, registration, dispatch
• src/Lean/Elab/Tactic/CbvSimproc.lean — pattern elaboration and command elaborators

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1f03e3252001a9a5cdfb354bfc45895d047bf4ff --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-19 16:56:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8ed6b30084dfc1d2fe303dbc7a8d1c435dac6655 --onto e7e3588c973226e85d79ed0f3154cfca79b61c6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 15:51:50)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8ed6b30084dfc1d2fe303dbc7a8d1c435dac6655 --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 10:31:42)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-04 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. (2026-03-04 13:01:04)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-05 12:28:58)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1f03e3252001a9a5cdfb354bfc45895d047bf4ff --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-19 16:56:15)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8ed6b30084dfc1d2fe303dbc7a8d1c435dac6655 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 15:51:53)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-04 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. (2026-03-04 13:01:06)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-05 12:29:00)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-09 20:40:31)