如何获得嵌套修复的归纳原则

Question

我正在使用一个搜索一系列值的函数。

Require Import List.

(* Implementation of ListTest omitted. *)
Definition ListTest (l : list nat) := false.

Definition SearchCountList n :=
  (fix f i l := match i with
  | 0 => ListTest (rev l)
  | S i1 =>
    (fix g j l1 := match j with
    | 0 => false
    | S j1 =>
      if f i1 (j :: l1)
      then true
      else g j1 l1
    end) (n + n) (i :: l)
  end) n nil
.

我希望能够对这个函数进行推理。

但是，我似乎无法让 coq 的内置归纳原理工具工作。

Functional Scheme SearchCountList := Induction for SearchCountList Sort Prop.

Error: GRec not handled

看起来 coq 是为处理相互递归而不是嵌套递归而设置的。在这种情况下，我基本上有 2 个嵌套的 for 循环。

然而，翻译成相互递归也不是那么容易：

Definition SearchCountList_Loop :=
  fix outer n i l {struct i} :=
    match i with
    | 0 => ListTest (rev l)
    | S i1 => inner n i1 (n + n) (i :: l)
    end
  with inner n i j l {struct j} :=
    match j with
    | 0 => false
    | S j1 =>
      if outer n i (j :: l)
      then true
      else inner n i j1 l
    end
  for outer
.

但这会产生错误

对内部的递归调用的主要参数等于 “n + n”而不是“i1”。

所以，看来我需要使用 measure 让它直接接受定义。我有时会重置 j 很困惑。但是，在嵌套设置中，这是有道理的，因为 i 减少了，而 i 是外循环。

那么，有没有一种处理嵌套递归的标准方法，而不是相互递归？有没有更简单的方法来推理这些案例，而不涉及制作单独的归纳定理？由于我还没有找到自动生成的方法，我想我还是坚持直接写归纳原理。

Answer 1

在这种情况下有一个避免相互递归的技巧：您可以在 f 中计算 f i1 并将结果传递给 g。

Fixpoint g (f_n_i1 : list nat -> bool) (j : nat) (l1 : list nat) : bool :=
  match j with
  | 0 => false
  | S j1 => if f_n_i1 (j :: l1) then true else g f_n_i1 j1 l1
  end.

Fixpoint f (n i : nat) (l : list nat) : bool :=
  match i with
  | 0 => ListTest (rev l)
  | S i1 => g (f n i1) (n + n) (i :: l)
  end.

Definition SearchCountList (n : nat) : bool := f n n nil.

您确定原始代码中的简单归纳还不够吗？那么有根据的归纳呢？