エラー：修正の引数の減少を推測できません。コック

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. 

2つの用語を比較する機能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を1つの関数に記述すれば十分です。

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.