Termination for Wrapped Fin in Lean4

Question

The following example type checks in Lean 4, but I am confused why the termination_by declaration is required.

import Mathlib.Tactic.Linarith

def Idx (n:Nat) := Fin n

def sum(k:Idx n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Idx n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum km1)
  termination_by sum k => k.val

Specifically, a very similar example does not require it:

def sum2(k:Fin n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Fin n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum2 km1)

Obviously, it has something to do with the fact that I've wrapped the Fin n with Idx n. I tried adding a @[simp] annotation, but that didn't help.

(also am interested in whether the example can be improved)

Answer 1

Best solution

If you write it as a structural recursion, then the code is much simpler (and idiomatic) and Lean doesn't need to be given hints:

def sum3 : (k:Idx n) -> Nat
| { val := 0,   isLt := _ } => 0
| { val := m+1, isLt := isLt } =>
  let km1 : Idx n := { val := m, isLt := (by linarith [isLt]) }
  1 + (sum3 km1)

(Of course, as Andrej says in the comments the simplest formula is just def sum (k: Idx n) := k.val. :) )

What can't Lean figure it out in your example?

I don't know the specifics of how Lean's equation compiler works, but unless your recursion is purely syntactic structural recursion, it is challenging to prove that a recursion is well-founded automatically. You need to show some value is decreasing automatically, but it often isn't clear to Lean what value that should be. For structures (Fin) and inductives (Nat), you can use the fields (val) or constructors (zero, succ), but for arbitrary types (Idx), it is not clear what value to use and Lean often gives up.

Yes, in this case, Lean could just unfold Idx, but from Lean's point of view, Idx is just another type. When you write things like k.val and

let km1 : Idx n := {val:=k.val-1,isLt:=(by linarith [k.isLt])}

Lean is doing a lot of coercion here, doing something like (↑k : Fin 1).val and

let km1 : Idx n := (↑{val:=(↑k : Fin n).val-1,isLt:=(by linarith [(↑k : Fin n).isLt])} : Idx n)

Without some hints, it is hard for Lean to know that km1 is "smaller" than the input k. Until it starts to unfold Idx, Lean doesn't know if Idx is a simple type alias or a complicated definition made of multiple parts. I assume such unfolding comes with a cost since often unfolding makes expressions a lot larger. (And Lean is already fairly slow, so it doesn't necessarily make sense to make it slower in this case by adding more things for the equation compiler to search for.)

As Andrej Bauer's comment says if you use [@reducible] that hints to Lean to unfold Idx more often than not, so Lean can then figure out in this case what the decreasing value is.

(Nonetheless, if you feel this is somehow an obvious missing case in Lean's equation compiler, you could report it as an issue on Github, but I don't see an obvious solution on first look.)