feat: float_match simproc and conv tactic

[nomeata]

This PR adds the float_match simproc and conv tactic.

This adds the ability float matches “up” (or equivalently push context into matches): For example, this allows to rewrite

f (match o with | some x => x + 1 | none => 0)

to

match o with | some x => f (x + 1) | none => f 0

One motivation are proofs like the following, where we are pushing a function (here, map f) “down” through another function, and that should be provable just by rewriting, without using split:

theorem List.filter_map' : filter p (map f l) = map f (filter (p ∘ f) l) := by
  induction l <;> simp [filter, *, float_match]

This adds

• foo.match_1.float, a (lazily realizable) theorem for each matcher that performs the rewrite above for an arbitrary f
• a float_match simproc
• a float_match conv tactic

For the purpose of these simprocs and tactics, ite and dite are considered a matcher.

The simproc only floats out through one function at a time, and only into Type context, not Prop-context. This is to prevent the write

    (match o with | some x => x + 1 | none => 0) = rhs
==> (match o with | some x => (x + 1) = rhs | none => 0  = rhs)

which is not wrong and may sometimes actually work, but in order to be useful reliably this would require more work (in particular strong contextual congruence rules for matchers that in particular allow to rewrite match statements inside the alts). The conv tactic does not have this restriction.

This is inspired by the “splitter” in Isabelle’s simplifier (https://stackoverflow.com/a/47124021/946226).

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5923 has successfully built against this PR. (2024-11-02 00:07:13) View Log
• ✅ Mathlib branch lean-pr-testing-5923 has successfully built against this PR. (2024-11-02 13:41:26) View Log
• ✅ Mathlib branch lean-pr-testing-5923 has successfully built against this PR. (2024-11-04 11:51:21) View Log
• ✅ Mathlib branch lean-pr-testing-5923 has successfully built against this PR. (2024-11-04 14:44:44) View Log
• ✅ Mathlib branch lean-pr-testing-5923 has successfully built against this PR. (2024-11-04 15:46:46) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 970dc6f7aac1ceb16c5324f0f8c0230dab879fd6 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 12:14:27)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 14c3d4b1a6cd6b9a755c952a2fa8f4c205c4b3e4 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 10:21:58)