feat: GuessLex: print inferred termination argument

[nomeata]

With

set_option showInferredTerminationBy true

this prints a message like

Inferred termination argument:
termination_by
  ackermann n m => (sizeOf n, sizeOf m)

it tries hard to use names that

• match the names that the user used, if present
• have no daggers (so that it can be copied)
• do not shadow each other
• do not shadow anything from the environment (just to be nice)

it does so by appending sufficient ' to the name.

Some of the emitted sizeOf calls are unnecessary, but they are needed
sometimes with dependent parameters. A follow-up PR will not emit them
for non-dependent arguments, so that in most cases the output is pretty.

Somewhen down the road we also want a code action, maybe triggered by
termination_by?. This should come after #2921, as that simplifies that
feature (no need to merge termination arguments from different cliques
for example.)

[nomeata]

This seems to work, but there may be room for refinements:

• Is this a good name for the option?

• Is the way I generate fresh, accessible names appropriate?

• Why does

  let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
  

  not remove the local namespace in

  termination_by
    VarNames.shadow1 x2 x2 => sizeOf x2
  

[nomeata]

Ok, figued out the last question myself :-)

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-3012 has successfully built against this PR. (2023-12-02 12:46:33) View Log
• ✅ Mathlib branch lean-pr-testing-3012 has successfully built against this PR. (2023-12-02 13:23:17) View Log
• ✅ Mathlib branch lean-pr-testing-3012 has successfully built against this PR. (2023-12-04 18:43:16) View Log
• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-05 09:45:31)

[nomeata]

I built mathlib with the option set to true, these the termination metrics that are printed:

termination_by
  aux i j H b => sizeOf i
termination_by
  SatisfiesM_foldlM.go i j b h₁ h₂ H => sizeOf i
termination_by
  takeWhile₂_eq_takeWhile₂TR.go as bs acca accb => sizeOf as
termination_by
  zoom_ins path t' path' t cmp => sizeOf t
termination_by
  zoom_del cut path t' path' t => sizeOf t
termination_by
  firstDiffPos_loop_eq l₁ l₂ r₁ r₂ stop p hl₁ hl₂ hstop => sizeOf r₁
termination_by
  splitAux_of_valid l m r acc => sizeOf r
termination_by
  succ_div x1 x2 => sizeOf x1
termination_by
  mem_of_subset' x1 x2 x3 x4 => sizeOf x1
termination_by
  maxPowDiv.go k p n => sizeOf n
termination_by
  go_succ k p n => sizeOf n
termination_by
  xgcdAux x1 x2 x3 x4 x5 x6 => sizeOf x1
termination_by
  decidableEq x1 x2 => sizeOf x1
termination_by
  interleave x1 x2 => sizeOf x1
termination_by
  append_bind xs ys f => sizeOf xs
termination_by
  ltb s₁ s₂ => sizeOf s₁
termination_by
  inductionOn it₁ it₂ ind eq base₁ base₂ => sizeOf it₁
termination_by
  cprankMax_add x1 x2 x3 x4 x5 x6 => sizeOf x1
termination_by
  exists_subgroup_card_pow_prime_le x1 x2 x3 => sizeOf x2

Only 19 definitions in all of mathlib need the decreasing argument to be guessed (all others are either structural, have an explicit terminating_by or have only one plausible argument). That’ll make me write more tests :-)

None of these use more than one argument, which is expected, as until very recently, a definition that needed a lexicographic argument would not be accepted.

There are 33 termination_by annotations that were necessary before, and should now no longer be necessary:

