The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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