## Stream: new members

### Topic: Product types, functions and structural recursion

#### Ioannis Konstantoulas (Jan 15 2023 at 08:11):

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 (Jan 15 2023 at 08:30):

There's a couple of solutions to your problem.

1. Make idBool an abbrev:
abbrev idBool (inp : List Bool) : List Bool := inp

1. 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)

1. 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 (Jan 15 2023 at 08:56):

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 (Jan 15 2023 at 10:28):

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 (Jan 15 2023 at 14:19):

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

Last updated: Dec 20 2023 at 11:08 UTC