The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Eduardo Gimenez wrote:
> Hi,
>
> As far as I remember about a piece of code written more than 10 years 
> ago, the algorithm underlying the "Guarded" command starts by extracting 
> the proof term and then traverses it verifying that the condition holds 
> everywhere. There is no incremental verification (and possibly it will 
> be very  hard to implement). This means that the more you advance in 
> your proof, the slowlest the "Guarded" command becomes.

        Dear Eduardo,
this is not a problem with me.  However, a polynomial slow down
would be far more acceptable to me than the current exponential
slow down.
        I can probably be more explicit.  The generated proof
term is typically an expression that contains 18 calls to
some function f1.  The code for f1 contains 6 calls to f2,
f2 contains 6 calls to f3, f3 contains 18 calls to f4, and
so on.  If you analyze each branch in the control flow
separately, you're doomed.  If you analyze each of f1, f2,
f3, ..., only once, producing some kind of summary as to
which arguments decrease across calls, you retain the sharing
present in the initial proof term, and that should be fine.


> The command is not documented because it was NOT an acceptable solution 
> to me. Should be replaced some day by a typing system ensuring 
> termination (without using a guard condition).

        OK.  I wasn't hoping on a patch to Coq, or on a new
version, rather on a workaround.
        Best,


        -- Jean Goubault-Larrecq
        (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI).