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

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 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.
(* Goal: forall _ : and (Rle d x) (Rlt x u), inbetween inbetween_loc *)
intros Hx.
(* Goal: inbetween inbetween_loc *)
unfold inbetween_loc.
(* Goal: inbetween match Rcompare x d with | Eq => loc_Exact | Lt => loc_Exact | Gt => loc_Inexact (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) end *)
destruct (Rcompare_spec x d) as [H|H|H].
(* Goal: inbetween loc_Exact *)
(* Goal: inbetween loc_Exact *)
(* Goal: inbetween (loc_Inexact (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH)))))) *)
now elim Rle_not_lt with (1 := proj1 Hx).
(* Goal: inbetween loc_Exact *)
(* Goal: inbetween (loc_Inexact (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH)))))) *)
now constructor.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
constructor.
(* Goal: and (Rlt d x) (Rlt x u) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) *)
now split.
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) *)
easy.
Qed.

Theorem inbetween_unique :
  forall l l',
  inbetween l -> inbetween l' -> l = l'.
Proof.
(* Goal: forall (l l' : location) (_ : inbetween l) (_ : inbetween l'), @eq location l l' *)
intros l l' Hl Hl'.
(* Goal: @eq location l l' *)
inversion_clear Hl ; inversion_clear Hl'.
(* Goal: @eq location loc_Exact loc_Exact *)
(* Goal: @eq location loc_Exact (loc_Inexact l0) *)
(* Goal: @eq location (loc_Inexact l0) loc_Exact *)
(* Goal: @eq location (loc_Inexact l0) (loc_Inexact l1) *)
apply refl_equal.
(* Goal: @eq location loc_Exact (loc_Inexact l0) *)
(* Goal: @eq location (loc_Inexact l0) loc_Exact *)
(* Goal: @eq location (loc_Inexact l0) (loc_Inexact l1) *)
rewrite H in H0.
(* Goal: @eq location loc_Exact (loc_Inexact l0) *)
(* Goal: @eq location (loc_Inexact l0) loc_Exact *)
(* Goal: @eq location (loc_Inexact l0) (loc_Inexact l1) *)
elim Rlt_irrefl with (1 := proj1 H0).
(* Goal: @eq location (loc_Inexact l0) loc_Exact *)
(* Goal: @eq location (loc_Inexact l0) (loc_Inexact l1) *)
rewrite H1 in H.
(* Goal: @eq location (loc_Inexact l0) loc_Exact *)
(* Goal: @eq location (loc_Inexact l0) (loc_Inexact l1) *)
elim Rlt_irrefl with (1 := proj1 H).
(* Goal: @eq location (loc_Inexact l0) (loc_Inexact l1) *)
apply f_equal.
(* Goal: @eq comparison l0 l1 *)
now rewrite <- H0.
Qed.

Section Fcalc_bracket_any.

Variable l : location.

Theorem inbetween_bounds :
  inbetween l ->
  (d <= x < u)%R.
Proof.
(* Goal: forall _ : inbetween l, and (Rle d x) (Rlt x u) *)
intros [Hx|l' Hx Hl] ; clear l.
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
rewrite Hx.
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
split.
(* Goal: Rle (@F2R beta (Float beta m e)) (@F2R beta (Float beta m e)) *)
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.add m (Zpos xH)) e)) *)
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
apply Rle_refl.
(* Goal: Rlt d u *)
(* Goal: and (Rle d x) (Rlt x u) *)
exact Hdu.
(* Goal: and (Rle d x) (Rlt x u) *)
now split ; try apply Rlt_le.
Qed.

Theorem inbetween_bounds_not_Eq :
  inbetween l ->
  l <> loc_Exact ->
  (d < x < u)%R.
