coq - 错误 : Cannot guess decreasing argument of fix. Coq

Question

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 的定义产生错误消息:

Error: Cannot guess decreasing argument of fix.

所以我感兴趣的是如何说服 Coq 终止。

Answer 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.