The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I have a recursive Gallina function that uses a nat-typed fuel arg to
guarantee termination.  In cases where the function terminates prior to
running out of fuel, I've found that larger than necessary fuel args
are very costly. For example, with a fuel value of 100, the function
takes 30 times longer than if the fuel value is 10 (neither runs out of
fuel, all other args are the same). In both cases, the computation was
done with vm_cast_no_check. Nothing is done with the fuel arg other
than the usual "match fuel with 0 => done | S n => loop n"
recursion idiom.

I guess this is probably due to the overhead of nats in Gallina.  But
it is still surprising to me, considering that if I wrote a function to
traverse the first 8 links in a list, I wouldn't expect it to take 30
times longer with a 100-element list than a 10-element list.

Is there a way around this?  I'd like to use a constant fuel value
that is plenty large enough, without having to compute one from the
function's arguments that is just barely large enough.