错误：无法猜测修复的递减参数。考克答案

【问题标题】：Error: Cannot guess decreasing argument of fix. Coq错误：无法猜测修复的递减参数。考克
【发布时间】：2017-05-21 13:24:05
【问题描述】：

I have the following definition for terms :

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Import ListNotations.

Definition VarIndex:Type := nat.


Inductive Term : Type :=
   |Var : VarIndex -> Term
   |Comb: string   -> (list Term) -> Term.


 (*compare two list *)
Fixpoint beq_list {X:Type} (l l' :list X) (EqX :X -> X -> bool): bool :=
     match l with
       | [] => match l' with
                | []  => true
                | a   => false
              end
       | (x::xs) => 
              match l' with
                |[]      => false
                |(y::ys) => if (EqX x y) then beq_list xs ys EqX else false 
              end
     end.


Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil       => 0
  | cons _ l' => S (length l')
  end.

和一个函数beq_term 来比较两个术语，定义如下：

Fixpoint beq_term (t1:Term)  (t2:Term) : bool :=
   match t1, t2 with
    | Var i, Var j             => beq_nat i j
    | Var _, Comb _ _           => false
    |Comb _ _, Var _            => false
    |(Comb s1 ts1), Comb s2 ts2 => if(beq_nat (length ts1) (length ts2)) 
                                   then beq_list ts1 ts2 beq_term
                                   else false
  end.

函数beq_term的定义产生错误信息：

错误：无法猜测 fix 的递减参数。

所以我对如何说服 Coq 终止协议很感兴趣。

【问题讨论】：

一个好的开始方法是说服我们我们可以复制您的代码并得到与您看到的相同的错误，而不是类似：“错误：参考 VarIndex在当前环境中找不到”。 IE。我们需要一个minimal reproducible example。
我已经更新了帖子。现在你应该有“错误：无法猜测修复的递减参数。”

标签： coq totality

【解决方案1】：

如果你特别想在这个简单的例子中使用 Coq 的语法检查，将 beq_list 和 beq_term 写到一个函数中就足够了。

Fixpoint beq_list (l l' :list Term) : bool :=
  match l, l' with
  | [], [] => true
  | (Var i)::xs, (Var j)::ys => beq_nat i j && beq_list xs ys
  | (Comb s1 ts1)::xs, (Comb s2 ts2)::ys => beq_list xs ys
  | _,_ => false
  end.

【讨论】：