The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

This is another common current weakness of the fixpoints termination
checker in Coq. For "match_expression equivl equivr limit1 limit2)" to
be expanded in the definition of pair_apply, you need to define
pair_apply with parameters t, r and f outside the scope of the
recursive call, as below:

Definition pair_apply {t} {r} (f : t -> t -> r -> option r) :=
  fix pair_apply (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 r1 r2 rr
                          | None => None
                          end
     | _ => None
     end.

This can be diagnosed by explicitly giving a "{struct e1}" hint to the
definition of match_expression.

Notice that Pierre Boutillier has worked on an improvement of the
termination checker that supports your example without having to do
any modification (to be integrated to the development version within a
couple of weeks).

Hugo Herbelin

On Tue, May 29, 2012 at 08:49:44AM -0700, Kenneth Roe wrote:
> 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