Proof.
(* Goal: forall (_ : inbetween l) (_ : not (@eq location l loc_Exact)), and (Rlt d x) (Rlt x u) *)
intros [Hx|l' Hx Hl] H.
(* Goal: and (Rlt d x) (Rlt x u) *)
(* Goal: and (Rlt d x) (Rlt x u) *)
now elim H.
(* Goal: and (Rlt d x) (Rlt x u) *)
exact Hx.
Qed.

End Fcalc_bracket_any.

Theorem inbetween_distance_inexact :
  forall l,
  inbetween (loc_Inexact l) ->
  Rcompare (x - d) (u - x) = l.
Proof.
(* Goal: forall (l : comparison) (_ : inbetween (loc_Inexact l)), @eq comparison (Rcompare (Rabs (Rminus d x)) (Rabs (Rminus u x))) l *)
intros l Hl.
(* Goal: @eq comparison (Rcompare (Rminus x d) (Rminus u x)) l *)
inversion_clear Hl as [|l' Hl' Hx].
(* Goal: @eq comparison (Rcompare (Rminus x d) (Rminus u x)) l *)
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.
(* Goal: forall (l : comparison) (_ : inbetween (loc_Inexact l)), @eq comparison (Rcompare (Rabs (Rminus d x)) (Rabs (Rminus u x))) l *)
intros l Hl.
(* Goal: @eq comparison (Rcompare (Rabs (Rminus d x)) (Rabs (Rminus u x))) l *)
rewrite Rabs_left1.
(* Goal: @eq comparison (Rcompare (Ropp (Rminus d x)) (Rabs (Rminus u x))) l *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
rewrite Rabs_pos_eq.
(* Goal: @eq comparison (Rcompare (Ropp (Rminus d x)) (Rminus u x)) l *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
rewrite Ropp_minus_distr.
(* Goal: @eq comparison (Rcompare (Rminus x d) (Rminus u x)) l *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
now apply inbetween_distance_inexact.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
apply Rle_0_minus.
(* Goal: Rle x u *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
apply Rlt_le.
(* Goal: Rle d x *)
apply (inbetween_bounds _ Hl).
(* Goal: Rle (Rminus d x) (IZR Z0) *)
apply Rle_minus.
(* Goal: Rle d x *)
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.
(* Goal: inbetween loc_Exact *)
(* Goal: inbetween (loc_Inexact (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH)))))) *)
now constructor.
exists (d + match l with Lt => 1 | Eq => 2 | Gt => 3 end / 4 * (u - d))%R.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
constructor.
(* *)
set (v := (match l with Lt => 1 | Eq => 2 | Gt => 3 end / 4)%R).
assert (0 < v < 1)%R.
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
split.
unfold v, Rdiv.
(* Goal: Rlt (IZR Z0) (Rmult (Z2R k) step) *)
(* Goal: Rlt x (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
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).
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
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_l 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.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) step) (Rmult (Z2R nb_steps) step) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rmult_lt_compat_r.
apply Rplus_lt_reg_r with v.
now ring_simplify.
(* Goal: Rlt d u *)
(* Goal: and (Rle d x) (Rlt x u) *)
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.
(* Goal: forall k : Z, @eq R (Rdiv (Rplus start (Rplus start (Rmult (Z2R k) step))) (IZR (Zpos (xO xH)))) (Rplus start (Rmult (Rdiv (Z2R k) (IZR (Zpos (xO xH)))) step)) *)
intros k.
(* Goal: Rlt (Rplus start step) (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) step) (Rmult (Z2R nb_steps) step) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) step *)
exact Hstep.
(* Goal: Rlt (Z2R (Z.mul (Zpos (xO xH)) k)) (Z2R nb_steps) *)
(* Goal: Rlt (IZR Z0) step *)
apply Z2R_lt.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
Qed.

Lemma middle_range :
  forall k,
  ((start + (start + Z2R k * step)) / 2 = start + (Z2R k / 2 * step))%R.
