The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Hi,

On Thu, 24 Sep 2009 13:14:49 +0200
Thomas Braibant 
<thomas.braibant AT gmail.com>
 wrote:

> I think that the important point here is that you omitted the proofs.
> 
> For example, the following does not work because you end the proof
> with Qed, and made the function opaque ...
> 
> Function factN (n : positive) {wf Plt n} : positive :=
> match n with
> | xH => xH
> | xO x => n * factN ( Ppred n)
> | xI x => n * factN ( Ppred n)
> end.
>   admit.
>   admit.
>   admit.
> Qed.
> 
This is perfectly true even if not documented (my mistakes sorry). 


> 
> If you have provided an actual proof, I guess you can reduce, even if
> it can be slow (because you compute the proof of accessibility of the
> argument you gave to the fonction)
> 
In fact, you should use the vm_compute strategy instead of the compute one. 
It should greatly decrease computation time.  

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


Bests,
Julien