Failed to show termination

Stream: lean4

[Brandon Brown]

I'm making my own int type derived from the built-in Nat type. I believe I have made a correct subtraction function and it seems obvious to me that it should terminate, because in the recursive calls the second parameter will eventually become either pos zero or neg zero but the termination checker isn't recognizing this and says it failed to show termination. If I mark it with unsafe I can check that it appears to be computing as expected nonetheless. How do I convince the termination checker?
MWE :

inductive int : Type where
| pos : Nat → int
| neg : Nat → int

open int

protected def int.decrement (a : int) : int :=
  match a with
  | pos 0 => neg 1
  | pos (b+1) => pos b
  | neg b => neg (b+1)

#reduce int.decrement $ pos $ 0

protected def int.increment (a : int) : int :=
  match a with
  | pos 0 => pos 1
  | neg 0 => pos 1
  | pos b => pos b.succ
  | neg (b+1) => neg b

#reduce int.increment $ neg $ 2

protected unsafe def int.sub (a b : int) : int :=
  match a,b with
  | pos c, pos 0 => a
  | neg c, pos 0 => a
  | neg c, neg 0 => a
  | pos c, neg 0 => a
  | pos c, pos (d+1) => int.sub (int.decrement a) (pos d)
  | neg c, pos (d+1) => int.sub (int.decrement a) (pos d)
  | neg c, neg (d+1) => int.sub (int.increment a) (neg d)
  | pos c, neg (d+1) => int.sub (int.increment a) (neg d)

-- (-1) - (-2) = +1
#reduce int.sub (neg 1) (neg 2)
-- (-2) - 3 = -5
#reduce int.sub (neg 2) (pos 3)
-- 5 - 3 = +2
#reduce int.sub (pos 5) (pos 3)
-- 3 - (-2) = +5
#reduce int.sub (pos 3) (neg 2)

[Kevin Buzzard]

My complete guess is that Lean might be looking at the first factor first, and here it is not at all obvious that what you write terminates, because increment and decrement can make terms more complex. Why not try a version of the definition where the first factor gets simpler? In Lean 3 you can write your own code to prove termination and get the equation compiler to use it but I don't know if this functionality is available yet in Lean 4.

[Ryan Lahfa]

You can define int.sub by well foundness with an appropriate measure (it looks like a + b is obviously fine but I might be wrong when you will get to the actual implementation)

[Daniel Fabian]

We have structural recursion on arbitrary arguments for types and soon for predicates. This doesn't cover mutually recursive definitions for now. And we don't have well-founded recursion yet.

[Mario Carneiro]

The usual trick here is to have auxiliary definitions that are structural recursive, and that works in this case too:

protected def int.sub (a : int) : int → int
| pos b => subNat a b
| neg b => addNat a b
where
  subNat (a : int) : Nat → int
  | 0 => a
  | d+1 => subNat (int.decrement a) d
  addNat (a : int) : Nat → int
  | 0 => a
  | d+1 => addNat (int.increment a) d

[Brandon Brown]

Cool, I didn't know you could have nested functions

[Michael Jam]

Considering this MWE

def f : Nat → Nat → Nat
  | .zero, .zero => .zero
  | .zero, .succ .. => .zero
  | .succ .., .zero  => .zero
  | .succ a, .succ b =>
      f b .zero

inductive N
| zero : N
| succ : N → N

def g : N → N → N
  | .zero, .zero => .zero
  | .zero, .succ .. => .zero
  | .succ .., .zero  => .zero
  | .succ a, .succ b =>
      g b .zero

On 08-27 nightly, lean fails to show termination for g but not for f which is really odd given that N is defined just like Nat. This looks like a bug to me. Thanks a lot for fixing this issue / explaining why it doesn't work.

[Andrés Goens]

@Michael Jam it looks a lot like Nat, but it's not Nat. Lean has special machinery there for Nat, see e.g.: https://github.com/leanprover/lean4/blob/78927542b7f8222887b0277d52ed433d6a5f8e30/stage0/src/Init/WF.lean#L151

[Michael Jam]

But here, if my understanding is correct, the proof should be by structural recursion and not by WF recursion so I am not sure this is relevant

[Michael Jam]

It works by the way, if you replace b by a on the last line

[Sebastian Ullrich]

No, Lean fails to dispatch f via structural recursion just like for g. If you dig through f's ultimate definition using #print, you can see the well-founded recursion.

[Michael Jam]

Ah so its just fortunate that it works for f because a Nat wf relation is defined behind the scenes

[Michael Jam]

Will structural recursion be able to handle such cases in the future? I really think of that example structurally or am I wrong to think like that?

[Andrés Goens]

Maybe it's not because of the currying? In a sense you're doing the recursion on N -> N, not on N there. I don't know the details of the type theory behind there though, so maybe I'm totally wrong there as well

[Sebastian Ullrich]

It should be technically feasible, but implementing it could be quite tough. You could try it yourself for this example if you want, you'll need course-of-values recursion via Nat.brecOn to jump straight from .succ b to .zero

[Michael Jam]

I think I was wrong to think it's structural because actually b changed of position as an argument sorry for wasting time.