Library Flocq.Calc.Fcalc_bracket

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 Guillaume Melquiond

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format.


Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.

Section Fcalc_bracket.

Variable d u : R.
Hypothesis Hdu : (d < u)%R.

Inductive location := loc_Exact | loc_Inexact : comparison -> location.

Variable x : R.

Definition inbetween_loc :=
  match Rcompare x d with
  | Gt => loc_Inexact (Rcompare x ((d + u) / 2))
  | _ => loc_Exact
  end.

Locates a real number with respect to the middle of two other numbers.

Inductive inbetween : location -> Prop :=
  | inbetween_Exact : x = d -> inbetween loc_Exact
  | inbetween_Inexact l : (d < x < u)%R -> Rcompare x ((d + u) / 2)%R = l -> inbetween (loc_Inexact l).

Theorem inbetween_spec :
  (d <= x < u)%R -> inbetween inbetween_loc.

Theorem inbetween_unique :
  forall l l',
  inbetween l -> inbetween l' -> l = l'.

Section Fcalc_bracket_any.

Variable l : location.

Theorem inbetween_bounds :
  inbetween l ->
  (d <= x < u)%R.

Theorem inbetween_bounds_not_Eq :
  inbetween l ->
  l <> loc_Exact ->
  (d < x < u)%R.

End Fcalc_bracket_any.

Theorem inbetween_distance_inexact :
  forall l,
  inbetween (loc_Inexact l) ->
  Rcompare (x - d) (u - x) = l.

Theorem inbetween_distance_inexact_abs :
  forall l,
  inbetween (loc_Inexact l) ->
  Rcompare (Rabs (d - x)) (Rabs (u - x)) = l.

End Fcalc_bracket.

Theorem inbetween_ex :
  forall d u l,
  (d < u)%R ->
  exists x,
  inbetween d u x l.

Section Fcalc_bracket_step.

Variable start step : R.
Variable nb_steps : Z.
Variable Hstep : (0 < step)%R.

Lemma ordered_steps :
  forall k,
  (start + Z2R k * step < start + Z2R (k + 1) * step)%R.

Lemma middle_range :
  forall k,
  ((start + (start + Z2R k * step)) / 2 = start + (Z2R k / 2 * step))%R.

Hypothesis (Hnb_steps : (1 < nb_steps)%Z).

Lemma inbetween_step_not_Eq :
  forall x k l l',
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  (0 < k < nb_steps)%Z ->
  Rcompare x (start + (Z2R nb_steps / 2 * step))%R = l' ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact l').

Theorem inbetween_step_Lo :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  (0 < k)%Z -> (2 * k + 1 < nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt).

Theorem inbetween_step_Hi :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  (nb_steps < 2 * k)%Z -> (k < nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Gt).

Theorem inbetween_step_Lo_not_Eq :
  forall x l,
  inbetween start (start + step) x l ->
  l <> loc_Exact ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt).

Lemma middle_odd :
  forall k,
  (2 * k + 1 = nb_steps)%Z ->
  (((start + Z2R k * step) + (start + Z2R (k + 1) * step))/2 = start + Z2R nb_steps /2 * step)%R.

Theorem inbetween_step_any_Mi_odd :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x (loc_Inexact l) ->
  (2 * k + 1 = nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact l).

Theorem inbetween_step_Lo_Mi_Eq_odd :
  forall x k,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x loc_Exact ->
  (2 * k + 1 = nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt).

Theorem inbetween_step_Hi_Mi_even :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  l <> loc_Exact ->
  (2 * k = nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Gt).

Theorem inbetween_step_Mi_Mi_even :
  forall x k,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x loc_Exact ->
  (2 * k = nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Eq).

Computes a new location when the interval containing a real number is split into nb_steps subintervals and the real is in the k-th one. (Even radix.)

Definition new_location_even k l :=
  if Zeq_bool k 0 then
    match l with loc_Exact => l | _ => loc_Inexact Lt end
  else
    loc_Inexact
    match Zcompare (2 * k) nb_steps with
    | Lt => Lt
    | Eq => match l with loc_Exact => Eq | _ => Gt end
    | Gt => Gt
    end.

Theorem new_location_even_correct :
  Zeven nb_steps = true ->
  forall x k l, (0 <= k < nb_steps)%Z ->
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  inbetween start (start + Z2R nb_steps * step) x (new_location_even k l).

Computes a new location when the interval containing a real number is split into nb_steps subintervals and the real is in the k-th one. (Odd radix.)

Definition new_location_odd k l :=
  if Zeq_bool k 0 then
    match l with loc_Exact => l | _ => loc_Inexact Lt end
  else
    loc_Inexact
    match Zcompare (2 * k + 1) nb_steps with
    | Lt => Lt
    | Eq => match l with loc_Inexact l => l | loc_Exact => Lt end
    | Gt => Gt
    end.

Theorem new_location_odd_correct :
  Zeven nb_steps = false ->
  forall x k l, (0 <= k < nb_steps)%Z ->
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  inbetween start (start + Z2R nb_steps * step) x (new_location_odd k l).

Definition new_location :=
  if Zeven nb_steps then new_location_even else new_location_odd.

Theorem new_location_correct :
  forall x k l, (0 <= k < nb_steps)%Z ->
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  inbetween start (start + Z2R nb_steps * step) x (new_location k l).

End Fcalc_bracket_step.

Section Fcalc_bracket_scale.

Lemma inbetween_mult_aux :
  forall x d s,
  ((x * s + d * s) / 2 = (x + d) / 2 * s)%R.

Theorem inbetween_mult_compat :
  forall x d u l s,
  (0 < s)%R ->
  inbetween x d u l ->
  inbetween (x * s) (d * s) (u * s) l.

Theorem inbetween_mult_reg :
  forall x d u l s,
  (0 < s)%R ->
  inbetween (x * s) (d * s) (u * s) l ->
  inbetween x d u l.

End Fcalc_bracket_scale.

Section Fcalc_bracket_generic.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Specialization of inbetween for two consecutive floating-point numbers.

Definition inbetween_float m e x l :=
  inbetween (F2R (Float beta m e)) (F2R (Float beta (m + 1) e)) x l.

Theorem inbetween_float_bounds :
  forall x m e l,
  inbetween_float m e x l ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R.

Specialization of inbetween for two consecutive integers.

Definition inbetween_int m x l :=
  inbetween (Z2R m) (Z2R (m + 1)) x l.

Theorem inbetween_float_new_location :
  forall x m e l k,
  (0 < k)%Z ->
  inbetween_float m e x l ->
  inbetween_float (Zdiv m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Zmod m (Zpower beta k)) l).

Theorem inbetween_float_new_location_single :
  forall x m e l,
  inbetween_float m e x l ->
  inbetween_float (Zdiv m beta) (e + 1) x (new_location beta (Zmod m beta) l).

Theorem inbetween_float_ex :
  forall m e l,
  exists x,
  inbetween_float m e x l.

Theorem inbetween_float_unique :
  forall x e m l m' l',
  inbetween_float m e x l ->
  inbetween_float m' e x l' ->
  m = m' /\ l = l'.

End Fcalc_bracket_generic.