Termination works in Lean 3, but fails in Lean 4

Stream: lean4

[Patrick Johnson]

Lean 3 (works):

def f : nat → nat → nat → nat
| 0 x y := x + y
| (n+1) x 0 := x
| (n+1) x (y+1) := f n (f (n+1) x y) (f (n+1) x y + y + 1)

Lean 4 (fails):

def f : Nat → Nat → Nat → Nat
| 0, x, y => x + y
| (n+1), x, 0 => x
| (n+1), x, (y+1) => f n (f (n+1) x y) (f (n+1) x y + y + 1)

Is this expected? My guess is that Lean 3 termination prover can pull some useful facts from mathlib, while Lean4 can't.

[Reid Barton]

I don't know what the reason is but it's not anything related to mathlib, because it works in Lean 3 without any imports.

[Arthur Paulino]

I was trying to bake a simpler example and I found out that this fails both in Lean 3 and Lean 4:

def g : ℕ → ℕ → ℕ -- fails in Lean 3
| (n+1) x := g n (g (n+1) x)
| _ _ := 0

def g : Nat → Nat → Nat -- fails in Lean 4
| (n+1), x => g n (g (n+1) x)
| _, _ => 0

[Alice Laroche]

Well this one can be expended infinitly so it's normal
You have :
g (n+1) x => g n (g (n+1) x)) => g n (g n (g (n+1) x))) => g n (g n (g n (g (n+1) x)))) => etc

[Patrick Johnson]

The example I posted is the Sudan function.

[Arthur Paulino]

Sorry, I think I got it this time:

def f : nat → nat → nat -- works on Lean 3
| (n + 1) (y + 1) := f n (f (n + 1) 0)
| _       _       := 0

def f : Nat → Nat → Nat -- fails on Lean 4
| (n + 1), (y + 1) => f n (f (n + 1) 0)
| _,       _       => 0

[Alice Laroche]

Maybe Lean 3 is able to infer that f (n + 1) 0 = 0 so it inline it in the first equation and then solve it ?

[Alice Laroche]

This hypothesis doesn't explain why Sudan work in Lean 3 and not in Lean 4 tho, since i don't see such inlining

[Mario Carneiro]

The function works in lean 3 because it's decreasing lexicographically on the arguments. It is compiled to a well founded recursion, and the default well order is the lexicographic one. The default decreasing tactic has just enough smarts to try each of the lex constructors and prove n < n+1 which is what is needed to prove this is decreasing

[Mario Carneiro]

in lean 4, it appears not to guess a termination measure anymore, it only tries structural recursion if the error message is to be believed. However you can give it the lex order pretty easily, and it goes through without issue:

def f : Nat → Nat → Nat → Nat
| 0, x, y => x + y
| (n+1), x, 0 => x
| (n+1), x, (y+1) => f n (f (n+1) x y) (f (n+1) x y + y + 1)
termination_by _ n x y => (n, x, y)

[Mario Carneiro]

For Arthur's test, the obvious thing doesn't work:

def f : Nat → Nat → Nat -- fails on Lean 4
| (n + 1), (y + 1) => f n (f (n + 1) 0)
| _,       _       => 0
termination_by _ n y => (n, y)

tactic 'assumption' failed,
case h
n y : Nat
⊢ 0 < Nat.succ y

Lean 3's default decreasing tactic has a small collection of built in theorems about natural numbers like x < x.succ and x <= x + y which are useful for proving things about the autogenerated sizeof function. It was always a bit ad hoc, and we tried to reduce it down to just assumption in lean#288. It appears that lean 4's default decreasing tactic is also weak, although I don't know whether this is a deliberate attempt to downsize or simply something the devs haven't gotten to yet.

[Arthur Paulino]

Thanks for the thoughtful answer Mario!