无法猜测 Coq 中嵌套匹配的递减参数

Question

我对术语有以下定义：

Inductive term : Type :=
  | Var : variable -> term
  | Func : function_symbol -> list term -> term.

和一个函数 pos_list 获取术语列表并为每个子术语返回 "positions" 列表。例如，对于 [Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]]，我应该得到 [[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]]，其中每个元素代表子项树层次结构中的一个位置。

Definition pos_list (args:list term) : list position :=
  let fix pos_list_aux ts is head :=
    let enumeration := enumerate ts in
      let fix post_enumeration ts is head :=
        match is with
        | [] => []
        | y::ys =>
          let new_head := (head++y) in
          match ts with
          | [] => []
          | (Var _)::xs => [new_head] ++ (post_enumeration xs ys head)
          | (Func _ args')::xs =>
            [new_head] ++
            (pos_list_aux args' [] new_head) ++
            (post_enumeration xs ys head)
          end
        end
      in post_enumeration ts enumeration head
  in pos_list_aux args [] [].

使用上面的代码我得到了错误

Error: Cannot guess decreasing argument of fix

在第一个 let fix 构造上，但在我看来，对 (pos_list_aux args' [] new_head) 的调用（这会导致问题）将参数 args' 作为参数 args' ，这是 [=19 的子项=] 本身就是 ts.

的子项

怎么了？

Answer 1

如果您明确告诉 Coq 您正在递归哪个参数，您会收到一条信息量稍大的错误消息。

let fix pos_list_aux ts is head {struct ts} :=

现在 Coq 说

Recursive call to pos_list_aux has principal argument equal to "args'" instead of
"xs".

如果你改用 {struct is}，Coq 说

Recursive call to pos_list_aux has principal argument equal to "[]" instead of
a subterm of "is".

确定递归是否正确的简单句法规则要求您使用来自用 match is with ... end.

破坏参数的术语进行递归

使用从 head 元素中获取的东西并不简单，如 args'，甚至在 is 上的递归情况下使用 []。例如，也许您创建了一个无限循环，在该循环中您使用 [] 作为递归参数调用自己。类型检查器需要防止这种情况。

句法规则是 "very simple" 并且在这种情况下并不适用，即使递归是 "obviously" 在这种情况下结构较小的组件上也是如此。因此，您必须以更复杂的方式说服类型检查器 args' 没问题。

也许其他人可以提供一种优雅的方式来做到这一点？我的第一个尝试是查看 Program 是否处理了这个问题（但没有处理）。

Answer 2

term 是一个嵌套的归纳类型（因为 Func 构造函数中的 list term）并且它经常需要一些额外的工作来向 Coq 解释你的函数是完整的。 CPDT 的 chapter 解释了如何处理这种情况（参见 "Nested inductive types" 部分）：

The term “nested inductive type” hints at the solution to this particular problem. Just as mutually inductive types require mutually recursive induction principles, nested types require nested recursion.

这是我为解决您的问题所做的尝试。首先，让我们添加一些导入和定义，以便编译所有内容：

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

Definition variable := string.
Definition function_symbol := string.
Definition position := list nat.

Inductive term : Type :=
  | Var : variable -> term
  | Func : function_symbol -> list term -> term.

我们首先实现一个函数来完成单个 term 的工作。请注意，我们定义了一个嵌套函数 pos_list_many_aux，这几乎是您最初想要的：

Definition pos_list_one (i : nat) (t : term) : list position :=
  let fix pos_list_one_aux (i : nat) (t : term) {struct t} : list position :=
      match t with
      | Var _ => [[i]]
      | Func _ args =>
          [i] :: map (cons i)
                     ((fix pos_list_many_aux i ts :=
                         match ts with
                         | [] => []
                         | t::ts =>
                             pos_list_one_aux i t ++ pos_list_many_aux (S i) ts
                         end) 1 args).     (* hardcoded starting index *)
      end
  in pos_list_one_aux i t.

现在，我们需要一个辅助函数mapi（从 OCaml 的标准库中借用的名称）。就像map，但是映射函数也接收当前列表元素的索引。

Definition mapi {A B : Type} (f : nat -> A -> B) (xs : list A) : list B :=
  let fix mapi i f xs :=
    match xs with
    | [] => []
    | x::xs => (f i x) :: mapi (S i) f xs
    end
  in mapi 0 f xs.

现在一切就绪，可以定义 pos_list 函数：

Definition pos_list (args : list term) : list position :=
  concat (mapi (fun i t => pos_list_one (S i) t) args).

让我们运行测试一下：

Section Test.
  Open Scope string_scope.

  Compute pos_list [Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]].
  (*
   = [[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]] : list position
   *)
End Test.

无法猜测 Coq 中嵌套匹配的递减参数

Cannot guess decreasing argument of fix for nested match in Coq

functional-programming

coq

totality