coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,
- Re: [Coq-Club] Estimate resulting error with [round_double], Sylvie Boldo
- <Possible follow-ups>
- Re: Re: [Coq-Club] Estimate resulting error with [round_double], Michael
- Re: [Coq-Club] Estimate resulting error with [round_double], Guillaume Melquiond
- Re: Re: [Coq-Club] Estimate resulting error with [round_double], Michael
- Re: [Coq-Club] Estimate resulting error with [round_double], Guillaume Melquiond
Archive powered by MhonArc 2.6.16.