How does Lean know that this terminates?

Stream: new members

[Kenny Lau]

def foo (m n : Nat) : Int :=
  if m < n then foo (m + 1) n else 100

#eval foo 2 5

[Kenny Lau]

this works and I don't know how

[Robin Arnez]

The termination measure is n - m here. This is the same kind of termination as in:

def foo (i : Nat) (as : Array Nat) : Int :=
  if h : i < as.size then
    foo (i + 1) as + as[i]
  else
    100

[Kenny Lau]

but how does 1. Lean know to use n-m and 2. Lean see it even though it's not a dependent if?

[Kenny Lau]

since it isn't a dependent if it shouldn't even make sense

[Aaron Liu]

in the preprocessing step nondependent ifs are converted into dependent ifs

[Robin Arnez]

It turns it into a dependent if in the recursion compiler. Also, the module that is responsible for this is Lean.Elab.PreDefinition.WF.GuessLex

[Robin Arnez]

Starting with basic measures (sizeOf xᵢ for all parameters xᵢ), and complex measures (e.g. e₂ - e₁ if e₁ < e₂ is found in the context of a recursive call) it tries all combinations until it finds one where all proof obligations go through with the given tactic (decerasing_by), if given, or the default decreasing_tactic.

[Kenny Lau]

ok on my end i did #print foo and found out the shenanigans involved

[Kenny Lau]

def foo (m n : Nat) : Int :=
  if m < n then foo (m + 1) n else 100

#eval foo 2 5
#print foo
/-
@[irreducible] def foo : Nat → Nat → Int :=
fun m n => foo._unary n m
-/
#print foo._unary
/-
def foo._unary : Nat → Nat → Int :=
fun n => ⋯.fix fun m a => if h : m < n then a (m + 1) ⋯ else 100
-/

[Kenny Lau]

it's always interesting when the #print output isn't at all similar to what I wrote in the code