The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

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