The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Continuing on-- I have the same AbsExp declaration as before.  However, now I've written a function that matches two expressions.  It is defined as follows:

Fixpoint pair_apply {t} {r} (f : t -> t -> r -> option r) (l1 : list t) (l2 : list t) (ret : r) : option r :=
    match (l1,l2) with
    | (nil,nil) => Some ret
    | (f1::r1,f2::r2) => match f f1 f2 ret with
                         | Some rr => pair_apply f r1 r2 rr
                         | None => None
                         end
    | _ => None
    end.

Fixpoint match_expression {f} (equivl : list (list (@absExp f))) (equivr : list (list (@absExp f))) (limit1 : list absType) (limit2 : list absType)
                                            (e1 : @absExp f) (e2 : @absExp f) (pairs : list (nat * nat)) : option (list (nat * nat)) :=
    match (e1,e2) with
    | (AbsNatVal v1,AbsNatVal v2) => if beq_nat v1 v2 then Some pairs else None
    | (AbsVar v1,AbsVar v2) => if beq_id v1 v2 then Some pairs else if equiv_absExp (AbsVar v1) (AbsVar v2) equivl equivr then Some pairs else None
    | (AbsQVar v1,AbsQVar v2) => if ble_nat (length limit1) v1 then
                                     if beq_nat v1 ((v2+(length limit1))-(length limit2)) then Some pairs else None
                                 else if mem_pair (v1,v2) pairs then
                                     Some pairs
                                 else if ble_nat (length limit2) v2 then
                                     None
                                 else if no_first v1 pairs then
                                     if no_second v2 pairs then
                                         match (nth v1 limit1 AbsNat,nth v2 limit2 AbsNat) with
                                         | (AbsNat,AbsNat) => Some ((v1,v2)::pairs)
                                         | (AbsHeap,AbsHeap) => Some ((v1,v2)::pairs)
                                         | _ => None
                                         end
                                     else None
                                 else None
    | (AbsFun i1 el1,AbsFun i2 el2) => if beq_id i1 i2 then
                                           pair_apply (match_expression equivl equivr limit1 limit2) el1 el2 pairs
                                       else None
    | _ => None
    end.

I get the same error as before "Cannot guess decreasing argument for fix."  How do I fix this problem?

                 - Ken

> Date: Thu, 24 May 2012 16:32:57 +0200
> From: mailinglists AT robbertkrebbers.nl
> To: kendroe AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Trouble with a recursive definition
>
> 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