decreasing_by in monadic context?

Stream: new members

[Marcus Völker]

Hello world, new Lean user here.

I'm trying to prove that a function I wrote is well-founded, but I can't get decreasing_by to give me all the context necessary to prove this.

The function itself looks like this:

def manyFunc {τ α} (p : StrongParser τ α) (t : List τ) : DCont String (List α × List τ) :=
  let val := p.val
  let H := p.property
  do
    let (a0,r) <- pFunc val t
    (λ(a,r') => (a0 :: a, r')) <$> manyFunc p r
  termination_by t.length
  decreasing_by
    sorry

In the goal state, I would have to prove (correctly) that r.length < t.length, but r essentially appears completely unconstrained.

MWE:

inductive DCont (ε α) where
  | Intro (run : (ρ : Type) → (α → ρ) → (ε → ρ) → ρ)

def run {ε α} (c : DCont ε α) := match c with
  | DCont.Intro r => r

instance {ε : Type u} : Functor (DCont ε) where
  map f c := DCont.Intro (λ ρ => λ bf => λ ef => run c ρ (bf ∘ f) ef)

instance {ε : Type u} : Applicative (DCont ε) where
  pure a := DCont.Intro (λ _ => λ af => λ _ => af a)
  seq cf ca := DCont.Intro (λ ρ => λ bf => λ ef => run cf ρ (λ f => run (ca ()) ρ (bf ∘ f) ef) ef)

instance {ε : Type u} : Monad (DCont ε) where
  bind x f := DCont.Intro (λρ => λbf => λef => run x ρ (λc => run (f c) ρ bf ef) ef)

def pFunc_is_dec {τ α} (pFunc : List τ → DCont String (α × List τ)) := ∀t, run (pFunc t) Bool (λ(_,r) => r.length <= t.length) (λ_ => true)
def pFunc_is_sdec {τ α} (pFunc : List τ → DCont String (α × List τ)) := ∀t, run (pFunc t) Bool (λ(_,r) => r.length < t.length) (λ_ => true)

inductive Parser (τ α) where
  | Intro (pFunc : List τ → DCont String (α × List τ)) (Hdec : pFunc_is_dec pFunc)

def pFunc {τ α} (p : Parser τ α) := match p with
  | Parser.Intro f _ => f

def StrongParser (τ α) := { p : Parser τ α // pFunc_is_sdec (pFunc p) }

def manyFunc {τ α} (p : StrongParser τ α) (t : List τ) : DCont String (List α × List τ) :=
  let val := p.val
  let H := p.property
  do
    let (a0,r) <- pFunc val t
    (λ(a,r') => (a0 :: a, r')) <$> manyFunc p r
  termination_by t.length
  decreasing_by
    sorry

I presume that the inclusion of the monad and the indirection of the continuation doesn't help here, but is there a way to get lean to give me more about r for this proof?

[Eric Wieser]

It doesn't answer your question, but

inductive DCont (ε α) where
  | Intro (run : (ρ : Type) → (α → ρ) → (ε → ρ) → ρ)

def run {ε α} (c : DCont ε α) := match c with
  | DCont.Intro r => r

can be more concisely written as

structure DCont (ε α) where
  intro ::
    run : (ρ : Type) → (α → ρ) → (ε → ρ) → ρ

[Eric Wieser]

(and similarly for Parser)

[Eric Wieser]

My suspicion is that you can't prove termination (because it doesn't terminate), since pFunc_is_dec doesn't protect against the case where pFunc inspects its continuation, and only produces a smaller list when (λ(_,r) => r.length <= t.length) is passed in, otherwise producing a larger one

[Eric Wieser]

I would speculate that

def pFunc_is_dec {τ α} (pFunc : List τ → DCont String (α × List τ)) :=
  ∀ t, SatisfiesM (·.2.length ≤ t.length) (pFunc t)

is the right condition

[Mirek Olšák]

I think you want to build an alternative function to pFunc which operates on a StrongParser, and returns also a proof of the result being smaller. So it would look something like

def spFunc {τ α} (p : StrongParser τ α) (l : List τ) : DCont String {x : (α × List τ) // x.2.length < l.length} := do
  let ⟨a0,r⟩ ← pFunc p.val l
  return ⟨⟨a0,r⟩, sorry⟩

def manyFunc {τ α} (p : StrongParser τ α) (t : List τ) : DCont String (List α × List τ) :=
  do
    let ⟨⟨a0,r⟩,h⟩ <- spFunc p t
    (λ(a,r') => (a0 :: a, r')) <$> manyFunc p r
  termination_by t.length
  decreasing_by exact h

Only that if you do it like this, spFunc indeed doesn't have enough context to prove the sorry. I would try to avoid the monad syntax, and figure out on a term-level if all the necessary information can be passed (and if it is even true).

[Mirek Olšák]

And just to be sure, you know that if the only purpose for the code is running (and not proving), you could use partial def and skip proving termination, right?

[Marcus Völker]

@Eric Wieser Thank you for the suggestions, I will rethink what parser termination actually means.
@Mirek Olšák That might be a good idea! Yes, I know I don't need to prove termination, but this is as much for me learning Lean as it is for producing a viable parser infrastructure, so I actually want to prove termination if I can (plus, I like the added guarantees that I get about the code if I manage the proof)