The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

> Could someone please tell us  how the guardedness condition test is
> being done ?

Dear Maria Joao,

In the first version of the guardedness condition that Christine
Paulin implemented for the V5.10 version, she introduced the
possibility of placing a pattern-matching destructuration as the
argument of a recursive call, provided that two condition are
fulfilled:
 (1) the argument of the pattern-matching expression is smaller 
     than the formal argument of the function;
 (2) all the branches of the pattern-matching yields a pattern
 variable.

Such kind of definitions are really necessary when writing functions
based on well-founded recursion (see Coq's tutorial on recursive types
for an example).  I guess that this is the condition that is still
described in the V6.3 of Coq's reference manual.

In 1998, I extend Christine's condition on pattern-matching
expressions to the case of recursive functions as follows: a recursive
call (f (g a)) of function f with formal parameter x is accepted if g
is a recursive function, and all the cases in g yield either a pattern
variable smaller than x, or an application of g. The idea behind this
extension is that you can easily prove that (g a) is smaller than x by
induction on the argument of g. Furthermore, when the real argument
<a> of g is strictly smaller than x, this information is transmitted to the
formal argument of g, and used when checking that every branch of g
returns something smaller than x. As far as I remember, this extension
has never been documented, at least in the reference manual.

This is why your first definition of div is accepted (the function
minus corresponds to the function g mentioned above):

=================================================================
Fixpoint minus [x:nat] : nat -> nat :=  
  [y:nat] Cases x of
            O      => O
          | (S x') => Cases y of
                         O     => x
                      | (S y') => (minus x' y')
                      end
          end.
Fixpoint div [x:nat] : nat -> nat :=
  [y:nat] Cases x of
             O     => O
          | (S x') => (S (div (minus x' y) y))
           end.
=================================================================

Now, if you modify the definition of g so that it returns the
constructor O instead of the variable x, then the function minus does
not longer satisfy the guardedness condition, since the first branch
that cannot be recognized by the algorithm as being strictly 
smaller than the formal argument of div.

This is yet another example of how using a syntactical condition for
ensuring termination make the recursive definitions to strongly depend
on the way they are presented.

Best wishes,
Eduardo Gimenez.

> Hello,
> 
> while trying to understand Coq's mechanism for
> guarded recursive definitions, we got surprised
> because Coq accepted the following
> div function:
> 
> 
> Fixpoint minus [x:nat] : nat -> nat :=
>   [y:nat] Cases x of
>                O => x
>          | (S x') => Cases y of
>                            O => x
>                     | (S y') => (minus x' y')
>              end
>          end.
> 
> 
> Fixpoint div [x:nat] : nat -> nat :=
>   [y:nat] Cases x of
>                 O => O
>          | (S x') => (S (div (minus x' y) y))
>           end.
> 
> (* div is recursively defined *)
> 
> 
> Then we modify the function minus by an equivalent one
> (note that we only replace  x by O,  in the case  x is O)
> 
> Fixpoint minus [x:nat] : nat -> nat :=
>   [y:nat] Cases x of
>                O => O
>          | (S x') => Cases y of
>                            O => x
>                     | (S y') => (minus x' y')
>              end
>          end.
> 
> 
> Fixpoint div [x:nat] : nat -> nat :=
>   [y:nat] Cases x of
>                 O => O
>          | (S x') => (S (div (minus x' y) y))
>           end.
> 
> (* is not well-formed *)
> 
> and the div function is not accepted.
> 
> 
> Could someone please tell us  how the guardedness condition test is
> being done ?
> 
> Thank you in advance,
> 
>      Maria Joao
> 
> ----------------------------------------------------------------
> Maria Joao Gomes Frade                email:  
> mjf AT di.uminho.pt
> Departamento de Informatica
> Universidade do Minho
> Campus de Gualtar                     TEL: +351 253 60 44 70
> 4710-057 Braga   (PORTUGAL)           FAX: +351 253 60 44 71
> ----------------------------------------------------------------
-- 
----------------------------------------------------------
Eduardo Gimenez                Tel :   (33) 1 30 97 25 13 
Trusted Logic SA               Std :   (33) 1 30 97 25 00 
5, rue du Bailliage            Fax :   (33) 1 30 97 25 19 
78000 Versailles               Web : www.trusted-logic.fr 
----------------------------------------------------------