feat: Guess lexicographic order for well-founded recursion

[nomeata]

This improves Lean’s capabilities to guess the termination measure for well-founded
recursion, by also trying lexicographic orders. For example:

def ackermann (n m : Nat) := match n, m with
  | 0, m => m + 1
  | .succ n, 0 => ackermann n 1
  | .succ n, .succ m => ackermann n (ackermann (n + 1) m)

now just works.

The module docstring of Lean.Elab.PreDefinition.WF.GuessLex tells the technical story.
Fixes #2837

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-14' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-14 21:53:21)
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-15' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-15 09:20:15)
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-15 12:22:42) View Log
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-15 16:19:12) View Log
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-15 18:15:41) View Log
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-16 20:50:40) View Log
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-18 14:04:44) View Log
• 💥 Mathlib branch lean-pr-testing-2874 build failed against this PR. (2023-11-20 12:23:57) View Log
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-21 18:37:16) View Log
• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-23 19:10:04)
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-24' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-24 09:32:34)
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-24 14:44:49) View Log
• ✅ Mathlib branch lean-pr-testing-2874 has successfully built against this PR. (2023-11-24 21:53:00) View Log

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit f3344ff.Found no runs to compare against.

[nomeata]

Whohoo, only one bug found via the lean test suite, and mathlib goes through on the first attempt :-)

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit e8b6cb3.
There were significant changes against commit 6d34920:

  Benchmark   Metric             Change
  ================================================
- stdlib      instructions         1.1% (2531.8 σ)
- stdlib      tactic execution    24.1%   (52.1 σ)
- stdlib      task-clock           1.2%   (12.2 σ)
- stdlib      wall-clock           1.9%   (56.6 σ)

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 64a8074.
There were significant changes against commit 260eaeb:

  Benchmark          Metric             Change
  =====================================================
- lake build no-op   instructions         2.4% (12.0 σ)
- stdlib             tactic execution    24.6% (51.5 σ)
- stdlib             task-clock           1.8% (20.5 σ)

[nomeata]

Here is the result for mathlib, if I got the commits right (it is quite tedious to do, or I am doing it wrong):

http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/f161591d-fb4a-4c72-94a9-b135d8792111?hash1=704bcb215266194da60944c1d5b5a98ede38c00b

I don't know how to read these reports yet. It seems that on mathlib there is no stderiv, and thus I cannot sort the table by regression?

In any case, it seems that the optimization in #2954 kicks in often enough to fix the mathlib regressions:

http://speed.lean-fro.org/mathlib4/compare/d34337f5-8cfa-430f-b5f6-24c006af430f/to/8aaf42b2-530f-4486-8137-ca90aa25563c