Showing termination in "Functional Programming in Lean"

Stream: lean4

[Peter B]

Hello! I'm just getting started with this newly-updated book and have run into a weird termination issue that I don't quite understand.

The exercise in the book reads:

Write a function zip that combines two lists into a list of pairs. The resulting list should be as long as the shortest input list. Start the definition with def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=.

My first cut at this, adopting the proposed function signature, was:

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

This gives me the following error:

fail to show termination for
  zip2
with errors
argument #3 was not used for structural recursion
  failed to eliminate recursive application
    zip2 tailx taily

argument #4 was not used for structural recursion
  failed to eliminate recursive application
    zip2 tailx taily

I read some of the threads here (the one about merge sort was particularly helpful), and I tried playing around with termination_by, but it's clear that at this point in the book that shouldn't be necessary.

So just in the nature of experimentation, I rewrote the function with a different signature, but doing substantively exactly the same thing:

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

What gives? Why is lean able to tell, without help, that the second form terminates but the first doesn't? In both cases the lists are clearly decreasing in length on each recursive call. What am I missing?

Tagging @David Thrane Christiansen in case other readers have hit the same speed bump.

(If it matters, I'm running Lean (version 4.0.0-nightly-2023-06-01, commit 28538fc74889, Release))

[Peter B]

Update: After poking around a bit, I had the epiphany that my parentheses in the match might be the issue (presumably because I was somehow now matching on a pair, vs matching on multiple expressions. This seems to make the termination checker happy

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

[David Thrane Christiansen]

Thanks for letting me know! This gotcha should definitely be in the book. I'm really busy and not sure when I can do it, but here's at least an issue to track it: https://github.com/leanprover/fp-lean/issues/125

Thanks again!