The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I have entered the following to define an abstract _expression_ type and a simple equality operator between expressions:

Inductive absExp ( f : id -> list ExpValue -> ExpValue ) : Type :=
   | AbsNatVal : nat -> absExp f
   | AbsHeapVal : heap -> absExp f
   | AbsVar : id -> absExp f
   | AbsQVar : absVar -> absExp f
   | AbsFun : id -> list (absExp f) -> absExp f.

Fixpoint beq_absExp_list x (e1 : list (absExp x)) (e2 : list (absExp x)) : bool :=
   match e1 with
   | nil => match e2 with nil => true | _ => false end
   | (AbsNatVal v)::r1 => match e2 with (AbsNatVal v2)::r2 => if beq_nat v v2 then beq_absExp_list x r1 r2 else false | _ => false end
   | (AbsVar v)::r1 => match e2 with (AbsVar v2)::r2 => if beq_id v v2 then beq_absExp_list x r1 r2 else false | _ => false end
   | (AbsQVar v)::r1 => match e2 with (AbsQVar v2)::r2 => if beq_nat v v2 then beq_absExp_list x r1 r2 else false | _ => false end
   | ((AbsFun id1 l1)::r1) => match e2 with
                                 ((AbsFun id2 l2)::r2) => if beq_id id1 id2 then
                                     if beq_absExp_list x l1 l2 then beq_absExp_list x r1 r2 else false else false | _ => false end
   | _ => false
   end.

I get the error "Error: Cannot guess decreasing argument of fix."  The problem is the second to last case which handles AbsFun.  I further isolated the problem to the fact that l1 and l2 are not recognized as subterms of e1 and e2.  How can I work around this issue?

                - Ken