Skip to Content.
Sympa Menu

coq-club - Re: Re: [Coq-Club] Estimate resulting error with [round_double]

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Re: [Coq-Club] Estimate resulting error with [round_double]


chronological Thread 
  • From: Michael<michaelschausten AT googlemail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: Re: [Coq-Club] Estimate resulting error with [round_double]
  • Date: Sun, 3 Oct 2010 12:32:44 +0200

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,



Archive powered by MhonArc 2.6.16.

Top of Page