Mathlib/Computability/Ackermann.lean:  termination_by ack m n => (m, n)
Mathlib/Computability/Ackermann.lean:  termination_by ack_strictMono_right m x y h => (m, x)
Mathlib/Computability/Ackermann.lean:  termination_by add_lt_ack m n => (m, n)
Mathlib/Computability/Ackermann.lean:  termination_by ack_strict_mono_left' x y => (x, y)
Mathlib/Computability/PartrecCode.lean:  termination_by evaln k c => (k, c)
Mathlib/Data/List/Infix.lean:termination_by decidableSuffix l₁ l₂ => (l₁, l₂)
Mathlib/Data/List/Infix.lean:termination_by decidableInfix l₁ l₂ => (l₁, l₂)
Mathlib/Data/Nat/Choose/Basic.lean:  termination_by multichoose a b => (a, b)
Mathlib/Data/Nat/Hyperoperation.lean:  termination_by hyperoperation a b c => (a, b, c)
Mathlib/RingTheory/Polynomial/Hermite/Basic.lean:termination_by _ n k => (n, k)
Mathlib/SetTheory/Game/Basic.lean:  termination_by _ => (x, y)
Mathlib/SetTheory/Game/Basic.lean:  termination_by _ => (x, y)
Mathlib/SetTheory/Game/Basic.lean:  termination_by _ => (x, y, z)
Mathlib/SetTheory/Game/Basic.lean:  termination_by _ => (x, y, z)
Mathlib/SetTheory/Game/Birthday.lean:termination_by birthday_congr x y _ => (x, y)
Mathlib/SetTheory/Game/Birthday.lean:termination_by birthday_add a b => (a, b)
Mathlib/SetTheory/Game/Impartial.lean:termination_by _ G H => (G, H)
Mathlib/SetTheory/Game/Impartial.lean:termination_by _ G H _ _ => (G, H)
Mathlib/SetTheory/Game/Ordinal.lean:termination_by toPGame_add a b => (a, b)
Mathlib/SetTheory/Game/PGame.lean:termination_by _ x y => (x, y)
Mathlib/SetTheory/Game/PGame.lean:termination_by _ w x y z _ _ => (x, z)
Mathlib/SetTheory/Game/PGame.lean:termination_by _ x y => (x, y)
Mathlib/SetTheory/Game/PGame.lean:termination_by _ x y => (x, y)
Mathlib/SetTheory/Game/PGame.lean:termination_by _ x y z => (x, y, z)
Mathlib/SetTheory/Game/PGame.lean:termination_by _ x y z => (x, y, z)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:  termination_by nadd o₁ o₂ => (o₁, o₂)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:termination_by nmul a b => (a, b)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:  termination_by nadd_comm a b => (a,b)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:termination_by _ => (a, b, c)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:termination_by nmul_comm a b => (a, b)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:termination_by nmul_nadd a b c => (a, b, c)
Mathlib/SetTheory/Ordinal/NaturalOps.lean:termination_by nmul_assoc a b c => (a, b, c)
Mathlib/SetTheory/Surreal/Basic.lean:termination_by _ x y _ _ => (x, y) -- Porting note: Added `termination_by`

Some of them say

--Porting note: `termination_by` required here where it wasn't before

– was lean3 able to guess lexicographic orders?

[digama0]

Some of them say

--Porting note: `termination_by` required here where it wasn't before

– was lean3 able to guess lexicographic orders?

Actually this is a source of confusion for me: What is the default termination metric if not lexicographic? In lean 3 this was what you get out of the box, and I haven't looked at this in detail but I don't see what else one could even do here. I don't see why "guessing" is necessary and this choice of terminology suggests that I don't understand what you are trying to do.

[nomeata]

– was lean3 able to guess lexicographic orders?

Actually this is a source of confusion for me: What is the default termination metric if not lexicographic? In lean 3 this was what you get out of the box, and I haven't looked at this in detail but I don't see what else one could even do here. I don't see why "guessing" is necessary and this choice of terminology suggests that I don't understand what you are trying to do.

If you have a function with two arguments, m and n, many termination arguments are feasible:

termination_by m n => m
termination_by m n => n
termination_by m n => (m, n)
termination_by m n => (n, m)
termination_by m n => m + n
termination_by m n => m - n
etc.

If you don't specify a termination_by, then lean tries a bunch of these, and picks the first that works. Until a week ago or so, it would only try the first two (pick one argument, see if it goes through). With the GuessLex code, it also tries all tuples of arguments (i.e. lexicographic orders). In neither case, more complex arguments (e.g. m + n) would be inferred. I do not know what lean3 did.

This is not about inferring the well-founded relation, given a termination argument; that is done by type class resolution, and I did not touch that part. And there, yes, there the default is to use lexicographic orders for Prod and Sigma, and SizeOf otherwise. (At least I believe so, didn't look closely).

[digama0]

lean 3 would always do termination_by m n => (m, n). IMO this is the obvious canonical option and should be the first choice, although you will want to skip arguments that don't change in the recursion because it's better to have things as parameters if possible for downstream reasoning.

[nomeata]

Thanks, that explains the porting comments.
The current code will, by construction, use that (or a subsequence therefor) if it works – but if not it will find other permutations, too, and in particular with mutual recursion more likely find a useful measure (e.g. handle cases where calls from f → g decrease the arguments, but g → f don’t.)

you will want to skip arguments that don't change in the recursion because it's better to have things as parameters if possible for downstream reasoning.

This already happens at least for the “fixed prefixes”. So if m is not changing in recursive calls, it’ll be a parameter. If m is changing and n isn’t, it won’t, however.