Library Flocq.Calc.Bracket
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2010-2018 Sylvie Boldo
Copyright (C) 2010-2018 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.
Copyright (C) 2010-2018 Guillaume Melquiond
Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format.
From Coq Require Import ZArith Reals Lia.
From Coq Require SpecFloat.
Require Import Zaux Raux Defs Float_prop.
Notation location := SpecFloat.location (only parsing).
Notation loc_Exact := SpecFloat.loc_Exact (only parsing).
Notation loc_Inexact := SpecFloat.loc_Inexact (only parsing).
Section Fcalc_bracket.
Variable d u : R.
Hypothesis Hdu : (d < u)%R.
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 :
∀ 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 :
∀ l,
inbetween (loc_Inexact l) →
Rcompare (x - d) (u - x) = l.
Theorem inbetween_distance_inexact_abs :
∀ l,
inbetween (loc_Inexact l) →
Rcompare (Rabs (d - x)) (Rabs (u - x)) = l.
End Fcalc_bracket.
Theorem inbetween_ex :
∀ d u l,
(d < u)%R →
∃ 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 :
∀ k,
(start + IZR k × step < start + IZR (k + 1) × step)%R.
Lemma middle_range :
∀ k,
((start + (start + IZR k × step)) / 2 = start + (IZR k / 2 × step))%R.
Hypothesis (Hnb_steps : (1 < nb_steps)%Z).
Lemma inbetween_step_not_Eq :
∀ x k l l',
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
(0 < k < nb_steps)%Z →
Rcompare x (start + (IZR nb_steps / 2 × step))%R = l' →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact l').
Theorem inbetween_step_Lo :
∀ x k l,
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
(0 < k)%Z → (2 × k + 1 < nb_steps)%Z →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact Lt).
Theorem inbetween_step_Hi :
∀ x k l,
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
(nb_steps < 2 × k)%Z → (k < nb_steps)%Z →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact Gt).
Theorem inbetween_step_Lo_not_Eq :
∀ x l,
inbetween start (start + step) x l →
l ≠ loc_Exact →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact Lt).
Lemma middle_odd :
∀ k,
(2 × k + 1 = nb_steps)%Z →
(((start + IZR k × step) + (start + IZR (k + 1) × step))/2 = start + IZR nb_steps /2 × step)%R.
Theorem inbetween_step_any_Mi_odd :
∀ x k l,
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x (loc_Inexact l) →
(2 × k + 1 = nb_steps)%Z →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact l).
Theorem inbetween_step_Lo_Mi_Eq_odd :
∀ x k,
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x loc_Exact →
(2 × k + 1 = nb_steps)%Z →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact Lt).
Theorem inbetween_step_Hi_Mi_even :
∀ x k l,
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
l ≠ loc_Exact →
(2 × k = nb_steps)%Z →
inbetween start (start + IZR nb_steps × step) x (loc_Inexact Gt).
Theorem inbetween_step_Mi_Mi_even :
∀ x k,
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x loc_Exact →
(2 × k = nb_steps)%Z →
inbetween start (start + IZR 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 Z.compare (2 × k) nb_steps with
| Lt ⇒ Lt
| Eq ⇒ match l with loc_Exact ⇒ Eq | _ ⇒ Gt end
| Gt ⇒ Gt
end.
Theorem new_location_even_correct :
Z.even nb_steps = true →
∀ x k l, (0 ≤ k < nb_steps)%Z →
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
inbetween start (start + IZR 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 Z.compare (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 :
Z.even nb_steps = false →
∀ x k l, (0 ≤ k < nb_steps)%Z →
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
inbetween start (start + IZR nb_steps × step) x (new_location_odd k l).
Definition new_location :=
if Z.even nb_steps then new_location_even else new_location_odd.
Theorem new_location_correct :
∀ x k l, (0 ≤ k < nb_steps)%Z →
inbetween (start + IZR k × step) (start + IZR (k + 1) × step) x l →
inbetween start (start + IZR nb_steps × step) x (new_location k l).
End Fcalc_bracket_step.
Section Bracket_plus.
Theorem inbetween_plus_compat :
∀ x d u l t,
inbetween x d u l →
inbetween (x + t) (d + t) (u + t) l.
Theorem inbetween_plus_reg :
∀ x d u l t,
inbetween (x + t) (d + t) (u + t) l →
inbetween x d u l.
End Bracket_plus.
Section Fcalc_bracket_scale.
Theorem inbetween_mult_compat :
∀ 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 :
∀ 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 :
∀ 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 (IZR m) (IZR (m + 1)) x l.
Theorem inbetween_float_new_location :
∀ x m e l k,
(0 < k)%Z →
inbetween_float m e x l →
inbetween_float (Z.div m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Zmod m (Zpower beta k)) l).
Theorem inbetween_float_new_location_single :
∀ x m e l,
inbetween_float m e x l →
inbetween_float (Z.div m beta) (e + 1) x (new_location beta (Zmod m beta) l).
Theorem inbetween_float_ex :
∀ m e l,
∃ x,
inbetween_float m e x l.
Theorem inbetween_float_unique :
∀ 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.