The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

You have to write it as a nested fixed point:

Require Import List Arith Bool.

Definition beq_list {A} (f : A -> A -> bool) : list A -> list A -> bool :=
  fix go l k :=
  match l, k with
  | nil, nil => true
  | x :: l, y :: k => f x y && go l k
  | _, _ => false
  end.

Definition absVar := nat.
Parameter (id ExpValue heap : Type).
Parameter (beq_id : id -> id -> bool).

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 x (e1 : absExp x) (e2 : absExp x) : bool :=
   match e1 with
   | AbsNatVal v => match e2 with AbsNatVal v2 => beq_nat v v2 | _ => 
false end
   | AbsVar v => match e2 with AbsVar v2 =>beq_id v v2 | _ => false end
   | AbsQVar v => match e2 with AbsQVar v2 => beq_nat v v2 | _ => false end
   | AbsFun id1 l1 => match e2 with AbsFun id2 l2 => beq_id id1 id2 && 
beq_list (beq_absExp x) l1 l2 | _ => false end
   | _ => false
   end.

On 05/24/2012 04:15 PM, Kenneth Roe wrote:
> 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