The Coq mailing list

[Sylvie.Boldo AT inria.fr]

Hello,

I recently needed a function to compute the product of n values. I then 
discovered the function prod_f_SO ((nat->R)-> nat-> R) that, given a
function f:nat-> R, computes  f(1)*...*f(n). Note the f(0) is unused. It 
multiplies the values of f(i) from i from 1 to n...

This is surprising as f is defined on all N, and it is inconsistent with 
the corresponding adding function  sum_f_R0 that computes 
f(0)+f(1)+...+f(n).


It is not very elegant, but the most surprising is that the lemmas on 
prod_f_S0 seem to assume that f(0) is needed! 
For example (lemma prod_SO_pos), for the product to be nonnegative, I need 
all the values including the unused f(0) to be nonnegative.


OK, I was able to prove the same lemma without f(0) needing to be 
nonnegative, but it may be a good idea to change something (either the 
definition or the lemmas) to be coherent.
Personnally, I would vote on the definition to be changed for consistency 
with sum_f_R0.

Regards,

Sylvie Boldo


--
Sylvie Boldo, projet ProVal, INRIA Futurs, PCRI