showing termination

Stream: lean4

[James Sully]

Hi, I'm reading "functional programming in lean", I'm up to the exercise that has you implement zip.

I have:

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

I'm getting

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

argument #4 was not used for structural recursion
  failed to eliminate recursive application
    zip moreXs moreYs

structural recursion cannot be used

How do I show lean that this terminates?

[James Sully]

I managed it with a nested match, is there a nicer way? and why isn't lean smart enough to figure out the first one?

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

[Reid Barton]

I would guess the overlapping cases give Lean some trouble. Try making the second case (_ :: _), []?

[James Sully]

didn't work unfortunately. Not even this works:

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

[James Sully]

maybe it's something to do with it being inside a newly cooked up pair?

[James Sully]

is it possible to match on multiple arguments at once without a pair?

[Henrik Böving]

Don't match on a tuple, match on both arguments directly

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

this was recently discussed on the issue tracker as well. maybe it should be clarified in the book?

[James Sully]

nice, thanks. That's handy

[Henrik Böving]

https://github.com/leanprover/lean4/issues/2242

[Arthur Adjedj]

Henrik Böving said:

Don't match on a tuple, match on both arguments directly

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

this was recently discussed on the issue tracker as well. maybe it should be clarified in the book?

Perhaps it would be best to "desugar" matching on tuples to the usual matching on multiple terms ? I've seen quite a lot of people get termination issues because they'd parenthesize on the match where they'd only mean to match on two terms.

[Damiano Testa]

This is also only tangential, but Lean allows you to start with the more "meaty" match first and then handles the rest on its own:

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

[Trebor Huang]

Can't we add a linter or warning that detects whether a newly constructed tuple is directly matched away?

[David Thrane Christiansen]

Thanks for the feedback on the book - I've added it to the issue tracker for next time I get to fixing problems. I'm sorry to have led you astray and caused frustration.