Proving termination of monadic functions

Stream: lean4

[Henrik Böving]

Given a monadic function where the thing that is reducing size such as a Parsec one, how can I tell the termination_by that I am actually interested in proving that the size of the monadic state is decreasing, e.g.:

import Lean
open Lean Parsec

inductive Exp where
| num (x : Int)
| add (lhs : Exp) (rhs : Exp)

def parseNum : Parsec Exp := do
  let digits := String.mk (←many1 digit).toList
  return .num (String.toInt! digits)

def isAtEof? : Parsec Bool := fun it => .success it it.atEnd

def parseAdd (lhs : Exp) : Parsec Exp := do
  if (←isAtEof?) then
    return lhs
  else
    ws -- whitespace
    skipChar '+'
    ws
    let rhs ← parseNum
    let newLhs := .add lhs rhs
    parseAdd newLhs
termination_by <what do I do here>


def parser : Parsec Exp := do
  let initialLhs ← parseNum
  parseAdd initialLhs

I cannot termination_by parsedAdd lhs it => because I can only used the named arguments here it seems so how can I access it?

[James Gallicchio]

I'm not sure I understand completely, what should it be ?

Can you add a fuel parameter to parseAdd based on the size of the state?

[Henrik Böving]

it is the String.Iterator that Parsec is keeping as its internal state, as you can see in the isAtEof? implementation it is the implicit parameter passed in by the Parsec monad so I would like to be able to refer to it from within termination_by as well.

I dont exactly see how the fuel parameter stuff would work, could you show an example? The code above is fully self contained.

[Jannis Limperg]

You could always unfold Parsec in the type signature and explicitly introduce it. Then you could try to abstract the termination argument into a combinator since you'll be using it a lot.

[James Gallicchio]

Something like this:

def parseAdd' (lhs : Exp) (fuel : Nat) : Parsec Exp := do
  if (←isAtEof?) then
    return lhs
  else
    ws -- whitespace
    skipChar '+'
    ws
    let rhs ← parseNum
    let newLhs := .add lhs rhs
    let newFuel := sorry
    have : newFuel < fuel := sorry
    parseAdd' newLhs newFuel
termination_by _ fuel => fuel

def parseAdd (lhs : Exp) : Parsec Exp :=
  λ it => parseAdd' lhs (sorry /- enough fuel -/) it

[James Gallicchio]

(You'll probably need to require something about fuel to prove you can have a newFuel always, but hopefully your size measure is simple?)