# proof of termination for zip in Lean

I'm making my way through Functional Programming in Lean and there's an exercise to implement zip, which takes two lists and returns a list of tuples the length of the shorter of the two input lists. This is my attempt:

def zip {α β : Type} (as: List α) (bs: List β) : List (α × β) :=
match (as, bs) with
| (a::arest, b::brest) => (a, b) :: zip arest brest
| _ => []


This seems clearly correct to me, but Lean gives me this cryptic error:

fail to show termination for
zip
with errors
argument #3 was not used for structural recursion
failed to eliminate recursive application
zip arest brest

argument #4 was not used for structural recursion
failed to eliminate recursive application
zip arest brest

structural recursion cannot be used

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


I'm recursing on both of the inductive arguments at once, so to me this clearly terminates.

What do arguments #3 and #4 refer in the error messages refer to, and how do I convince Lean that this definitely terminates?

It seems you are trying to use Simultaneous Matching on the two lists as and bs but messed up the syntax, and instead are pattern-matching on the pair (as,bs). The difference is subtle, but since the latter is not of the type List of the function's argument, this gets Lean's termination checker confused. What you meant to write is probably the following:

def zip {α β : Type} (as: List α) (bs: List β) : List (α × β) :=
match as, bs with
| a::arest, b::brest => (a, b) :: zip arest brest
| _, _ => []


If you really want to use pairs, then the following is also accepted, but is probably less idiomatic (and has a more complicated termination proof, although in this case Lean still finds it)

def zip {α β : Type} (l: List α × List β) : List (α × β) :=
match l with
| (a::arest, b::brest) => (a, b) :: zip (arest,brest)
| _ => []

• I’m not sure what you mean by “latter is not an inductive type”. Are you are saying that because product is a structure instead of an inductive type, that is the reason the termination checker fails. If so, I don’t think that is the reason. match works fine on structures as well as inductive types. I think it has more to do with the fact that you are matching on an inductive/structure type other than the inputs to the function. Aug 30, 2023 at 14:47
• You are right, indeed, thanks. I edited the answer Aug 30, 2023 at 14:58
• Thank you! Adding parens makes it a pair instead of... I don't don't what it's called. A simultaneous match pattern? Aug 30, 2023 at 22:33

The answer by Meven Lennon-Bertrand is exactly right, but the best way to ensure you are doing structural recursion is to avoid writing the match statement in the first place:

def zip {α β : Type} : (as: List α) -> (bs: List β) -> List (α × β)
| a::arest, b::brest => (a, b) :: zip arest brest
| _, _ => []


While it is no more than semantic sugar for Meven’s answer, it is, I would say, more idiomatic for Lean. (Also I labeled the parameters as and bs, but that isn’t needed.)

Also maybe it is worth making an issue about your example on the Lean GitHub. It seems that Lean could make this compile or at least provide a better error message, since I think that will be a common user mistake since it is the way recursive functions matching on two variables are done in some other functional languages.

• Maybe this also warrants a word of warning in Functional Programming in Lean when simultaneous matching is introduced (if that book is meant to be evolved over time)? Aug 31, 2023 at 9:28