How can I convince Coq that my function is in fact recursive?

Question

I'm trying to write a program in Coq to parse a relatively simple context-free grammar (one type of parenthesis) and my general algorithm is for the parser to potentially return the remainder of a string. For example, parsing "++]>><<" should return CBTerminated [Incr Incr] ">><<" and then, say a parser that is parsing "[++]>><<" would be able to pick up the ">><<" and continue with that.

So obviously, the string is smaller, but convincing Coq of that is another matter. It is giving me the error

Recursive definition of parseHelper is ill-formed. [...] Recursive call to parseHelper has principal argument equal to "rest'" instead of "rest".

Which I assume means that it isn't convinced that rest' < input in the way that it's convinced that rest < input. (where < means "is smaller than").

I'd thought of instead returning a count of how many characters to skip, but that seems rather inelegant and uneccessary.

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Require Import ZArith.

Open Scope char_scope.
Open Scope list_scope.

Notation " [ ] " := nil (format "[ ]") : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope.

Inductive BF :=
    | Incr : BF
    | Decr : BF
    | Left : BF
    | Right : BF
    | In : BF
    | Out : BF
    | Sequence : list BF -> BF
    | While : BF -> BF.

Inductive BF_Parse_Result :=
    | UnmatchedOpen
    | EOFTerminated (u : list BF)
    | CBTerminated (u : list BF) (rest : string).

Definition bind (val : BF) (onto : BF_Parse_Result) :=
    match onto with
        | UnmatchedOpen => UnmatchedOpen
        | EOFTerminated values => EOFTerminated (cons val values)
        | CBTerminated values rest => CBTerminated (cons val values) rest
    end.

Fixpoint parseHelper (input : string) : BF_Parse_Result :=
    match input with
        | EmptyString => EOFTerminated nil
        | String first rest =>
             match first with
                 | "+" => bind Incr (parseHelper rest)
                 | "-" => bind Decr (parseHelper rest)
                 | "<" => bind Left (parseHelper rest)
                 | ">" => bind Right (parseHelper rest)
                 | "," => bind In (parseHelper rest)
                 | "." => bind Out (parseHelper rest)
                 | "]" => CBTerminated nil rest
                 | "[" =>
                     match parseHelper rest with
                         | UnmatchedOpen => UnmatchedOpen
                         | EOFTerminated _ => UnmatchedOpen
                         | CBTerminated vals rest' =>
                             bind (While (Sequence vals)) (parseHelper rest')
                     end
                 | _ => parseHelper rest
             end
    end.

Tiro

Umm, that one is usually tricky. As a first attempt, I suggest you define your function by recursion on the numbers of calls. That is to say, add a nat parameter that limits how many times the function is called. But parseHelper (length input) input will be correct. Once you get that form working, you could start to refactor (maybe using an accumulator?) See: x80.org/collacoq/abidadadol.coq – Prindle

@Prindle I tried that but found it very difficult to prove that parseHelper (length input) input was in fact correct. – Tiro

Umm, it shouldn't be more difficult than proving the version you posted correct, would it be accepted by Coq. You may want a lemma thou stating that the result of parsing is the same for sizes greater than lenght input or switch to returning some sizes to have exact values, but you didn't want that. – Prindle

Yeah, in particular, for the given definition, you need to generalize the correctness lemma to forall n, length input <= n, "correct" parseHelper n input to get an usable induction hypothesis. – Prindle

Answer 1

Have you considered using well-founded recursion? Coq's standard library has a series of useful combinators for defining functions over well-founded relations. Reference 1 shows two techniques (well-founded recursion and a monad) for general recursion.

Other technique that is also very useful in context of Agda, is the so-called Bove-Capretta method, which defines an inductive predicate that mimics the call graph of defined function.

Coq also has the Function command that can be used to define more general recursive functions. Whenever I needed to define non-structurally recursive functions, I have used well-founded recursion.

Hope that this helps you.

Frisco

Thanks for letting me know about this interesting strategy. In my case, I ended up just refactoring to a different design that uses an explicit stack of all the open parentheses at a given point, I think I just taill-call-eliminated it, it's a little simpler. – Tiro

For completeness, Program Fixpoint can be used quite the same way as Function to deal with non-structural recursion. – Brooks