The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Hermann Lehner wrote:
> I'm trying to define a function 'SumFilterZ' in Coq that corresponds 
> to the addition of all integers between 'lo' and 'hi' if 'filter' is 
> true.

You should be able to do it by:
- Subtracting 'lo' from 'hi'
- Converting to [nat] (give up at this point (by, e.g., returning [None] 
or 0) if the result was negative)
- Calling a function that is primitive recursive on a natural number N, 
which takes an integer i and acts like your filter function for i..i+N 
(with conversions between naturals and integers as needed)