为什么Coq无法定义参数化偶/奇列表的互归纳append函数？

Coq的Fixpoint递归定义有严格的终止性检查要求：递归调用的参数中必须有一个是外层传入参数的严格结构子项，以此保证递归一定会终止。
你代码的问题出在oapp函数的递归调用逻辑：

• 你定义的eapp函数预期第一个参数是递减的结构参数，应该是第一个拼接参数的子项
• 但你在oapp中调用eapp时，把两个参数写反了：eapp el el'，这里第一个参数是oapp的第二个输入el，而非oapp第一个输入ol的结构子项el'
• Coq找不到符合要求的递减参数，因此抛出错误。

只需要修正oapp中eapp调用的参数顺序即可，你也可以手动用{struct}关键字显式指定递减参数，避免Coq猜测出错，完整可运行代码如下：

Module mutual_induct.

  Inductive even_list (T: Set) : Set :=
  | ENil
  | ECons (t: T) (ol: odd_list T)
  with odd_list (T: Set) : Set :=
  | OCons (t: T) (el: even_list T).

  Fixpoint elength {T: Set} (el: even_list T) : nat :=
    match el with
    | ENil _ => 0
    | ECons _ _ ol => 1 + olength ol
    end
      
  with olength {T: Set} (ol: odd_list T) : nat :=
    match ol with
    | OCons _ _ el => 1 + elength el
    end.

  (* 显式指定递减参数是第一个偶列表el1 *)
  Fixpoint eapp {T: Set} (el1 el2: even_list T) {struct el1} : even_list T :=
    match el1 with
    | ENil _ => el2
    | ECons _ t' ol' => ECons T t' (oapp ol' el2)
    end
  (* 显式指定递减参数是奇列表ol *)
  with oapp {T: Set} (ol: odd_list T) (el: even_list T) {struct ol} : odd_list T :=
    match ol with
    | OCons _ t' el' => OCons T t' (eapp el' el) (* 这里修正了参数顺序 *)
    end.
           
End mutual_induct.

你可以用以下代码验证拼接功能正常：

(* 构造两个偶列表：[1,2] 和 [3,4] *)
Compute let el1 := ECons nat 1 (OCons nat 2 (ENil nat)) in
        let el2 := ECons nat 3 (OCons nat 4 (ENil nat)) in
        eapp el1 el2.

运行后会得到长度为4的偶列表ECons nat 1 (OCons nat 2 (ECons nat 3 (OCons nat 4 (ENil nat))))，符合预期。

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