如何让 Coq 相信我的函数实际上是递归的？

Question

我正在尝试在 Coq 中编写一个程序来解析一个相对简单的上下文无关语法（一种括号），我的一般算法是让解析器可能返回字符串的其余部分。例如，解析"++]>><<" 应该返回CBTerminated [Incr Incr] ">><<"，然后说解析“[++]>>>

很明显，字符串更小了，但说服 Coq 是另一回事。它给了我错误

parseHelper 的递归定义格式不正确。 [...] 对 parseHelper 的递归调用的主要参数等于“rest” “休息”。

我假设这意味着它不相信rest' < input，就像它相信rest < input一样。 （其中< 表示“小于”）。

我曾想过返回一个要跳过多少字符的计数，但这似乎相当不雅和不必要。

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.

Answer 1

您是否考虑过使用well-founded recursion？ Coq 的标准库有一系列有用的组合器，用于在有根据的关系上定义函数。参考文献1 展示了两种通用递归技术（有根据的递归和单子）。

在 Agda 的上下文中也非常有用的其他技术是所谓的Bove-Capretta method，它定义了一个模仿已定义函数的调用图的归纳谓词。

Coq 还有Function 命令，可用于定义更通用的递归函数。每当我需要定义非结构递归函数时，我都会使用有根据的递归。

希望对您有所帮助。