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: 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 ≤ e ≤ 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,
- 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.