如何让Coq接受归纳类型与nat的互递归定义？

这事儿我熟！Coq的默认终止检查器对互递归函数确实有个“死板”的限制——它要求所有互递归函数的主递归参数得属于同一个归纳类型，但你的evalT主参数是自定义的T类型，evalBar的主参数是nat，俩类型不搭，所以就触发了报错。不过放心，有好几种办法能让Coq接受这个定义，给你列几个常用的：

方案1：用Program Fixpoint手动指定终止度量 #

Program Fixpoint允许你给每个函数指定一个“终止度量”，简单说就是一个能衡量参数“大小”的数值，你只需要证明每次递归调用的度量都会严格变小，Coq就会认可函数的终止性。

示例代码：

Require Import Program.Wf.
Require Import Arith.

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

Program Fixpoint evalT (t:T) {measure (size t)} : nat :=
  match t with
  | foo => 1
  | bar n x => evalBar x n
  end
with evalBar (x:T) (n:nat) {measure n} : nat :=
  match n with
  | O => 0
  | S n' => (evalT x) + (evalBar x n')
  end.
Next Obligation.
  (* 证明evalT x的参数比evalT (bar n x)的参数结构更小 *)
  simpl; apply lt_S_n.
Qed.
Next Obligation.
  (* 证明evalBar x n'的参数n'比n更小 *)
  apply lt_n_S.
Qed.
Next Obligation.
  (* 确认nat的小于关系是良基的（Coq自动能处理） *)
  apply wf_nat.
Qed.

方案2：把互递归改成单递归（最简洁） #

其实你可以把evalBar作为evalT的局部辅助函数，这样就避开了互递归的类型限制，Coq的终止检查器能直接识别出参数的递减关系：

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

Fixpoint evalT (t:T) : nat :=
  match t with
  | foo => 1
  | bar n x =>
      (* 把evalBar嵌套在bar分支里，作为局部函数 *)
      let fix evalBar (m:nat) : nat :=
        match m with
        | O => 0
        | S m' => evalT x + evalBar m'
        end
      in evalBar n
  end.

这个版本里，evalBar的递归参数m每次都会减1，而evalT x的参数x是bar n x的子项，结构肯定比原参数小，Coq会直接通过检查，连额外证明都不需要。

方案3：用Function命令支持跨类型互递归 #

如果你一定要保留互递归的结构，可以用Coq的Recdef库提供的Function命令，它支持更灵活的终止性证明，包括跨不同归纳类型的互递归：

Require Import Recdef.

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

Function evalT (t:T) : nat :=
  match t with
  | foo => 1
  | bar n x => evalBar x n
  end
with evalBar (x:T) (n:nat) : nat :=
  match n with
  | O => 0
  | S n' => evalT x + evalBar x n'
  end.
Proof.
  (* 定义一个组合的良基关系：要么T类型的参数结构更小，要么nat参数更小 *)
  intros.
  apply (well_founded_compose (Wf_nat.lt_wf) (size)) with (x := (x, n)).
  - intros (x1, n1) (x2, n2) H.
    destruct H as [H1 | H2].
    + left; apply H1.
    + right; apply H2.
  - destruct t; simpl.
    + auto.
    + right; apply lt_n_S.
  - destruct n; simpl.
    + auto.
    + left; apply le_n_S; reflexivity.
Qed.

如果只是简单场景，方案2绝对是最省心的；如果必须保留互递归结构，方案1或3都能解决问题。

内容的提问来源于stack exchange，提问作者krokodil