The Coq mailing list

[Maria Joao Frade <mjf AT di.uminho.pt>]

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
----------------------------------------------------------------