Prove decreasing list size

Stream: lean4

[Alex Sweeney]

I have a function called List.chunk that turns a list into a list of chunks of a given size. I know it terminates but I have no idea how to prove it.

-- Helper: Move n elements from source to acc. This terminates.
def extract : Nat → List α → List α → (List α × List α)
  | _, [], acc => ([], acc.reverse)
  | 0, source, acc => (source, acc.reverse)
  | n + 1, a :: rest, acc =>
    let m := extract n rest (a :: acc)
    (m.fst, m.snd)

#eval extract 2 [1, 2, 3, 4, 5] []
-- ([3, 4, 5], [1, 2])

def List.chunk : List α → Nat → List (List α)
  | [], _ => []
  | _, 0 => []
  | list, n =>
    let (rest, chunk) := extract n list []
    chunk :: List.chunk rest n         -- failed to prove termination.
termination_by _ l _ => l.length

It wants me to prove ⊢ length rest < length list which sounds right but I don't know how to do that. Clearly n is positive, so (rest, chunk) := extract n list [] should take n items thus length rest < length list. I also don't fully understand what termination_by is doing, but it seemed to be a step in the right direction. Any help is appreciated.

[Henrik Böving]

You want to write a lemma that shows that if you call extract n xs acc where n > 0 (which is the case in your thing, you can prove it in that particular match arm but also just use the match arm| list, n + 1 to get this more easily) then the rest part of the output is smaller than xs, probably by induction, potentially generalizing on the acc argument. Once you have that lemma you can go on to prove the thing that termination_by wants you to do in a have. You can find general information about the workings of termination_by here: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html#well-founded-recursion-and-induction