GuessLex too clever for the default terminaton_tactic.

[nomeata]

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.

[nomeata]

Another possible fix could be

  `(tactic|
    (simp_wf
+   try omega
    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)

Not very disciplined, and will run omega twice since it is also part of trivial_decreasing (maybe remove it there then?), but maybe good enough as an interim solution.

[nomeata]

Hmm, now that I think about it, I am not sure why I abandoned my attempt at letting decreasing_with handle this correctly. I vaguely remember playing with a variant of decreasing_with that is smarter about this, at the expense of requiring backtracking.

Am I right that Lean does not support backtracking across ;, in the sense that (first | a | b) ; c (or a variant thereof) will try a;c first and if that fails (in a or c), will try b;c, right?

Then probably this needs something like

syntax "solve_lex" tacticSeq : tactic

macro_rules
 | `(tactic| solve_lex $ts:tacticSeq) =>
   `(tactic| first | (apply Prod.Lex.right ; ($ts))
                   | solve | apply Prod.Lex.left
                             ($ts)
                           | apply Prod.Lex.right
                             . $ts
                             . solve_lex $ts
                           | $ts)

(if that is reasonable, with all the recursion and duplication and hopefully correct backtracking) to be used as

macro "decreasing_with " ts:tacticSeq : tactic =>
 `(tactic|
   (simp_wf
    solve_lex (
      first
      | done
      | $ts
      | fail "failed to prove termination, possible solutions:
    - Use `have`-expressions to prove the remaining goals
    - Use `termination_by` to specify a different well-founded relation
    - Use `decreasing_by` to specify your own tactic for discharging this kind of goal")
   )))

I’ll try that the coming week if none beats me to it.