# Library Flocq.Calc.Bracket

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
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.

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
| Gtloc_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_Exactl | _loc_Inexact Lt end
else
loc_Inexact
match Z.compare (2 × k) nb_steps with
| LtLt
| Eqmatch l with loc_ExactEq | _Gt end
| GtGt
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_Exactl | _loc_Inexact Lt end
else
loc_Inexact
match Z.compare (2 × k + 1) nb_steps with
| LtLt
| Eqmatch l with loc_Inexact ll | loc_ExactLt end
| GtGt
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.