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: Sat, 2 Oct 2010 17:42:18 +0200

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 &#8804; e &#8804; 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,



Archive powered by MhonArc 2.6.16.

Top of Page