GuessLex too clever for the default terminaton_tactic.

Consider this terminating function

def foo (n m : Nat) : Nat :=
  if h : m = 0 then
    if _ : n = 0 then 0 else foo (n - 1) n
  else
    foo (n - 1) (m - 1)
termination_by?

Here is what happens: GuessLex looks at how n and m decrease in each call, and finds out that (n, m) is a suitable termination measure: In the second call, n decreases non-strictly (≤) and m decreases strictly (<). Because GuessLex looks at how each of these behave separately, this looks promising, and it sets

termination_by (sizeOf n, sizeOf m)

But then the default decreasing_tactic is not able to make use sense of this, because

    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)

can only handle (<, ?) and (=, <), (with = being defeq), but not (≤, <). When I wrote GuessLex I was hoping to improve the decreasing_tactic behavior along it, but revamping that did not happen yet.

Incidentially, omega has some (incomplete) support for Prod.Lex, that’s why

decreasing_by all_goals simp_wf; omega

Probably GuessLex should not even look for ≤, at least not until the default termination tactic can handle that, as unfortunate as that is.

Versions

4.7.0

Additional Information

Observed on Zulip at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/brecOn.20application.20type.20mismatch.20during.20termination.20check.3F/near/433118224

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the GuessLex and default decreasing_tactic behavior described in the issue, then reproduce the example using termination_by? and inspect how Prod.Lex handles the generated comparisons. Compare this with decreasing_by all_goals simp_wf; omega. Done means the example no longer produces an unusable termination measure or the default tactic can discharge the resulting obligations.