Puzzled by termination checking

Stream: new members

[Matt Pillsbury]

Hi all. I'm just starting out with Lean and dependently typed languages.

To get started, I'm making my way through the book and exercises when I tripped over the following in my implementation of zip:

def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
  match (xs, ys) with
  | ([], _) => []
  | (_, []) => []
  | (x :: xs', y :: ys') => (x, y) :: zip xs' ys'

I get a message saying Lean failed to prove termination because arguments #3 and #4 are "not used for structural recursion". When I rewrite the function into a form that looks totally equivalent to me, the complaint goes away:

def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
  match xs with
  | [] => []
  | x :: xs' =>
    match ys with
    | [] => []
    | y :: ys' => (x, y) :: zip xs' ys'

Is there some difference between the two versions that means they aren't equivalent from the standpoint of involving structural recursion?

Thanks!

[Adam Topaz]

def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
  match xs, ys with
  | [], _ => []
  | _, [] => []
  | x :: xs', y :: ys' => (x, y) :: zip xs' ys'

[Adam Topaz]

There is no need to match on tuples.

[Kevin Buzzard]

I suspect that this has to do with the fact that if you want to define a function on lists recursively then there's a auto-generated theorem of the form "if you've defined it for nil and for cons then you're done, and in the cons case you can assume it's already defined for the tail" but the analogous theorem for pairs is "if you want to define it for pairs then you have to define it for all pairs and you can't assume anything" because the definition of a pair is not recursive in the same way. So induction on pairs isn't going to work out of the box.

[Matt Pillsbury]

Thank you both!

Also the syntax Adam introduced solved my problem, so I flipped to the next page in the book, which shows exactly that syntax.