proof of termination for zip in Lean

Question

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?

Answer 1

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)
    | _ => []

Answer 2

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.