Proof.
(* Goal: forall k : Z, @eq R (Rdiv (Rplus start (Rplus start (Rmult (Z2R k) step))) (IZR (Zpos (xO xH)))) (Rplus start (Rmult (Rdiv (Z2R k) (IZR (Zpos (xO xH)))) step)) *)
intros k.
(* Goal: @eq R (Rdiv (Rplus (Rmult x s) (Rmult d s)) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) s) *)
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.
(* Goal: forall (x : R) (k : Z) (l : location) (l' : comparison) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l) (_ : and (Z.lt Z0 k) (Z.lt k nb_steps)) (_ : @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) l'), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact l') *)
intros x k l l' Hx Hk Hl'.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
constructor.
(* . *)
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
split.
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
apply Rlt_le_trans with (2 := proj1 Hx').
(* Goal: Rlt start (Rplus start (Rmult (Z2R k) step)) *)
(* Goal: Rlt x (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
rewrite <- (Rplus_0_r start) at 1.
(* Goal: Rlt (Rplus start step) (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (IZR Z0) (Rmult (Z2R k) step) *)
(* Goal: Rlt x (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (Z2R k) *)
(* Goal: Rlt (IZR Z0) step *)
(* Goal: Rlt x (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
now apply (Z2R_lt 0).
(* Goal: Rlt (IZR Z0) step *)
exact Hstep.
(* Goal: Rlt x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH)))) *)
apply Rlt_le_trans with (1 := proj2 Hx').
(* Goal: Rle (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
apply Rplus_le_compat_l.
(* Goal: Rle (Rmult (Z2R (Z.add k (Zpos xH))) step) (Rmult (Z2R nb_steps) step) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
apply Rmult_le_compat_r.
(* Goal: Rle x u *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
now apply Rlt_le.
(* Goal: Rle (Z2R nb_steps) (Z2R (Z.mul (Zpos (xO xH)) k)) *)
(* Goal: Rlt (IZR Z0) step *)
apply Z2R_le.
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* . *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) l' *)
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.
(* Goal: forall (x : R) (k : Z) (l : location) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l) (_ : Z.lt nb_steps (Z.mul (Zpos (xO xH)) k)) (_ : Z.lt k nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
intros x k l Hx Hk1 Hk2.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
apply inbetween_step_not_Eq with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: @eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_Lt.
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
(* Goal: Rlt x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH)))) *)
apply Rlt_le_trans with (1 := proj2 Hx').
(* Goal: Rle (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (Z2R k) step)) *)
apply Rcompare_not_Lt_inv.
(* Goal: not (@eq comparison (Rcompare (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (IZR (Zpos xH)) step))) Lt) *)
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
(* Goal: not (@eq comparison (Rcompare (Z2R (Z.mul (Zpos (xO xH)) k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_not_Lt.
(* Goal: not (@eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
change 2%R with (Z2R 2).
(* Goal: not (@eq comparison (Rcompare (Rmult (Z2R (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
rewrite <- Z2R_mult.
(* Goal: Rle (Z2R nb_steps) (Z2R (Z.mul (Zpos (xO xH)) k)) *)
(* Goal: Rlt (IZR Z0) step *)
apply Z2R_le.
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: Rlt (IZR Z0) step *)
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.
(* Goal: forall (x : R) (k : Z) (l : location) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l) (_ : Z.lt nb_steps (Z.mul (Zpos (xO xH)) k)) (_ : Z.lt k nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
intros x k l Hx Hk1 Hk2.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
apply inbetween_step_not_Eq with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Gt *)
apply Rcompare_Gt.
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
apply Rlt_le_trans with (2 := proj1 Hx').
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (Z2R k) step)) *)
apply Rcompare_Lt_inv.
(* Goal: not (@eq comparison (Rcompare (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (IZR (Zpos xH)) step))) Lt) *)
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
(* Goal: @eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_Lt.
(* Goal: not (@eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
change 2%R with (Z2R 2).
(* Goal: not (@eq comparison (Rcompare (Rmult (Z2R (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
rewrite <- Z2R_mult.
(* Goal: Rlt (Z2R (Z.mul (Zpos (xO xH)) k)) (Z2R nb_steps) *)
(* Goal: Rlt (IZR Z0) step *)
apply Z2R_lt.
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: Rlt (IZR Z0) step *)
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.
(* Goal: forall (x : R) (l : location) (_ : inbetween start (Rplus start step) x l) (_ : not (@eq location l loc_Exact)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
intros x l Hx Hl.
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
constructor.
(* . *)
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
split.
(* Goal: Rlt start x *)
(* Goal: Rlt x (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Hx'.
(* Goal: Rlt x (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rlt_trans with (1 := proj2 Hx').
(* Goal: Rlt (Rplus start step) (Rplus start (Rmult (Z2R nb_steps) step)) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rplus_lt_compat_l.
(* Goal: Rlt step (Rmult (Z2R nb_steps) step) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
rewrite <- (Rmult_1_l step) at 1.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) step) (Rmult (Z2R nb_steps) step) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) step *)
exact Hstep.
(* Goal: Rlt (IZR (Zpos xH)) (Z2R nb_steps) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
now apply (Z2R_lt 1).
(* . *)
(* Goal: @eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_Lt.
(* Goal: Rlt x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH)))) *)
apply Rlt_le_trans with (1 := proj2 Hx').
(* Goal: Rle (Rplus start step) (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH)))) *)
rewrite middle_range.
(* Goal: Rle (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (Z2R k) step)) *)
apply Rcompare_not_Lt_inv.
(* Goal: not (@eq comparison (Rcompare (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start step)) Lt) *)
rewrite <- (Rmult_1_l step) at 2.
(* Goal: not (@eq comparison (Rcompare (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (IZR (Zpos xH)) step))) Lt) *)
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
(* Goal: not (@eq comparison (Rcompare (Z2R nb_steps) (Rmult (IZR (Zpos (xO xH))) (IZR (Zpos xH)))) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
rewrite Rmult_1_r.
(* Goal: not (@eq comparison (Rcompare (Z2R (Z.mul (Zpos (xO xH)) k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_not_Lt.
(* Goal: Rle (IZR (Zpos (xO xH))) (Z2R nb_steps) *)
(* Goal: Rlt (IZR Z0) step *)
apply (Z2R_le 2).
(* Goal: Z.le (Zpos (xO xH)) nb_steps *)
(* Goal: Rlt (IZR Z0) step *)
now apply (Zlt_le_succ 1).
(* Goal: Rlt (IZR Z0) step *)
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.
(* Goal: forall (k : Z) (_ : @eq Z (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps), @eq R (Rdiv (Rplus (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step))) (IZR (Zpos (xO xH)))) (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) *)
intros k Hk.
(* Goal: Z.lt (Z.mul (Zpos (xO xH)) k) nb_steps *)
(* Goal: Rlt (IZR Z0) step *)
rewrite <- Hk.
(* Goal: @eq R (Rdiv (Rplus (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step))) (IZR (Zpos (xO xH)))) (Rplus start (Rmult (Rdiv (Z2R (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH))) (IZR (Zpos (xO xH)))) step)) *)
rewrite 2!Z2R_plus, Z2R_mult.
(* Goal: @eq R (Rdiv (Rplus (Rmult x s) (Rmult d s)) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) s) *)
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.
(* Goal: forall (x : R) (k : Z) (l : comparison) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x (loc_Inexact l)) (_ : @eq Z (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact l) *)
intros x k l Hx Hk.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
apply inbetween_step_not_Eq with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) l *)
inversion_clear Hx as [|l' _ Hl].
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) l *)
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.
(* Goal: forall (x : R) (k : Z) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x loc_Exact) (_ : @eq Z (Z.mul (Zpos (xO xH)) k) nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
intros x k Hx Hk.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
apply inbetween_step_not_Eq with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Lt *)
inversion_clear Hx as [Hl|].
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Lt *)
rewrite Hl.
(* Goal: not (@eq comparison (Rcompare (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Lt) *)
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
(* Goal: @eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_Lt.
(* Goal: not (@eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
change 2%R with (Z2R 2).
(* Goal: not (@eq comparison (Rcompare (Rmult (Z2R (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
rewrite <- Z2R_mult.
(* Goal: Rlt (Z2R (Z.mul (Zpos (xO xH)) k)) (Z2R nb_steps) *)
(* Goal: Rlt (IZR Z0) step *)
apply Z2R_lt.
(* Goal: Z.lt (Z.mul (Zpos (xO xH)) k) nb_steps *)
(* Goal: Rlt (IZR Z0) step *)
rewrite <- Hk.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
(* Goal: Rlt (IZR Z0) step *)
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.
(* Goal: forall (x : R) (k : Z) (l : location) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l) (_ : not (@eq location l loc_Exact)) (_ : @eq Z (Z.mul (Zpos (xO xH)) k) nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
intros x k l Hx Hl Hk.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
apply inbetween_step_not_Eq with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Gt *)
apply Rcompare_Gt.
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
(* Goal: Rlt (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) x *)
apply Rle_lt_trans with (2 := proj1 Hx').
(* Goal: Rle (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) (Rplus start (Rmult (Z2R k) step)) *)
apply Rcompare_not_Lt_inv.
(* Goal: not (@eq comparison (Rcompare (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Lt) *)
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
(* Goal: not (@eq comparison (Rcompare (Rmult (IZR (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
change 2%R with (Z2R 2).
(* Goal: not (@eq comparison (Rcompare (Rmult (Z2R (Zpos (xO xH))) (Z2R k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
rewrite <- Z2R_mult.
(* Goal: not (@eq comparison (Rcompare (Z2R (Z.mul (Zpos (xO xH)) k)) (Z2R nb_steps)) Lt) *)
(* Goal: Rlt (IZR Z0) step *)
apply Rcompare_not_Lt.
(* Goal: Rle (Z2R nb_steps) (Z2R (Z.mul (Zpos (xO xH)) k)) *)
(* Goal: Rlt (IZR Z0) step *)
apply Z2R_le.
(* Goal: Z.le nb_steps (Z.mul (Zpos (xO xH)) k) *)
(* Goal: Rlt (IZR Z0) step *)
rewrite Hk.
(* Goal: Z.le nb_steps nb_steps *)
(* Goal: Rlt (IZR Z0) step *)
apply Zle_refl.
(* Goal: Rlt (IZR Z0) step *)
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.
(* Goal: forall (x : R) (k : Z) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x loc_Exact) (_ : @eq Z (Z.mul (Zpos (xO xH)) k) nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
intros x k Hx Hk.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
apply inbetween_step_not_Eq with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: @eq comparison (Rcompare x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step))) Eq *)
apply Rcompare_Eq.
(* Goal: @eq R x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) *)
inversion_clear Hx as [Hx'|].
(* Goal: @eq R x (Rplus start (Rmult (Rdiv (Z2R nb_steps) (IZR (Zpos (xO xH)))) step)) *)
rewrite Hx', <- Hk, Z2R_mult.
(* Goal: @eq R (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Rdiv (Rmult (Z2R (Zpos (xO xH))) (Z2R k)) (IZR (Zpos (xO xH)))) step)) *)
simpl (Z2R 2).
(* Goal: @eq R (Rdiv (Rplus (Rmult x s) (Rmult d s)) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) s) *)
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.
(* Goal: forall (_ : @eq bool (Zeven nb_steps) true) (x : R) (k : Z) (l : location) (_ : and (Z.le Z0 k) (Z.lt k nb_steps)) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (new_location_even k l) *)
intros He x k l Hk Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (new_location_even k l) *)
unfold new_location_even.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (if Zeq_bool k Z0 then match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end else loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
destruct (Zeq_bool_spec k 0) as [Hk0|Hk0].
(* k = 0 *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite Hk0 in Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end).
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x l' *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)).
(* Goal: and (Rlt d x) (Rlt x u) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) *)
unfold l' ; case l ; try (now left) ; right ; now split.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x l' *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
constructor.
(* Goal: @eq R x start *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite H1 in Hx.
(* Goal: @eq R x start *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
now inversion_clear Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
now apply inbetween_step_Lo_not_Eq with (2 := H1).
(* k <> 0 *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.mul (Zpos (xO xH)) k) nb_steps with | Eq => match l with | loc_Exact => Eq | loc_Inexact c => Gt end | Lt => Lt | Gt => Gt end) *)
destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1].
(* . 2 * k < nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match l with | loc_Exact => Eq | loc_Inexact c => Gt end) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
apply inbetween_step_Lo with (1 := Hx).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: Z.lt nb_steps (Z.mul (Zpos (xO xH)) k) *)
(* Goal: Z.lt k nb_steps *)
destruct (Zeven_ex nb_steps).
(* Goal: Z.lt (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match l with | loc_Exact => Eq | loc_Inexact c => Gt end) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
rewrite He in H.
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* . 2 * k = nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match l with | loc_Exact => Eq | loc_Inexact c => Gt end) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
set (l' := match l with loc_Exact => Eq | _ => Gt end).
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact l') *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)).
(* Goal: and (Rlt d x) (Rlt x u) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) *)
unfold l' ; case l ; try (now left) ; right ; now split.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x l' *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
(* Goal: @eq R x start *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite H1 in Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Eq) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
now apply inbetween_step_Mi_Mi_even with (1 := Hx).
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
now apply inbetween_step_Hi_Mi_even with (1 := Hx).
(* . 2 * k > nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
apply inbetween_step_Hi with (1 := Hx).
(* Goal: Z.lt nb_steps (Z.mul (Zpos (xO xH)) k) *)
(* Goal: Z.lt k nb_steps *)
exact Hk1.
(* Goal: Z.lt k nb_steps *)
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.
(* Goal: forall (_ : @eq bool (Zeven nb_steps) false) (x : R) (k : Z) (l : location) (_ : and (Z.le Z0 k) (Z.lt k nb_steps)) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (new_location_odd k l) *)
intros Ho x k l Hk Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (new_location_odd k l) *)
unfold new_location_odd.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (if Zeq_bool k Z0 then match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end else loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
destruct (Zeq_bool_spec k 0) as [Hk0|Hk0].
(* k = 0 *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite Hk0 in Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x match l with | loc_Exact => l | loc_Inexact c => loc_Inexact Lt end *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end).
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x l' *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)).
(* Goal: and (Rlt d x) (Rlt x u) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) *)
unfold l' ; case l ; try (now left) ; right ; now split.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x l' *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
constructor.
(* Goal: @eq R x start *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
rewrite H1 in Hx.
(* Goal: @eq R x start *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
now inversion_clear Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
now apply inbetween_step_Lo_not_Eq with (2 := H1).
(* k <> 0 *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
destruct (Zcompare_spec (2 * k + 1) nb_steps) as [Hk1|Hk1|Hk1].
(* . 2 * k + 1 < nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match l with | loc_Exact => Lt | loc_Inexact l => l end) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
apply inbetween_step_Lo with (1 := Hx) (3 := Hk1).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* . 2 * k + 1 = nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match l with | loc_Exact => Lt | loc_Inexact l => l end) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
destruct l.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact c) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
apply inbetween_step_Lo_Mi_Eq_odd with (1 := Hx) (2 := Hk1).
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact c) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1).
(* . 2 * k + 1 > nb_steps *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Gt) *)
apply inbetween_step_Hi with (1 := Hx).
(* Goal: Z.lt nb_steps (Z.mul (Zpos (xO xH)) k) *)
(* Goal: Z.lt k nb_steps *)
destruct (Zeven_ex nb_steps).
(* Goal: Z.lt nb_steps (Z.mul (Zpos (xO xH)) k) *)
(* Goal: Z.lt k nb_steps *)
rewrite Ho in H.
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: Z.lt k nb_steps *)
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.
(* Goal: forall (x : R) (k : Z) (l : location) (_ : and (Z.le Z0 k) (Z.lt k nb_steps)) (_ : inbetween (Rplus start (Rmult (Z2R k) step)) (Rplus start (Rmult (Z2R (Z.add k (Zpos xH))) step)) x l), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (new_location k l) *)
intros x k l Hk Hx.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (new_location k l) *)
unfold new_location.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven nb_steps then new_location_even else new_location_odd) k l) *)
generalize (refl_equal nb_steps) (Zle_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)).
(* Goal: forall (_ : @eq Z nb_steps nb_steps) (_ : Z.lt Z0 nb_steps), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven nb_steps then new_location_even else new_location_odd) k l) *)
pattern nb_steps at 2 3 5 ; case nb_steps.
(* Goal: forall (_ : @eq Z nb_steps Z0) (_ : Z.lt Z0 Z0), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven Z0 then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zpos p)) (_ : Z.lt Z0 (Zpos p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos p) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
now intros _.
(* . *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zpos p)) (_ : Z.lt Z0 (Zpos p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos p) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
intros [p|p|] Hp _.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos (xI p)) then new_location_even else new_location_odd) k l) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos (xO p)) then new_location_even else new_location_odd) k l) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos xH) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
apply new_location_odd_correct with (2 := Hk) (3 := Hx).
(* Goal: @eq bool (Zeven nb_steps) true *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos xH) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
now rewrite Hp.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos (xO p)) then new_location_even else new_location_odd) k l) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos xH) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
apply new_location_even_correct with (2 := Hk) (3 := Hx).
(* Goal: @eq bool (Zeven nb_steps) true *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos xH) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
now rewrite Hp.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zpos xH) then new_location_even else new_location_odd) k l) *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
now rewrite Hp in Hnb_steps.
(* . *)
(* Goal: forall (p : positive) (_ : @eq Z nb_steps (Zneg p)) (_ : Z.lt Z0 (Zneg p)), inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x ((if Zeven (Zneg p) then new_location_even else new_location_odd) k l) *)
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.
(* Goal: forall x d s : R, @eq R (Rdiv (Rplus (Rmult x s) (Rmult d s)) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) s) *)
intros x d s.
(* Goal: @eq R (Rdiv (Rplus (Rmult x s) (Rmult d s)) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) 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.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
intros x d u l s Hs [Hx|l' Hx Hl] ; constructor.
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
now rewrite Hx.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) step) (Rmult (Z2R nb_steps) step) *)
(* Goal: @eq comparison (Rcompare x (Rdiv (Rplus start (Rplus start (Rmult (Z2R nb_steps) step))) (IZR (Zpos (xO xH))))) Lt *)
now split ; apply Rmult_lt_compat_r.
(* Goal: @eq comparison (Rcompare (Rmult u s) (Rdiv (Rplus (Rmult x s) (Rmult d s)) (IZR (Zpos (xO xH))))) l' *)
rewrite inbetween_mult_aux.
(* Goal: @eq comparison (Rcompare (Rmult u s) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) s)) l' *)
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.
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x loc_Exact *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact Lt) *)
(* Goal: inbetween start (Rplus start (Rmult (Z2R nb_steps) step)) x (loc_Inexact match Z.compare (Z.add (Z.mul (Zpos (xO xH)) k) (Zpos xH)) nb_steps with | Eq => match l with | loc_Exact => Lt | loc_Inexact l => l end | Lt => Lt | Gt => Gt end) *)
intros x d u l s Hs [Hx|l' Hx Hl] ; constructor.
(* Goal: @eq R u x *)
(* Goal: and (Rlt x u) (Rlt u d) *)
(* Goal: @eq comparison (Rcompare u (Rdiv (Rplus x d) (IZR (Zpos (xO xH))))) l' *)
apply Rmult_eq_reg_r with (1 := Hx).
now apply Rgt_not_eq.
(* Goal: and (Rlt x u) (Rlt u d) *)
(* Goal: @eq comparison (Rcompare u (Rdiv (Rplus x d) (IZR (Zpos (xO xH))))) l' *)
now split ; apply Rmult_lt_reg_r with s.
(* Goal: @eq comparison (Rcompare u (Rdiv (Rplus x d) (IZR (Zpos (xO xH))))) l' *)
rewrite <- Rcompare_mult_r with (1 := Hs).
(* Goal: @eq comparison (Rcompare (Rmult u s) (Rmult (Rdiv (Rplus x d) (IZR (Zpos (xO xH)))) s)) l' *)
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.
(* Goal: forall (x : R) (m e : Z) (l : location) (_ : inbetween_float m e x l), and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
intros x m e l [Hx|l' Hx Hl].
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
rewrite Hx.
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
split.
(* Goal: Rle (@F2R beta (Float beta m e)) (@F2R beta (Float beta m e)) *)
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.add m (Zpos xH)) e)) *)
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
apply Rle_refl.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.add m (Zpos xH)) e)) *)
apply F2R_lt_compat.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
(* Goal: and (Rle (@F2R beta (Float beta m e)) x) (Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e))) *)
split.
(* Goal: Rle x u *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
now apply Rlt_le.
(* Goal: Rlt x (@F2R beta (Float beta (Z.add m (Zpos xH)) e)) *)
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.
(* Goal: forall (x : R) (m e : Z) (l : location) (k : Z) (_ : Z.lt Z0 k) (_ : inbetween_float m e x l), inbetween_float (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
intros x m e l k Hk Hx.
(* Goal: inbetween_float (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
unfold inbetween_float in *.
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
assert (Hr: forall m, F2R (Float beta m (e + k)) = F2R (Float beta (m * Zpower beta k) e)).
(* Goal: forall m : Z, @eq R (@F2R beta (Float beta m (Z.add e k))) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) k)) e)) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
clear -Hk. intros m.
(* Goal: @eq R (@F2R beta (Float beta m (Z.add e k))) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) k)) e)) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
rewrite (F2R_change_exp beta e).
(* Goal: @eq R (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub (Z.add e k) e))) e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) k)) e)) *)
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))).
(* Goal: @eq Z (Z.sub (Z.add e k) e) k *)
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
ring.
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
omega.
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
assert (Hp: (Zpower beta k > 0)%Z).
(* Goal: Z.gt (Z.pow (radix_val beta) k) Z0 *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
apply Zlt_gt.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
apply Zpower_gt_0.
(* Goal: Z.le Z0 k *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
now apply Zlt_le_weak.
(* . *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
rewrite 2!Hr.
(* Goal: inbetween (@F2R beta (Float beta (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) e)) (@F2R beta (Float beta (Z.mul (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.pow (radix_val beta) k)) e)) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
rewrite Zmult_plus_distr_l, Zmult_1_l.
(* Goal: inbetween (@F2R beta (Float beta (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) e)) (Rmult (Z2R (@Fnum beta (Float beta (Z.add (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) e))) (Fcore_Raux.bpow beta (@Fexp beta (Float beta (Z.add (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) e)))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
unfold F2R at 2. simpl.
(* Goal: inbetween (@F2R beta (Float beta (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) e)) (Rmult (Z2R (Z.add (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
rewrite Z2R_plus, Rmult_plus_distr_r.
(* Goal: inbetween (@F2R beta (Float beta (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) e)) (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.pow (radix_val beta) k)) (Fcore_Raux.bpow beta e))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
apply new_location_correct.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Z.lt (Zpos xH) (Z.pow (radix_val beta) k) *)
(* Goal: and (Z.le Z0 (Z.modulo m (Z.pow (radix_val beta) k))) (Z.lt (Z.modulo m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) *)
(* Goal: inbetween (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.modulo m (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e))) (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add (Z.modulo m (Z.pow (radix_val beta) k)) (Zpos xH))) (Fcore_Raux.bpow beta e))) x l *)
apply bpow_gt_0.
(* Goal: Z.lt (Zpos xH) (Z.pow (radix_val beta) k) *)
(* Goal: and (Z.le Z0 (Z.modulo m (Z.pow (radix_val beta) k))) (Z.lt (Z.modulo m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) *)
(* Goal: inbetween (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.modulo m (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e))) (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add (Z.modulo m (Z.pow (radix_val beta) k)) (Zpos xH))) (Fcore_Raux.bpow beta e))) x l *)
now apply Zpower_gt_1.
(* Goal: and (Z.le Z0 (Z.modulo m (Z.pow (radix_val beta) k))) (Z.lt (Z.modulo m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) *)
(* Goal: inbetween (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.modulo m (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e))) (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add (Z.modulo m (Z.pow (radix_val beta) k)) (Zpos xH))) (Fcore_Raux.bpow beta e))) x l *)
now apply Z_mod_lt.
(* Goal: inbetween (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.modulo m (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e))) (Rplus (Rmult (Z2R (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add (Z.modulo m (Z.pow (radix_val beta) k)) (Zpos xH))) (Fcore_Raux.bpow beta e))) x l *)
rewrite <- 2!Rmult_plus_distr_r, <- 2!Z2R_plus.
(* Goal: inbetween (Rmult (Z2R (Z.add (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) (Z.modulo m (Z.pow (radix_val beta) k)))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add (Z.mul (Z.div m (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k)) (Z.add (Z.modulo m (Z.pow (radix_val beta) k)) (Zpos xH)))) (Fcore_Raux.bpow beta e)) x l *)
rewrite Zmult_comm, Zplus_assoc.
(* Goal: inbetween (Rmult (Z2R (Z.add (Z.mul (Z.pow (radix_val beta) k) (Z.div m (Z.pow (radix_val beta) k))) (Z.modulo m (Z.pow (radix_val beta) k)))) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add (Z.add (Z.mul (Z.pow (radix_val beta) k) (Z.div m (Z.pow (radix_val beta) k))) (Z.modulo m (Z.pow (radix_val beta) k))) (Zpos xH))) (Fcore_Raux.bpow beta e)) x l *)
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.
(* Goal: forall (x : R) (m e : Z) (l : location) (_ : inbetween_float m e x l), inbetween_float (Z.div m (radix_val beta)) (Z.add e (Zpos xH)) x (new_location (radix_val beta) (Z.modulo m (radix_val beta)) l) *)
intros x m e l Hx.
(* Goal: inbetween_float (Z.div m (radix_val beta)) (Z.add e (Zpos xH)) x (new_location (radix_val beta) (Z.modulo m (radix_val beta)) l) *)
replace (radix_val beta) with (Zpower beta 1).
(* Goal: inbetween_float (Z.div m (Z.pow (radix_val beta) (Zpos xH))) (Z.add e (Zpos xH)) x (new_location (Z.pow (radix_val beta) (Zpos xH)) (Z.modulo m (Z.pow (radix_val beta) (Zpos xH))) l) *)
(* Goal: @eq Z (Z.pow (radix_val beta) (Zpos xH)) (radix_val beta) *)
now apply inbetween_float_new_location.
(* Goal: @eq Z (Z.pow (radix_val beta) (Zpos xH)) (radix_val beta) *)
apply Zmult_1_r.
Qed.

