It is possible to induct on recursive function calls?

Stream: lean4

[Alex Zani]

So I'm working on a parser and I have functions that look like this MWE. acceptNextsteps through the input. advanceWhile skips through characters as long as a predicate is true. (In the real code, acceptNext does some bookkeeping for things like line and column numbers which is why it is a separate function)

def acceptNext : List Char → Option (List Char × Char)
  | (c :: cs) => some (cs, c)
  | [] => none


def advanceWhile (l : List Char) (pred : Char → Bool) : List Char :=
  match isSome : acceptNext l with
  | some (ls, c) =>
    if pred c
    then advanceWhile ls pred
    else l
  | none => l
  termination_by (l.length)
  decreasing_by
    simp_wf
    revert isSome
    induction l with
    | nil => unfold acceptNext; simp
    | cons c' ls' =>
      unfold acceptNext
      simp
      intro hls _
      rw [hls]
      simp

In order to help me prove that some callers terminate, I would like to prove that

theorem advanceWhile_progresses (l : List Char) (pred : Char → Bool) :
  (advanceWhile l pred).length ≤ l.length := by

I'm very confused by how to go about it. If I was doing it on paper, I would probably do something like induction on the size of the call stack. But I'm not sure how I would do that here.

[Edward van de Meent]

if the proof follows the same shape as the function, i imagine advanceWhile.induct might help

[Bhavik Mehta]

Lean generates acceptNext.induct and advanceWhile.induct, one of these might be helpful to you

[Bhavik Mehta]

In particular, acceptNext.induct will do induction on the size of the call stack, since that's the shape of that definition. You could alternatively induct on l itself, which should do something similar, and will induct on the shape of the list

[Alex Zani]

Thanks. acceptNext.induct does not appear to exist. I'm also a bit unsure how I'm supposed to go about using acceptWhile.induct. I assume I should constructure an assumption using it, but the first thing it wants is a function from my parameters to Prop.

[Ruben Van de Velde]

Does the fun_induction tactic work now?

[Alex Zani]

I'm getting "unknown tactic"

[Kyle Miller]

What does #version say for you?

[Alex Zani]

unexpected token '#'; expected command

eval Lean.versionString gives 4.10.0

[Kyle Miller]

I see — the latest stable release is 4.18, and 4.19 is currently under testing. Would you be able to upgrade?

[Alex Zani]

I'll see if I can.