# Zulip Chat Archive

## 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.

- Make
`idBool`

an`abbrev`

:

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

- 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)
```

- 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