Termination checker regression in v4.18.0-rc1

Stream: lean4

[Frédéric Dupuis]

While updating my repositories to v4.18.0-rc1, I encountered the following regression in the termination checker:

def computeFuel (mass : Nat) : Nat :=
  let rec go acc cur :=
    let n := cur / 3 - 2
    if n = 0 then acc + cur else go (acc + cur) n
  go 0 mass - mass

This worked fine in v4.17.0-rc1, but now it fails to prove termination for go:

failed to infer structural recursion:
Cannot use parameter acc:
  failed to eliminate recursive application
    computeFuel.go (acc + cur) n
Cannot use parameter cur:
  failed to eliminate recursive application
    computeFuel.go (acc + cur) n

However, if I write go as a separate function instead of a let rec, it works again:

def computeFuel' (acc cur : Nat) :=
  let n := cur / 3 - 2
  if n = 0 then acc + cur else computeFuel' (acc + cur) n

def computeFuel (mass : Nat) : Nat := computeFuel' 0 mass - mass

works fine.

This is not a major issue for me but I thought I would report it here.

[Henrik Böving]

CC @Joachim Breitner

[Joachim Breitner]

Thanks! That looks like a bug. A work-around is to write if _ : n = 0
Now tracked at issue https://github.com/leanprover/lean4/issues/7408

[Joachim Breitner]

Another work-around

def computeFuel (mass : Nat) : Nat :=
  let rec go acc cur :=
    letI n := cur / 3 - 2
    if n = 0 then acc + cur else go (acc + cur) n
  termination_by cur
  go 0 mass - mass

somehow the let gets in the way