The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

>> A nice trick by B. Barras & G. Gonthier some time ago on this list was
>> to use a "guard"  to the well_foundedness argument, which hides it.
>>
> I'm not sure to understand the interest of this trick.
> The only way to really prove the termination of the function is to be able 
> to give an upper bound of the number of recursive steps done in guard. In 
> that case, why > not use the {measure ....} construction.

But, sometime, the upper bound can be very big, and using measure (or
wf), wouldn't you start by evaluating this upper bound, by computing
the witness of termination, in order to exhibit all the constructors
needed for the recursion? In our case, the function was the
determinisation of NFA, and the bound was 2 to the power of the number
of states of the original automata. Which is quite big.

Here, using this guard, you still need to prove the well-foundedness
of the recursive calls, but you are given 2^n recursion steps, before
trying to compute the witness...

Here is the original post on this list from where this is originated :
http://logical.saclay.inria.fr/coq-puma/messages/7d5a3493009fd0e2

Thomas