The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

> I'm trying to re-play Eduardo Gimenez's proof of well-founded
> recursion given in the tutorial on recursive types, with the div
> function.
> The proof of div (p.36) doesn't save:
> 
>  Condition violated : Recursive call applied to an illegal term
> The recursive definition
> [x,y:nat; H:(Acc nat Lth x)]
>  Cases (iseq x O) of
>    (left _) => O
>  | (right a) =>
>     Cases (iseq y O) of
>       (left _) => x
>     | (right a0) => (S (div (minus x y) y (decrease x y H a a0)))
>     end
>  end
> is not well-formed


Hi Pablo,

You are pointing to one of the drawbacks of using an auxiliary side
condition to ensure the termination of a recursive definition: in
order to verify that the term (decrease x y H a a0) in the recursive
call of div is smaller than its formal argument H, Coq has to unfold
the definition of "decrease" and check what it does with H.  However,
in your script "decrease" is an opaque constant (because you saved it
with the "Qed" command and not with "Defined", as it is done in the
tutorial), and hence cannot be unfolded.

The constant can be made unfoldable using the Transparent
command. Once this is done, Coq realizes that the definition is correct:

-------------------------------------------------------------------
div < Guarded.
Condition violated : Recursive call applied to an illegal term
The recursive definition
[x,y:nat; H:(Acc nat Lth x)]
 Cases (iseq x O) of
   (left _) => O
 | (right a) => 
    Cases (iseq y O) of
      (left _) => x
    | (right a0) => (S (div (minus x y) y (decrease x y H a a0)))
    end
 end
is not well-formed

div < Transparent decrease.

div < Guarded.
The condition holds up to here
div < Defined.
div is defined
-------------------------------------------------------------------

I have advocated many times for replacing the guardedness side
condition by a type system where the termination of div can be cheked
directly from the type of "decrease", and not from its
definition. Such a type system actually exists (see the article
"Structural Recursive Definitions in type theory" at
http://pauillac.inria.fr/~gimenez/papers.html).  Unfortunately, its
implementation would require some important modifications in Coq's
core, so I guess that it will not be available to the users very
soon...

Best wishes,
Eduardo Gimenez.