Proving termination for mutually recursive functions.

Stream: lean4

[Alex Zani]

So I'm working on a little parser combinator and I'm having a hard time proving termination. When I look at the acceptTermNoApp function, the only assumption it gives me is (state : State). And simp_wf gives me |- False, which is less than ideal. How would I go about proving termination?

(Sorry for the long example, I tried my best to condense.)

structure State where
  src : List Char

inductive Result
  | ok (state : State)
  | fail
  | fatal

def State.acceptNext : State → Result
  | {src := []} => Result.fail
  | {src := (_ :: cs)} => Result.ok {src := cs}

def State.acceptChar : Char → State → Result
  | t, {src := (c :: cs)} => if t == c
                             then Result.ok {src := cs}
                             else Result.fail
  | _, _ => Result.fail

def State.acceptVar (state : State) : Result :=
  match state.acceptNext with
  | Result.ok state' => Result.ok state'
  | other => other

mutual
  def State.acceptTermNoApp (state : State) : Result :=
    match state.acceptAbstraction with
    | Result.fail => state.acceptVar
    | other => other
  termination_by state

  def State.acceptTerm (state : State) : Result :=
    match state.acceptApplication with
    | Result.fail => state.acceptTermNoApp
    | other => other
  termination_by state

  def State.acceptAbstraction (state : State) : Result :=
    match state.acceptChar 'λ' with
    | Result.ok state' => state'.acceptTerm
    | Result.fail => Result.fatal -- Expected to see a body after a lambda
    | Result.fatal => Result.fatal
  termination_by state

  def State.acceptApplication (state : State) : Result :=
    match state.acceptTermNoApp with
    | Result.ok state' => state.acceptTerm
    | other => other
  termination_by state
end

[Robin Arnez]

Simplest way is just to not prove termination, i.e. put partial in front of everything in the mutual block. Note: partial causes the functions to work as expected at runtime but not requiring termination by making them opaque for proofs. As long as you don't need proofs, this should be fine though.

[Aaron Liu]

Problem: it doesn't terminate? acceptTerm and acceptApplication can call each other forever.

[Alex Zani]

Aaron Liu said:

Problem: it doesn't terminate? acceptTerm and acceptApplication can call each other forever.

I don't think that's correct. acceptApplication will only call acceptTerm if acceptTermNoApp has made progress.

[Aaron Liu]

Alex Zani said:

Aaron Liu said:

Problem: it doesn't terminate? acceptTerm and acceptApplication can call each other forever.

I don't think that's correct. acceptApplication will only call acceptTerm if acceptTermNoApp has made progress.

Suppose:
acceptTerm is called

it calls acceptApplication to compute the match

it calls acceptTermNoApp, which computes ok and the result is discarded
it calls acceptTerm

loop