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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: 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.

[nomeata]

@brunodurtertre repored another instance of this issue:

variable {α: Type} [BEq α] [LE α] [DecidableRel ((· : α) ≤ ·)]

-- search whether we can split w into two subwords w₁ and w₂ such that
-- p₁ w₁ and p₂ w₂ are true
def search_split (w: List α) (p₁ p₂: List α → Bool): Bool :=
  loop 0
where loop (i: Nat): Bool :=
  if h : i ≤ w.length then
    p₁ (w.take i) && p₂ (w.drop i) || loop (i + 1)
  else false
termination_by w.length + 1 - i

def in_range (w: List α) (b c: α): Bool :=
  if h: w.length = 1 then b ≤ w[0] && w[0] ≤ c else false

inductive Regex (α: Type)
  | none
  | empty
  | word (w₀: List α)
  | concat (a: Array (Regex α))
  | union (a: Array (Regex α))
  | intersection (a: Array (Regex α))
  | range (b c: α)
  | star (r₀: Regex α)
  | plus (r₀: Regex α)
  | all_char
mutual
-- check wether `w` is in `r`
def in_re (w: List α) (r: Regex α): Bool :=
  match r with
  | .none => false
  | .empty => w.isEmpty
  | .word w₀ => w == w₀
  | .concat a => in_concat w a 0
  | .union a => ∃ i, i < a.size ∧ ∀ (k: i < a.size), in_re w a[i]
  | .intersection a => ∀ i, (k: i < a.size) → in_re w a[i]
  | .range b c => in_range w b c
  | .star r₀ => in_star w r₀
  | .plus r₀ => in_plus w r₀
  | .all_char => w.length == 1
termination_by (sizeOf r, w.length, 0)

-- check whether `w` is in `r*`
def in_star (w: List α) (r: Regex α): Bool :=
  w.isEmpty || in_plus w r
termination_by (sizeOf r, w.length, 2)

-- check whether `w` is in `r+`
def in_plus (w: List α) (r: Regex α): Bool :=
  in_re w r ||
    search_split w
      (fun w₀ => if w₀.length < w.length then in_re w₀ r else false)
      (fun w₀ => if w₀.length < w.length then in_plus w₀ r else false)
termination_by (sizeOf r, w.length, 1)

-- check whether `w` is in `a[i] ++ .. ++ a[n-1]` (where n = a.size)
def in_concat (w: List α) (a: Array (Regex α)) (i: Nat): Bool :=
  if h: i < a.size then
    search_split w
      (fun w₀ => if w₀.length ≤ w.length then in_re w₀ a[i] else false)
      (fun w₀ => if w₀.length ≤ w.length then in_concat w₀ a (i+1) else false)
  else
    w.isEmpty
termination_by (sizeOf a, w.length, a.size - i)
-- This decreasing_by clause is needed in 4.11.0 (without it, we get unprovable goals).
-- This is fixed upstream: https://github.com/leanprover/lean4/issues/5027
decreasing_by
  all_goals (simp_wf; simp [Prod.lex_def])
  omega

end

Worth adding as a test case once we tackle this.