The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

I also tried to bring a "in the middle" to circumvent the gappa restrictions,
however (as you mentioned), this doesn't help me to prove that (rnd x) stays
between a and a+1 (only nearly).

My idea now was to try it without gappa in another way: Prove only: a : Z, x :
R, -1000 <= a <= 1000 -> a <= x -> a <= double_value (round_double 
nearest_even
x))
I already know that a is exactly a float, so I tried to prove " x < a ->
False". I already got to something like "RND_EvenClosest bdouble radix 53 x),
however I don't know how to make the "step" from here to "EvenClosest".
My thought was (hope you understand it), that if (rnd x < a), then |x-a| < |x 
-
rnd x|, which should be a contradiction (shouldn't it). However, I don't 
manage
to implement this in coq, I hope you can help me here.


Sincerely,