归纳类型和 nat 上的相互递归答案

【问题标题】：mutual recursion on an inductive type and nat归纳类型和 nat 上的相互递归
【发布时间】：2018-05-22 23:44:05
【问题描述】：

考虑这个例子：

Inductive T :=
| foo : T
| bar : nat -> T -> T.

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => evalBar x n
  end
with evalBar (x:T) (n:nat) {struct n} : nat :=
  match n with
  | O => 0
  | S n' => (evalT x) + (evalBar x n')
  end.

Coq 以错误拒绝它：对 evalBar 的递归调用的主要参数等于“n”而不是“x”。

我知道终止检查器被两种不相关的归纳类型（T 和 nat）弄糊涂了。但是，看起来我试图定义的函数确实会终止。如何让 Coq 接受它？

【问题讨论】：

标签： recursion coq termination

【解决方案1】：

另一种解决方案是使用嵌套的固定点。

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => let fix evalBar n {struct n} :=
                 match n with
                 | 0 => 0
                 | S n' => Nat.add (evalT x) (evalBar n')
                 end
               in evalBar n
  end.

重要的一点是从evalBar 中删除参数x。因此，对evalT 的递归调用是在来自bar n x 的x 上完成的，而不是作为evalBar 的参数给出的x，因此终止检查器可以验证evalT 的定义。

这与使另一个答案中提出的带有nat_rec 的版本起作用的想法相同。

【讨论】：

【解决方案2】：

我找到的一个解决方案是使用nat_rec 而不是evalBar：

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => @nat_rec _ 0 (fun n' t' => (evalT x) + t') n
  end.

它有效，但我希望我可以将 nat_rec 隐藏在 evalBar 定义下以隐藏详细信息。在我的实际项目中，这样的构造被多次使用。

【讨论】：