The Coq mailing list

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

Le samedi 02 octobre 2010 à 17:42 +0200, Michael a écrit :

> 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?

Unfortunately, Gappa is not able to prove it, I think. My guess is that
it is missing some facts about monotony. It is able to prove that
'rnd(x)' is almost between 'a' and 'a+1', but that's not really
interesting.

If you want to bypass the restriction on the bounds, you have to modify
your inequalities so that you don't have to bypass it. In your case (the
uninteresting version with enlarged bounds), that means:

Notation rnd := (rounding_float roundNE 53 1074).
Goal forall a, (-100000 <= a <= 100000)%R ->
     forall x, (0 <= x - a <= 1)%R ->
  (- powerRZ 2 (-37) <= rnd x - a <= 137438953473 * powerRZ 2 (-37))%R.
gappa.
Qed.

(Just in case you wonder, the right-hand side is 1 + 2**(-37).)

As for your other idea, it is indeed possible to do loops in Coq. But
I'm not sure it is sane to do it on so many values. Script below is for
0 <= a <= 10.

Lemma plop :
  forall (P : Z -> Prop) m n, P m ->
  (forall a, (m + 1 <= a <= n)%Z -> P a) ->
  (forall a, (m <= a <= n)%Z -> P a).
Proof.
intros P m n Pm HP a Ha.
destruct (Z_eq_dec m a) as [H|H].
now rewrite <- H.
apply HP.
omega.
Qed.

Goal
  forall a, (0 <= a <= 10)%Z ->
  forall x,
  (Float1 a <= x <= Float1 (a + 1))%R ->
  (Float1 a <= rnd x <= Float1 (a + 1))%R.
Proof.
do 10 (
  intros a Ha;
  apply (plop (fun a => forall x : R,
    (Float1 a <= x <= Float1 (a + 1))%R ->
    (Float1 a <= rnd x <= Float1 (a + 1))%R)) with (3 := Ha);
  simpl; [gappa|clear a Ha]).
intros a Ha.
rewrite (Zle_antisym _ _ (proj2 Ha) (proj1 Ha)).
simpl. gappa.
Qed.

Best regards,

Guillaume