feat: termination_by structural

[nomeata]

This implements the termination_by structural syntax proposed in #3909.

I went with termination_by structural over, say,
termination_by (config := {method := .structural}) mainly because it was
easier to get going (otherwise I’d have to look into how to define recursive
parsers, as Parser.config depends on term and termination_by is part of
term. But also because I find it more ergonomic and aesthetic as a user.
But syntax can still change.

The termination_by? syntax will no longer force well-founded recursion,
and instead the inferred termination_by structurally annotation will be shown
if structural termination is possible.

While I was it, this fixes #4546 the easy way (log errors about but otherwise
ignore incomplete termination_by sets for mutual recursion). Maybe we get
multiple replacements (#4551), but even then this this good behavior.

Involves a bit of shuffling around TerimationHints (now validated for a
clique already by PreDefinition.main) and TerminationArguments (now lifted
out of the WF namespace, and a bit simplified).

Fixes #3909

[nomeata]

More on my preferrence of termination_by structurally over termination_by (config := {method := .structural}):

As a user, these “record terms syntax as part of tactic syntax” feels very clumsy and heavy (not helped by the rather verbose (config := and )). This gives me the impression that setting options is meant for advanced users, for corner cases, not for “idiomatic lean”.

I get this impression for example from the fact the simp syntax offers simp only rather than simp (config := {onlyGivenTheorems := true), because simp only is a common, basic use case , while other simp options (memoize, failIfUnchanged) are clearly more advanced, and appear to be more aimed at users wrapping up the simp tactic within other user-facing tactic, or maybe even only intended for use from the MetaM level.

Maybe if the concrete syntax was a bit less heavy (no config :=, no need for := true for boolean flags) I’d come to a different conclusion.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 378b02921d930ff805b8111a1ece04abc905b963 --onto 24d51b90cc4adbc68386671bba4587d6e47188d6. (2024-06-23 16:10:10)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 378b02921d930ff805b8111a1ece04abc905b963 --onto e3578c2f36c2d4fa9cc55584a7671c0c81c70ed9. (2024-06-24 12:07:44)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 18c97926a13bfc82c9266bf00483ab13c6acb64f --onto 49249b91074a8eab8926308cedc2b3e31d973b51. (2024-06-26 12:47:09)
• ✅ Mathlib branch lean-pr-testing-4542 has successfully built against this PR. (2024-06-28 19:55:27) View Log
• ✅ Mathlib branch lean-pr-testing-4542 has successfully built against this PR. (2024-06-29 12:24:44) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7f00767b1e123f550d06a0e740bfd4e663b5c6bf --onto 4d0b7cf66c140dd83f8c8634293047335a385026. (2024-07-01 16:15:00)