Product types, functions and structural recursion

Stream: new members

[Ioannis Konstantoulas]

Hello all; I was writing some test code in Lean, and encountered the following situation:

Let idBool : List Bool -> List Bool be the identity function on the type. Define the following two functions in Lean 4, together with the identity:

def idBool (inp : List Bool) : List Bool := inp

def TermBool : Nat \x List Bool -> Nat \x List Bool
| (0, L) => (0, L)
| (Nat.succ k, L) => TermBool (k, L)

partial def TermBool? : Nat \x List Bool -> Nat \x List Bool
| (0, L) => (0, L)
| (Nat.succ k, L) => TermBool? (k, idBool L)

Lean happily accepts the first function, but has trouble proving that the second one terminates: removing the partial marker gives the error

fail to show termination for
  TermBool?
with errors
structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

My question is: what is the reason for the rejection in the second situation, and how can one provide evidence of termination? More generally, if we have an arbitrary (properly defined) function F : List Bool -> List Bool, where is Lean stuck proving termination of

partial def TermF? : Nat \x List Bool -> Nat \x List Bool
| (0, L) => (0, L)
| (Nat.succ k, L) => TermBool? (k, F L)

and how can we overcome this?

Thanks a lot for your time!

[Marcus Rossel]

There's a couple of solutions to your problem.

1. Make idBool an abbrev:

abbrev idBool (inp : List Bool) : List Bool := inp

2. Provide TermBool? in curried form:

def TermBool? : Nat → List Bool -> Nat × List Bool
  | 0, L => (0, L)
  | Nat.succ k, L => TermBool? k (idBool L)

3. Explicitly tell Lean which part is decreasing when recursing:

def TermBool? : Nat × List Bool -> Nat × List Bool
  | (0, L) => (0, L)
  | (Nat.succ k, L) => TermBool? (k, idBool L)
termination_by TermBool? x => x.fst

Options 2 and 3 also work for your general TermF?.

[Marcus Rossel]

As to what's causing the problem in the first place, I think it's the following (please correct me if this is wrong).
If we consider the recursive case in TermF?:

| (Nat.succ k, L) => TermF? (k, F L)

... for the recursion to be allowed, Lean tries to show that (k, F L) is smaller than (Nat.succ k, L) wrt. to some well-founded relation.
The way Lean handles this by default is by assigning a Nat to both terms: sizeOf (k, F L) = n and sizeOf (Nat.succ k, L) = m. Then Lean tries to prove n < m, which thus ensures that the recursion is decreasing.
The sizeOf function comes from the SizeOf type class:

class SizeOf (α : Sort u) where
  sizeOf : α → Nat

Lean creates instances of this for any type you define automatically.
If we now check what the sizes are for some concrete values of type Nat × List Bool, we can see why Lean can't prove that the recursive call in TermF? is decreasing:

#reduce sizeOf (10, [true]) -- 14
#reduce sizeOf (9, [true, false]) -- 15

Here, even though the first member of the tuple decreased, the increased size of the second member caused the total size of the tuple to increase. Thus, Lean couldn't prove termination.

[Ioannis Konstantoulas]

Thank you so much for the detailed explanation of what is going on behind the scenes! I see now that your solution 3 is the most satisfactory for me if I want to insist that the function's signature is some Prod -> Prod.

[Reid Barton]

Or you can use 2, and then provide an uncurried wrapper. That would reduce better.