default termination tactic: array_dec_dec tactic too eager, and too weak

[BrunoDutertre]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [ x] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [ x] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [x ] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

On this example, lean produces a confusing error.

inductive Term (α: Type): Type where
  | Composite : Array (Term α) → Term α
  | Atom: α → Term α

-- height of a term
def height (f: Term α): Nat :=
  let rec max_height (a: Array (Term α)) (i: Nat) (m: Nat): Nat :=
    if h: i < a.size then
      max_height a (i + 1) (max (height a[i]) m). -- error for `height a[I]`
    else
      m
  match f with
  | .Composite a => 1 + max_height a 0 0
  | .Atom _ => 1

The error is this:

Height.lean:10:33
unsolved goals
case h
α : Type
a : Array (Term α)
i m : Nat
h : i < a.size
⊢ False

Adding explicit termination_by clauses, as in the following, does not help:

mutual
def max_height' (a: Array (Term α)) (i: Nat) (m: Nat): Nat :=
  if h: i < a.size then
    max_height' a (i + 1) (max (height' a[i]) m)
  else
    m
termination_by (sizeOf a, a.size - i)

def height' (f: Term α): Nat :=
  match f with
  | .Composite a => 1 + max_height' a 0 0
  | .Atom _ => 1
termination_by (sizeOf f, 0)
end

Steps to Reproduce

1. Cut and paste one of the above examples. Then run lean.

Expected behavior:

In order of preference:

1. Have the default termination heuristics synthesize a termination ordering that works on the example
2. If that fails, produce an error message that explains that the problem is related to termination

Actual behavior:

Obscure error: lean just produce a message about an 'unsolved goal` but this goal is unsolvable.
It's not clear at all from the message that this is related to termination.

Versions

Lean 4.10.0

Additional Information

NA

Impact

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

[nomeata]

Thanks for the report. The issue is somewhere with array_get_dec, which forms part of decreasing_trivial. Inlining it all we get

inductive Term (α: Type): Type where
  | Composite : Array (Term α) → Term α
  | Atom: α → Term α

-- height of a term
mutual
def max_height' (a: Array (Term α)) (i: Nat) (m: Nat): Nat :=
  if h: i < a.size then
    max_height' a (i + 1) (max (height' a[i]) m)
  else
    m
termination_by (sizeOf a, a.size - i)
decreasing_by
  . decreasing_with    
      (with_reducible apply Nat.lt_trans (Array.sizeOf_getElem ..))
      -- sizeOf a < sizeOf a
      simp_arith
      
  . decreasing_tactic


def height' (f: Term α): Nat :=
  match f with
  | .Composite a => 1 + max_height' a 0 0
  | .Atom _ => 1
termination_by (sizeOf f, 0)
decreasing_by 
  . decreasing_tactic

end

And of course sizeOf a < sizeOf a is bogus.

I assume that the lemma should be phrased with Nat.lt_of_lt_of_le instead of Nat.lt_trans. Same for the corresponding list lemma.

It is a bit unfortunate that we even need these lemmas here; I wish there was a way to tell omega all it needs to know about the theory of sizeOf that a simple omega would suffice. Until then, we’ll fix these issues as they come up.