Error: 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.

and a function beq_term to compare two terms define as follow :

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.

The definition of the function beq_term yields the error message:

Error: Cannot guess decreasing argument of fix.

So I am interested in how to convince Coq of the termination.

A good way to start is by convincing us that we can copy your code and get the same error you see and not something like: "Error: The reference VarIndex was not found in the current environment". I.e. we need a minimal reproducible example. — Anton Trunov
i have updated the post. Now you should have the " Error: Cannot guess decreasing argument of fix." — DerMann

larsr larsr · Accepted Answer · 2017-05-22T06:52:59

If you want to be able to use Coq's syntactic check in this simple example in particular, it is enough to write beq_list and beq_term into a single function.

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.

Error: Cannot guess decreasing argument of fix. Coq

1 Answers