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.
Proof.
Theorem inbetween_unique :
forall l l',
inbetween l ->
inbetween l' ->
l =
l'.
Proof.
intros l l'
Hl Hl'.
inversion_clear Hl ;
inversion_clear Hl'.
apply refl_equal.
rewrite H in H0.
elim Rlt_irrefl with (1 :=
proj1 H0).
rewrite H1 in H.
elim Rlt_irrefl with (1 :=
proj1 H).
apply f_equal.
now rewrite <-
H0.
Qed.
Section Fcalc_bracket_any.
Variable l :
location.
Theorem inbetween_bounds :
inbetween l ->
(
d <=
x <
u)%
R.
Proof.
intros [
Hx|
l'
Hx Hl] ;
clear l.
rewrite Hx.
split.
apply Rle_refl.
exact Hdu.
now split ;
try apply Rlt_le.
Qed.
Theorem inbetween_bounds_not_Eq :
inbetween l ->
l <>
loc_Exact ->
(
d <
x <
u)%
R.
Proof.
intros [Hx|l' Hx Hl] H.
now elim H.
exact Hx.
Qed.
End Fcalc_bracket_any.
Theorem inbetween_distance_inexact :
forall l,
inbetween (
loc_Inexact l) ->
Rcompare (
x -
d) (
u -
x) =
l.
Proof.
intros l Hl.
inversion_clear Hl as [|
l'
Hl'
Hx].
now rewrite Rcompare_middle.
Qed.
Theorem inbetween_distance_inexact_abs :
forall l,
inbetween (
loc_Inexact l) ->
Rcompare (
Rabs (
d -
x)) (
Rabs (
u -
x)) =
l.
Proof.
End Fcalc_bracket.
Theorem inbetween_ex :
forall d u l,
(
d <
u)%
R ->
exists x,
inbetween d u x l.
Proof.
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.
Proof.
Lemma middle_range :
forall k,
((
start + (
start +
Z2R k *
step)) / 2 =
start + (
Z2R k / 2 *
step))%
R.
Proof.
intros k.
field.
Qed.
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').
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
intros x d s.
field.
Qed.
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.
Proof.
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.
Proof.
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.
Proof.
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).
Proof.
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).
Proof.
Theorem inbetween_float_ex :
forall m e l,
exists x,
inbetween_float m e x l.
Proof.
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'.
Proof.
End Fcalc_bracket_generic.