The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Thanks a lot, especially for the long proof in [4], which helped me very much
to get an overview of the Lemmas you can use for rounding. The Gappa tool also
helps a lot.

I have another question concerning the Gappa tool. The manual says "The tactic
only handles goals and hypotheses that are pair of inequalities on real
numbers: b1 ≤ e ≤ b2 . The bounds have to be explicit dyadic
numbers."
I'd like to prove now, that rounding a real to a double keeps the value 
between
two integers (a : Z, a <= x <= a+1 -> a <= rnd(x) <= a+1). I can easily proof
this for any constant a, of course (assuming a is not to big, e.g. 0 <= a <=
1000), however I can't prove it for any a (at once) in this range (due to the
restriction mentioned above). Is there a way to bypass that restriction (maybe
with a sort of loop for all a), or any other way to prove it?


Sincerely,