我可以在Coq中进行“复杂的”相互递归而不使用let绑定吗？

Question

考虑以下一对相互递归的Coq数据类型，它们表示一个非空Forest的Tree，Tree的每个Branch都有一个额外的布尔标志，我们可以用isOK提取它。

Inductive Forest a : Type
  := Empty    : Forest a
  |  WithTree : Tree a -> Forest a -> Forest a
with Tree a : Type
  := Branch : bool -> a -> Forest a -> Tree a.

Arguments Empty    {_}.
Arguments WithTree {_} _ _.
Arguments Branch   {_} _ _ _.

Definition isOK {a} (t : Tree a) : bool :=
  match t with
  | Branch ok _ _ => ok
  end.

现在，如果忽略这个布尔标志，我们可以编写一对映射函数来将函数应用于Forest或Tree中的每个值，这很好：

Fixpoint mapForest_always {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_always f t) (mapForest_always f ts)
  end
with mapTree_always {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_always f ts)
  end.

但是，假设布尔值表示一些有效性检查，这在实际代码中会更复杂。所以我们首先检查布尔值，如果有必要的话，它实际上是递归的。这意味着我们有三个相互递归的函数，但其中一个函数只是简单地完成了工作。不幸的是，这是行不通的：

Fail Fixpoint mapForest_bad {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_bad f t) (mapForest_bad f ts)
  end
with mapTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  if isOK t
  then mapOKTree_bad f t
  else t
with mapOKTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_bad f ts)
  end.

问题是，mapTree_bad根据一个实际上并不小的参数调用mapOKTree_bad。

除…外mapOKTree_bad所做的只是经过一些预处理之后的一个额外步骤。这将永远终止，但Coq看不到这一点。为了说服终止检查器，我们可以定义mapOKTree_good，它是一个本地let-binding；然后，终止检查器将看穿let-binding，并允许我们定义mapForest_good和mapTree_good。如果我们想获得mapOKTree_good，那么在定义了相互递归的函数之后，我们可以使用一个简单的旧定义，该函数与let-binding具有相同的主体：

Fixpoint mapForest_good {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_good f t) (mapForest_good f ts)
  end
with mapTree_good {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  let mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
        match t with
        | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
        end in
  if isOK t
  then mapOKTree_good f t
  else t.

Definition mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
  end.

这个很管用，但它不漂亮。有什么方法可以说服Coq的终止检查器接受_bad变体，或者_good技巧是最好的吗？为我工作的命令(如Program Fixpoint或Function )也是完全合理的解决方案。

Answer 1

非常片面的回答:我们可以在定义mapOKTree_good之前用mapForest_good参数化的中间定义重构它的两个定义。

Definition mapOKTree_good_ {a} mapForest_good
           (f : a -> a) (t : Tree a) : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
  end.

Fixpoint mapForest_good {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_good f t) (mapForest_good f ts)
  end
with mapTree_good {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  if isOK t
  then mapOKTree_good_ mapForest_good f t
  else t.

Definition mapOKTree_good {a} := @mapOKTree_good_ a mapForest_good.