1 files changed, 688 insertions, 0 deletions

diff --git a/flocq/Calc/Fcalc_bracket.v b/flocq/Calc/Fcalc_bracket.v
new file mode 100644
index 0000000..dd4bd97
--- /dev/null
+++ b/flocq/Calc/Fcalc_bracket.v
@@ -0,0 +1,688 @@
+(**
+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
+#<br />#
+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.
+Proof.
+intros Hx.
+unfold inbetween_loc.
+destruct (Rcompare_spec x d) as [H|H|H].
+now elim Rle_not_lt with (1 := proj1 Hx).
+now constructor.
+constructor.
+now split.
+easy.
+Qed.
+
+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.
+intros l Hl.
+rewrite Rabs_left1.
+rewrite Rabs_pos_eq.
+rewrite Ropp_minus_distr.
+now apply inbetween_distance_inexact.
+apply Rle_0_minus.
+apply Rlt_le.
+apply (inbetween_bounds _ Hl).
+apply Rle_minus.
+apply (inbetween_bounds _ Hl).
+Qed.
+
+End Fcalc_bracket.
+
+Theorem inbetween_ex :
+  forall d u l,
+  (d < u)%R ->
+  exists x,
+  inbetween d u x l.
+Proof.
+intros d u [|l] Hdu.
+exists d.
+now constructor.
+exists (d + match l with Lt => 1 | Eq => 2 | Gt => 3 end / 4 * (u - d))%R.
+constructor.
+(* *)
+set (v := (match l with Lt => 1 | Eq => 2 | Gt => 3 end / 4)%R).
+assert (0 < v < 1)%R.
+split.
+unfold v, Rdiv.
+apply Rmult_lt_0_compat.
+case l.
+now apply (Z2R_lt 0 2).
+now apply (Z2R_lt 0 1).
+now apply (Z2R_lt 0 3).
+apply Rinv_0_lt_compat.
+now apply (Z2R_lt 0 4).
+unfold v, Rdiv.
+apply Rmult_lt_reg_r with 4%R.
+now apply (Z2R_lt 0 4).
+rewrite Rmult_assoc, Rinv_l.
+rewrite Rmult_1_r, Rmult_1_l.
+case l.
+now apply (Z2R_lt 2 4).
+now apply (Z2R_lt 1 4).
+now apply (Z2R_lt 3 4).
+apply Rgt_not_eq.
+now apply (Z2R_lt 0 4).
+split.
+apply Rplus_lt_reg_r with (d * (v - 1))%R.
+ring_simplify.
+rewrite Rmult_comm.
+now apply Rmult_lt_compat_l.
+apply Rplus_lt_reg_r with (-u * v)%R.
+replace (- u * v + (d + v * (u - d)))%R with (d * (1 - v))%R by ring.
+replace (- u * v + u)%R with (u * (1 - v))%R by ring.
+apply Rmult_lt_compat_r.
+apply Rplus_lt_reg_r with v.
+now ring_simplify.
+exact Hdu.
+(* *)
+set (v := (match l with Lt => 1 | Eq => 2 | Gt => 3 end)%R).
+rewrite <- (Rcompare_plus_r (- (d + u) / 2)).
+rewrite <- (Rcompare_mult_r 4).
+2: now apply (Z2R_lt 0 4).
+replace (((d + u) / 2 + - (d + u) / 2) * 4)%R with ((u - d) * 0)%R by field.
+replace ((d + v / 4 * (u - d) + - (d + u) / 2) * 4)%R with ((u - d) * (v - 2))%R by field.
+rewrite Rcompare_mult_l.
+2: now apply Rlt_Rminus.
+rewrite <- (Rcompare_plus_r 2).
+ring_simplify (v - 2 + 2)%R (0 + 2)%R.
+unfold v.
+case l.
+exact (Rcompare_Z2R 2 2).
+exact (Rcompare_Z2R 1 2).
+exact (Rcompare_Z2R 3 2).
+Qed.
+
+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.
+intros k.
+apply Rplus_lt_compat_l.
+apply Rmult_lt_compat_r.
+exact Hstep.
+apply Z2R_lt.
+apply Zlt_succ.
+Qed.
+
+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.
+intros x k l l' Hx Hk Hl'.
+constructor.
+(* . *)
+assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
+split.
+apply Rlt_le_trans with (2 := proj1 Hx').
+rewrite <- (Rplus_0_r start) at 1.
+apply Rplus_lt_compat_l.
+apply Rmult_lt_0_compat.
+now apply (Z2R_lt 0).
+exact Hstep.
+apply Rlt_le_trans with (1 := proj2 Hx').
+apply Rplus_le_compat_l.
+apply Rmult_le_compat_r.
+now apply Rlt_le.
+apply Z2R_le.
+omega.
+(* . *)
+now rewrite middle_range.
+Qed.
+
+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.
+intros x k l Hx Hk1 Hk2.
+apply inbetween_step_not_Eq with (1 := Hx).
+omega.
+apply Rcompare_Lt.
+assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
+apply Rlt_le_trans with (1 := proj2 Hx').
+apply Rcompare_not_Lt_inv.
+rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
+apply Rcompare_not_Lt.
+change 2%R with (Z2R 2).
+rewrite <- Z2R_mult.
+apply Z2R_le.
+omega.
+exact Hstep.
+Qed.
+
+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.
+intros x k l Hx Hk1 Hk2.
+apply inbetween_step_not_Eq with (1 := Hx).
+omega.
+apply Rcompare_Gt.
+assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
+apply Rlt_le_trans with (2 := proj1 Hx').
+apply Rcompare_Lt_inv.
+rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
+apply Rcompare_Lt.
+change 2%R with (Z2R 2).
+rewrite <- Z2R_mult.
+apply Z2R_lt.
+omega.
+exact Hstep.
+Qed.
+
+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.
+intros x l Hx Hl.
+assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
+constructor.
+(* . *)
+split.
+apply Hx'.
+apply Rlt_trans with (1 := proj2 Hx').
+apply Rplus_lt_compat_l.
+rewrite <- (Rmult_1_l step) at 1.
+apply Rmult_lt_compat_r.
+exact Hstep.
+now apply (Z2R_lt 1).
+(* . *)
+apply Rcompare_Lt.
+apply Rlt_le_trans with (1 := proj2 Hx').
+rewrite middle_range.
+apply Rcompare_not_Lt_inv.
+rewrite <- (Rmult_1_l step) at 2.
+rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
+rewrite Rmult_1_r.
+apply Rcompare_not_Lt.
+apply (Z2R_le 2).
+now apply (Zlt_le_succ 1).
+exact Hstep.
+Qed.
+
+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.
+intros k Hk.
+rewrite <- Hk.
+rewrite 2!Z2R_plus, Z2R_mult.
+simpl. field.
+Qed.
+
+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.
+intros x k l Hx Hk.
+apply inbetween_step_not_Eq with (1 := Hx).
+omega.
+inversion_clear Hx as [|l' _ Hl].
+now rewrite (middle_odd _ Hk) in Hl.
+Qed.
+
+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.
+intros x k Hx Hk.
+apply inbetween_step_not_Eq with (1 := Hx).
+omega.
+inversion_clear Hx as [Hl|].
+rewrite Hl.
+rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
+apply Rcompare_Lt.
+change 2%R with (Z2R 2).
+rewrite <- Z2R_mult.
+apply Z2R_lt.
+rewrite <- Hk.
+apply Zlt_succ.
+exact Hstep.
+Qed.
+
+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.
+intros x k l Hx Hl Hk.
+apply inbetween_step_not_Eq with (1 := Hx).
+omega.
+apply Rcompare_Gt.
+assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
+apply Rle_lt_trans with (2 := proj1 Hx').
+apply Rcompare_not_Lt_inv.
+rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
+change 2%R with (Z2R 2).
+rewrite <- Z2R_mult.
+apply Rcompare_not_Lt.
+apply Z2R_le.
+rewrite Hk.
+apply Zle_refl.
+exact Hstep.
+Qed.
+
+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.
+intros x k Hx Hk.
+apply inbetween_step_not_Eq with (1 := Hx).
+omega.
+apply Rcompare_Eq.
+inversion_clear Hx as [Hx'|].
+rewrite Hx', <- Hk, Z2R_mult.
+simpl (Z2R 2).
+field.
+Qed.
+
+(** 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.
+intros He x k l Hk Hx.
+unfold new_location_even.
+destruct (Zeq_bool_spec k 0) as [Hk0|Hk0].
+(* k = 0 *)
+rewrite Hk0 in Hx.
+rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx.
+set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end).
+assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)).
+unfold l' ; case l ; try (now left) ; right ; now split.
+destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
+constructor.
+rewrite H1 in Hx.
+now inversion_clear Hx.
+now apply inbetween_step_Lo_not_Eq with (2 := H1).
+(* k <> 0 *)
+destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1].
+(* . 2 * k < nb_steps *)
+apply inbetween_step_Lo with (1 := Hx).
+omega.
+destruct (Zeven_ex nb_steps).
+rewrite He in H.
+omega.
+(* . 2 * k = nb_steps *)
+set (l' := match l with loc_Exact => Eq | _ => Gt end).
+assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)).
+unfold l' ; case l ; try (now left) ; right ; now split.
+destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
+rewrite H1 in Hx.
+now apply inbetween_step_Mi_Mi_even with (1 := Hx).
+now apply inbetween_step_Hi_Mi_even with (1 := Hx).
+(* . 2 * k > nb_steps *)
+apply inbetween_step_Hi with (1 := Hx).
+exact Hk1.
+apply Hk.
+Qed.
+
+(** 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.
+intros Ho x k l Hk Hx.
+unfold new_location_odd.
+destruct (Zeq_bool_spec k 0) as [Hk0|Hk0].
+(* k = 0 *)
+rewrite Hk0 in Hx.
+rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx.
+set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end).
+assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)).
+unfold l' ; case l ; try (now left) ; right ; now split.
+destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
+constructor.
+rewrite H1 in Hx.
+now inversion_clear Hx.
+now apply inbetween_step_Lo_not_Eq with (2 := H1).
+(* k <> 0 *)
+destruct (Zcompare_spec (2 * k + 1) nb_steps) as [Hk1|Hk1|Hk1].
+(* . 2 * k + 1 < nb_steps *)
+apply inbetween_step_Lo with (1 := Hx) (3 := Hk1).
+omega.
+(* . 2 * k + 1 = nb_steps *)
+destruct l.
+apply inbetween_step_Lo_Mi_Eq_odd with (1 := Hx) (2 := Hk1).
+apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1).
+(* . 2 * k + 1 > nb_steps *)
+apply inbetween_step_Hi with (1 := Hx).
+destruct (Zeven_ex nb_steps).
+rewrite Ho in H.
+omega.
+apply Hk.
+Qed.
+
+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.
+intros x k l Hk Hx.
+unfold new_location.
+generalize (refl_equal nb_steps) (Zle_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)).
+pattern nb_steps at 2 3 5 ; case nb_steps.
+now intros _.
+(* . *)
+intros [p|p|] Hp _.
+apply new_location_odd_correct with (2 := Hk) (3 := Hx).
+now rewrite Hp.
+apply new_location_even_correct with (2 := Hk) (3 := Hx).
+now rewrite Hp.
+now rewrite Hp in Hnb_steps.
+(* . *)
+now intros p _.
+Qed.
+
+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.
+intros x d u l s Hs [Hx|l' Hx Hl] ; constructor.
+now rewrite Hx.
+now split ; apply Rmult_lt_compat_r.
+rewrite inbetween_mult_aux.
+now rewrite Rcompare_mult_r.
+Qed.
+
+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.
+intros x d u l s Hs [Hx|l' Hx Hl] ; constructor.
+apply Rmult_eq_reg_r with (1 := Hx).
+now apply Rgt_not_eq.
+now split ; apply Rmult_lt_reg_r with s.
+rewrite <- Rcompare_mult_r with (1 := Hs).
+now rewrite inbetween_mult_aux in Hl.
+Qed.
+
+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.
+intros x m e l [Hx|l' Hx Hl].
+rewrite Hx.
+split.
+apply Rle_refl.
+apply F2R_lt_compat.
+apply Zlt_succ.
+split.
+now apply Rlt_le.
+apply Hx.
+Qed.
+
+(** 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.
+intros x m e l k Hk Hx.
+unfold inbetween_float in *.
+assert (Hr: forall m, F2R (Float beta m (e + k)) = F2R (Float beta (m * Zpower beta k) e)).
+clear -Hk. intros m.
+rewrite (F2R_change_exp beta e).
+apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))).
+ring.
+omega.
+assert (Hp: (Zpower beta k > 0)%Z).
+apply Zlt_gt.
+apply Zpower_gt_0.
+now apply Zlt_le_weak.
+(* . *)
+rewrite 2!Hr.
+rewrite Zmult_plus_distr_l, Zmult_1_l.
+unfold F2R at 2. simpl.
+rewrite Z2R_plus, Rmult_plus_distr_r.
+apply new_location_correct.
+apply bpow_gt_0.
+now apply Zpower_gt_1.
+now apply Z_mod_lt.
+rewrite <- 2!Rmult_plus_distr_r, <- 2!Z2R_plus.
+rewrite Zmult_comm, Zplus_assoc.
+now rewrite <- Z_div_mod_eq.
+Qed.
+
+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.
+intros x m e l Hx.
+replace (radix_val beta) with (Zpower beta 1).
+now apply inbetween_float_new_location.
+apply Zmult_1_r.
+Qed.
+
+Theorem inbetween_float_ex :
+  forall m e l,
+  exists x,
+  inbetween_float m e x l.
+Proof.
+intros m e l.
+apply inbetween_ex.
+apply F2R_lt_compat.
+apply Zlt_succ.
+Qed.
+
+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.
+intros x e m l m' l' H H'.
+refine ((fun Hm => conj Hm _) _).
+rewrite <- Hm in H'. clear -H H'.
+apply inbetween_unique with (1 := H) (2 := H').
+destruct (inbetween_float_bounds x m e l H) as (H1,H2).
+destruct (inbetween_float_bounds x m' e l' H') as (H3,H4).
+cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; omega.
+now split ; apply F2R_lt_reg with beta e ; apply Rle_lt_trans with x.
+Qed.
+
+End Fcalc_bracket_generic.