Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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.
like image 286
k_g Avatar asked May 26 '16 23:05

k_g


1 Answers

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.

like image 93
Rodrigo Ribeiro Avatar answered Nov 20 '22 07:11

Rodrigo Ribeiro