Theorem inbetween_float_ex :
  forall m e l,
  exists x,
  inbetween_float m e x l.
Proof.
(* Goal: forall (m e : Z) (l : location), @ex R (fun x : R => inbetween_float m e x l) *)
intros m e l.
(* Goal: @ex R (fun x : R => inbetween_float m e x l) *)
apply inbetween_ex.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.add m (Zpos xH)) e)) *)
apply F2R_lt_compat.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
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.
(* Goal: forall (x : R) (e m : Z) (l : location) (m' : Z) (l' : location) (_ : inbetween_float m e x l) (_ : inbetween_float m' e x l'), and (@eq Z m m') (@eq location l l') *)
intros x e m l m' l' H H'.
(* Goal: and (@eq Z m m') (@eq location l l') *)
refine ((fun Hm => conj Hm _) _).
(* Goal: @eq location l l' *)
(* Goal: @eq Z m m' *)
rewrite <- Hm in H'. clear -H H'.
(* Goal: @eq location l l' *)
(* Goal: @eq Z m m' *)
apply inbetween_unique with (1 := H) (2 := H').
(* Goal: @eq Z m m' *)
destruct (inbetween_float_bounds x m e l H) as (H1,H2).
(* Goal: @eq Z m m' *)
destruct (inbetween_float_bounds x m' e l' H') as (H3,H4).
(* Goal: Z.le e (Z.add e k) *)
(* Goal: inbetween (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) (@F2R beta (Float beta (Z.add (Z.div m (Z.pow (radix_val beta) k)) (Zpos xH)) (Z.add e k))) x (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) *)
cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; omega.
(* Goal: and (Z.lt m (Z.add m' (Zpos xH))) (Z.lt m' (Z.add m (Zpos xH))) *)
now split ; apply F2R_lt_reg with beta e ; apply Rle_lt_trans with x.
Qed.

End Fcalc_bracket_generic.
