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