The Coq mailing list

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

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.

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

Hope it helps.
Cheers,
Eduardo Gimenez.


Jean Goubault-Larrecq a écrit :
>     Hi again,
>
> to say a bit more, on rem_2421, 'Guarded' returns
> 'The condition holds up to here' in no time on
> the first two subgoals... and in 4h 6min. on
> the sole third subgoal.  (Only 15 to go, and
> we'll have completed rem_2421, on a bit less
> than 80000 remarks...)
>     Best,
>
>     -- Jean Goubault-Larrecq
>     (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI).
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> __________ Information NOD32 2942 (20080312) __________
>
> Ce message a ete verifie par NOD32 Antivirus System.
> http://www.nod32.com