The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le dimanche 03 octobre 2010 à 12:33 +0200, Michael a écrit :
> 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.

If you are going the manual way, there is a much simpler proof. Since
"a" is exactly a float, it also means it is equal to its own rounded
value "rnd(a)". Therefore your goal "a <= rnd(x)" can be rewritten to
"rnd(a) <= rnd(x)" which is true by monotonicity of "rnd".

Best regards,

Guillaume