Converting a simple function from Lean3 to Lean4

Stream: lean4

[Richard Evans]

Apologies in advance: this is a beginner's question as well as a Lean4 question.

I am trying to convert a simple function from Lean3 to Lean4.

Here is the original Lean3 function (from https://github.com/blanchette/logical_verification_2020/tree/master/lean)

def drop {α : Type} : ℕ → list α → list α
| 0       xs        := xs
| (_ + 1) []        := []
| (m + 1) (x :: xs) := drop m xs

To convert to Lean4, I replaced list with List and also added an explicit match (because Lean4 doesn't seem to like | on multiple arguments unless I am missing something):

def drop {α : Type} : Nat → List α → List α := λ n as => match (n, as) with
| (0,       xs)         => xs
| (_ + 1,   [])         => []
| (Nat.succ m, x :: xs) => drop m xs

But Lean4 doesn't like this because it cannot prove that it terminates:

fail to show termination for drop with errors: argument #2 was not used for structural recursion failed to eliminate recursive application drop m xs

Can someone please explain what is going on? Thanks in advance.

[Henrik Böving]

So first things first you can actually write it like this:

def drop {α : Type} : Nat → List α → List α
| 0,       xs        => xs
| (_ + 1), []        => []
| (m + 1), (x :: xs) => drop m xs

secondly, the termination checker does solve this just fine for me.

[Sébastien Michelland]

You're not matching on the second argument but on a pair built using the second argument, which "hides" the structural recursion. If you match on the two values rather than a pair, it works:

def drop {α : Type} : Nat → List α → List α := λ n as => match n, as with
| 0,       xs         => xs
| _ + 1,   []         => []
| Nat.succ m, x :: xs => drop m xs

You can also drop the match, as Henrik just showed.

[Richard Evans]

That's great. Thank you!