The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello Pierre,

thanks for the reference.

I was aware that the current Coq guardedness condition first reduces the 
body. However, still, the fully reduced version of my example

  fix foo (n : nat) : nat :=
    match n with
    | 0 => 0
    | S x => S (foo
       ((fix minus (n0 m : nat) {struct n0} : nat :=
         match n0 with
         | 0 => n0
         | S k =>
           match m with
           | 0 => n0
           | S l => minus k l
           end
         end) x 2))
    end

is not accepted by Giménez' guardedness condition (there the recursive 
argument of the recursive call to "foo" should be of the shape "z Q1 ... 
Qn" with "z" in the set of allowed variables). Here it is a "fix" construct.

I do not directly see whether it it covered by yours. Having a "fix" 
construct as the recursive argument of the recursive call to "foo" seems 
to be fine. While checking the body of the inner fix (after using the 
FixSpec rule) we have

  ..., minus ▶ ⊥, n0 ▶ <, m ▶ ⊥

After that, to check the body of the "S l" case in the second match, it 
seems to fail on

  minus k l

Am I missing something maybe?

Best,

Robbert

On 01/09/2013 12:17 PM, Pierre Boutillier wrote:
> Hi,
>
> The formal description of the current guardedness condition :
> http://hal.inria.fr/hal-00651780
>
> Very approximately (and the devil is in the details), it is Giménez
> guardedness condition but on the weak head normal form of the body of
> the fixpoint
>
> (
>      match n with
>      | 0 =>  0
>      | S x =>  S (foo (x - 2))
>      end.
> in your second example)
>
> All the best,
> Pierre B
>
> On 09/01/2013 12:09, Robbert Krebbers wrote:
> > Hello,
> >
> > today I noticed that the gcd function on nat is defined as follows
> >
> >    Fixpoint gcd a b :=
> >      match a with
> >      | O =>  b
> >      | S a' =>  gcd (b mod (S a')) (S a')
> >      end.
> >
> > I was quite surprised that this is accepted by Coq's guardedness
> > checker. After all, it is not obvious that (b mod (S a')) is indeed
> > structurally smaller than (S a').
> >
> > Also an example like
> >
> >    Fixpoint foo (n : nat) :=
> >      match n with
> >      | 0 =>  0
> >      | S x =>  S (foo (S x - 3))
> >      end.
> >
> > is happily accepted.
> >
> > This does not seem to be covered by, nor to be an obvious extension
> > of, the guardedness condition as defined in Giménez' 1994 "Codifying
> > guarded definitions with recursive schemes" to which (Chapter 4 of)
> > the reference manual refers.
> >
> > Is there a formal description of the current guardedness condition
> > that captures the above cases? Or an intuitive explanation on what it
> > is doing to check these.
> >
> > Robbert