(**
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.
*)

(** * Floating-point format with gradual underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_FLX.
Require Import Fcore_FIX.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.

Section RND_FLT.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable emin prec : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.

(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z.

Definition FLT_exp e := Zmax (e - prec) emin.

(** Properties of the FLT format *)
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
Proof.
(* Goal: Valid_exp FLT_exp *)
intros k.
(* Goal: and (forall _ : Z.lt (FLT_exp e) e, Z.lt (FLT_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLT_exp e), @eq Z (FLT_exp (Z.add (FLT_exp e) (Zpos xH))) (FLT_exp e)) *)
unfold FLT_exp.
(* Goal: and (forall _ : Z.lt (Z.max (Z.sub k prec) emin) k, Z.le (Z.max (Z.sub (Z.add k (Zpos xH)) prec) emin) k) (forall _ : Z.le k (Z.max (Z.sub k prec) emin), and (Z.le (Z.max (Z.sub (Z.add (Z.max (Z.sub k prec) emin) (Zpos xH)) prec) emin) (Z.max (Z.sub k prec) emin)) (forall (l : Z) (_ : Z.le l (Z.max (Z.sub k prec) emin)), @eq Z (Z.max (Z.sub l prec) emin) (Z.max (Z.sub k prec) emin))) *)
generalize (prec_gt_0 prec).
repeat split ;
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
  intros ; zify ; omega.
Qed.

Theorem generic_format_FLT :
  forall x, FLT_format x -> generic_format beta FLT_exp x.
Proof.
(* Goal: forall (x : R) (_ : generic_format beta FLT_exp x), generic_format beta (FIX_exp emin) x *)
clear prec_gt_0_.
(* Goal: forall (x : R) (_ : FLT_format x), generic_format beta FLT_exp x *)
intros x ((mx, ex), (H1, (H2, H3))).
(* Goal: generic_format beta FLT_exp x *)
simpl in H2, H3.
(* Goal: generic_format beta FLT_exp x *)
rewrite H1.
(* Goal: generic_format beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x))) *)
apply generic_format_F2R.
(* Goal: forall _ : not (@eq Z mx Z0), Z.le (canonic_exp beta FLT_exp (@F2R beta (Float beta mx ex))) ex *)
intros Zmx.
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLT_exp x)) *)
unfold canonic_exp, FLT_exp.
(* Goal: Z.le (Z.max (Z.sub (ln_beta_val beta (@F2R beta (Float beta mx ex)) (ln_beta beta (@F2R beta (Float beta mx ex)))) prec) emin) ex *)
rewrite ln_beta_F2R with (1 := Zmx).
(* Goal: Z.le (Z.max (Z.sub (Z.add (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) ex) prec) emin) ex *)
apply Zmax_lub with (2 := H3).
(* Goal: Z.le (Z.sub (Z.add (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) ex) prec) ex *)
apply Zplus_le_reg_r with (prec - ex)%Z.
(* Goal: Z.le (Z.add (Z.sub (Z.add (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) ex) prec) (Z.sub prec ex)) (Z.add ex (Z.sub prec ex)) *)
ring_simplify.
(* Goal: Z.le (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) prec *)
now apply ln_beta_le_Zpower.
Qed.

Theorem FLT_format_generic :
  forall x, generic_format beta FLT_exp x -> FLT_format x.
Proof.
(* Goal: forall x : R, iff (generic_format beta FLT_exp x) (FLT_format x) *)
intros x.
unfold generic_format.
set (ex := canonic_exp beta FLT_exp x).
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
intros Hx.
(* Goal: generic_format beta (FIX_exp emin) x *)
rewrite Hx.
eexists ; repeat split ; simpl.
apply lt_Z2R.
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply bpow_gt_0.
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
rewrite <- bpow_plus.
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
rewrite F2R_Zabs.
(* Goal: Z.le (canonic_exp beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x)))) (canonic_exp beta FLT_exp x) *)
rewrite <- Hx.
(* Goal: generic_format beta FLT_exp x *)
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply bpow_gt_0.
unfold canonic_exp in ex.
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
(* Goal: Z.ge (Z.sub ex prec) emin *)
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (ln_beta_val beta x (ln_beta beta x)) (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply bpow_le.
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
(* Goal: Z.le (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin) *)
apply Zle_max_l.
(* Goal: Z.le (canonic_exp beta (FIX_exp emin) x) (canonic_exp beta FLT_exp x) *)
apply Zle_max_r.
Qed.


Theorem FLT_format_bpow :
  forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
Proof.
(* Goal: forall (e : Z) (_ : Z.le emin e), generic_format beta FLT_exp (Fcore_Raux.bpow beta e) *)
intros e He.
(* Goal: and (forall _ : Z.lt (FLT_exp e) e, Z.lt (FLT_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLT_exp e), @eq Z (FLT_exp (Z.add (FLT_exp e) (Zpos xH))) (FLT_exp e)) *)
apply generic_format_bpow; unfold FLT_exp.
(* Goal: Z.le (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e *)
apply Z.max_case; try assumption.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.




Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.
(* Goal: satisfies_any FLT_format *)
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).
(* Goal: forall x : R, iff (generic_format beta FLT_exp x) (FLT_format x) *)
intros x.
(* Goal: iff (generic_format beta FLT_exp x) (FLT_format x) *)
split.
(* Goal: forall _ : generic_format beta FLT_exp x, FLT_format x *)
(* Goal: forall _ : FLT_format x, generic_format beta FLT_exp x *)
apply FLT_format_generic.
(* Goal: forall _ : FLT_format x, generic_format beta FLT_exp x *)
apply generic_format_FLT.
Qed.

Theorem canonic_exp_FLT_FLX :
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
intros x Hx.
(* Goal: @eq Z (canonic_exp beta FLT_exp x) (canonic_exp beta (FLX_exp prec) x) *)
assert (Hx0: x <> 0%R).
(* Goal: not (@eq R x (IZR Z0)) *)
(* Goal: @eq Z (canonic_exp beta FLT_exp x) (canonic_exp beta (FLX_exp prec) x) *)
intros H1; rewrite H1, Rabs_R0 in Hx.
(* Goal: False *)
(* Goal: @eq Z (canonic_exp beta FLT_exp x) (canonic_exp beta (FLX_exp prec) x) *)
contradict Hx; apply Rlt_not_le, bpow_gt_0.
(* Goal: @eq Z (canonic_exp beta FLT_exp x) (canonic_exp beta (FIX_exp emin) x) *)
unfold canonic_exp.
(* Goal: @eq Z (FLT_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
apply Zmax_left.
(* Goal: Z.ge (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) emin *)
destruct (ln_beta beta x) as (ex, He).
(* Goal: Z.ge (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))) emin *)
unfold FLX_exp. simpl.
(* Goal: Z.ge (Z.sub ex prec) emin *)
specialize (He Hx0).
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
cut (emin + prec - 1 < ex)%Z. omega.
(* Goal: Z.lt (Z.sub ex (Zpos xH)) (Z.add emin prec) *)
apply (lt_bpow beta).
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Fcore_Raux.bpow beta e) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply Rle_lt_trans with (1 := Hx).
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
apply He.
Qed.

(** Links between FLT and FLX *)
Theorem generic_format_FLT_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  generic_format beta (FLX_exp prec) x ->
  generic_format beta FLT_exp x.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)) (_ : generic_format beta (FLX_exp prec) x), generic_format beta FLT_exp x *)
intros x Hx H.
(* Goal: generic_format beta FLT_exp x *)
destruct (Req_dec x 0) as [Hx0|Hx0].
(* Goal: generic_format beta FLT_exp x *)
(* Goal: generic_format beta FLT_exp x *)
rewrite Hx0.
(* Goal: generic_format beta FLT_exp (IZR Z0) *)
(* Goal: generic_format beta FLT_exp x *)
apply generic_format_0.
(* Goal: generic_format beta FLT_exp x *)
unfold generic_format, scaled_mantissa.
(* Goal: @eq R x (@F2R beta (Float beta (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta FLT_exp x))))) (canonic_exp beta FLT_exp x))) *)
now rewrite canonic_exp_FLT_FLX.
Qed.

Theorem generic_format_FLX_FLT :
  forall x : R,
  generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
Proof.
(* Goal: forall (x : R) (_ : generic_format beta FLT_exp x), generic_format beta (FIX_exp emin) x *)
clear prec_gt_0_.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
intros x Hx.
(* Goal: generic_format beta (FIX_exp emin) x *)
unfold generic_format in Hx; rewrite Hx.
(* Goal: generic_format beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x))) *)
apply generic_format_F2R.
(* Goal: forall _ : not (@eq Z (Ztrunc (scaled_mantissa beta FLT_exp x)) Z0), Z.le (canonic_exp beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x)))) (canonic_exp beta FLT_exp x) *)
intros _.
(* Goal: Z.le (canonic_exp beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x)))) (canonic_exp beta FLT_exp x) *)
rewrite <- Hx.
(* Goal: Z.le (canonic_exp beta (FLX_exp prec) x) (canonic_exp beta FLT_exp x) *)
unfold canonic_exp, FLX_exp, FLT_exp.
(* Goal: Z.le (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin) *)
apply Zle_max_l.
Qed.

Theorem round_FLT_FLX : forall rnd x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
(* Goal: forall (rnd : forall _ : R, Z) (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), @eq R (round beta FLT_exp rnd x) (round beta (FLX_exp prec) rnd x) *)
intros rnd x Hx.
(* Goal: @eq R (round beta FLT_exp rnd x) (round beta (FLX_exp prec) rnd x) *)
unfold round, scaled_mantissa.
(* Goal: @eq R (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta FLT_exp x))))) (canonic_exp beta FLT_exp x))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta (FLX_exp prec) x))))) (canonic_exp beta (FLX_exp prec) x))) *)
rewrite canonic_exp_FLT_FLX ; trivial.
Qed.

(** Links between FLT and FIX (underflow) *)
Theorem canonic_exp_FLT_FIX :
  forall x, x <> 0%R ->
  (Rabs x < bpow (emin + prec))%R ->
  canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))) (_ : Rlt (Rabs x) (Fcore_Raux.bpow beta (Z.add emin prec))), @eq Z (canonic_exp beta FLT_exp x) (canonic_exp beta (FIX_exp emin) x) *)
intros x Hx0 Hx.
(* Goal: @eq Z (canonic_exp beta FLT_exp x) (canonic_exp beta (FIX_exp emin) x) *)
unfold canonic_exp.
(* Goal: @eq Z (FLT_exp (ln_beta_val beta x (ln_beta beta x))) (FIX_exp emin (ln_beta_val beta x (ln_beta beta x))) *)
apply Zmax_right.
(* Goal: Z.le (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) (FIX_exp emin (ln_beta_val beta x (ln_beta beta x))) *)
unfold FIX_exp.
(* Goal: Z.le (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin *)
destruct (ln_beta beta x) as (ex, Hex).
(* Goal: Z.le (Z.sub (ln_beta_val beta x (Build_ln_beta_prop beta x ex Hex)) prec) emin *)
simpl.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
cut (ex - 1 < emin + prec)%Z. omega.
(* Goal: Z.lt (Z.sub ex (Zpos xH)) (Z.add emin prec) *)
apply (lt_bpow beta).
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) (Fcore_Raux.bpow beta (Z.add emin prec)) *)
apply Rle_lt_trans with (2 := Hx).
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) (Rabs x) *)
now apply Hex.
Qed.

Theorem generic_format_FIX_FLT :
  forall x : R,
  generic_format beta FLT_exp x ->
  generic_format beta (FIX_exp emin) x.
Proof.
(* Goal: forall (x : R) (_ : generic_format beta FLT_exp x), generic_format beta (FIX_exp emin) x *)
clear prec_gt_0_.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
intros x Hx.
(* Goal: generic_format beta (FIX_exp emin) x *)
rewrite Hx.
(* Goal: generic_format beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x))) *)
apply generic_format_F2R.
(* Goal: forall _ : not (@eq Z (Ztrunc (scaled_mantissa beta FLT_exp x)) Z0), Z.le (canonic_exp beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x)))) (canonic_exp beta FLT_exp x) *)
intros _.
(* Goal: Z.le (canonic_exp beta (FIX_exp emin) (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta FLT_exp x)) (canonic_exp beta FLT_exp x)))) (canonic_exp beta FLT_exp x) *)
rewrite <- Hx.
(* Goal: Z.le (canonic_exp beta (FIX_exp emin) x) (canonic_exp beta FLT_exp x) *)
apply Zle_max_r.
Qed.

Theorem generic_format_FLT_FIX :
  forall x : R,
  (Rabs x <= bpow (emin + prec))%R ->
  generic_format beta (FIX_exp emin) x ->
  generic_format beta FLT_exp x.
Proof with auto with typeclass_instances.
apply generic_inclusion_le...
(* Goal: forall (e : Z) (_ : Z.le emin e), generic_format beta FLT_exp (Fcore_Raux.bpow beta e) *)
intros e He.
(* Goal: Z.le (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) (FIX_exp emin (ln_beta_val beta x (ln_beta beta x))) *)
unfold FIX_exp.
apply Zmax_lub.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
omega.
apply Zle_refl.
Qed.

Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
    ulp beta FLT_exp x = bpow emin.
Proof with auto with typeclass_instances.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
intros x Hx.
unfold ulp; case Req_bool_spec; intros Hx2.
(* x = 0 *)
case (negligible_exp_spec FLT_exp).
intros T; specialize (T (emin-1)%Z); contradict T.
(* Goal: and (forall _ : Z.lt (FLT_exp e) e, Z.lt (FLT_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLT_exp e), @eq Z (FLT_exp (Z.add (FLT_exp e) (Zpos xH))) (FLT_exp e)) *)
apply Zle_not_lt; unfold FLT_exp.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
apply Zle_trans with (2:=Z.le_max_r _ _); omega.
assert (V:FLT_exp emin = emin).
unfold FLT_exp; apply Z.max_r.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
unfold Prec_gt_0 in prec_gt_0_; omega.
intros n H2; rewrite <-V.
apply f_equal, fexp_negligible_exp_eq...
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
omega.
(* x <> 0 *)
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLT_exp x)) *)
apply f_equal; unfold canonic_exp, FLT_exp.
apply Z.max_r.
assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega].
(* Goal: Z.le (Z.sub (ln_beta_val beta x (Build_ln_beta_prop beta x ex Hex)) prec) emin *)
destruct (ln_beta beta x) as (e,He); simpl.
(* Goal: Z.lt (Z.sub (Z.add emin prec) (Zpos xH)) e *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply lt_bpow with beta.
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) (Fcore_Raux.bpow beta (Z.add emin prec)) *)
apply Rle_lt_trans with (2:=Hx).
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
now apply He.
Qed.

Theorem ulp_FLT_le :
  forall x, (bpow (emin + prec - 1) <= Rabs x)%R ->
  (ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
intros x Hx.
(* Goal: Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
assert (Zx : (x <> 0)%R).
(* Goal: not (@eq R x (IZR Z0)) *)
(* Goal: Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
  intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
  rewrite Z, Rabs_R0; apply bpow_gt_0.
(* Goal: Rle (ulp beta FLT_exp x) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
rewrite ulp_neq_0 with (1 := Zx).
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLT_exp x)) *)
unfold canonic_exp, FLT_exp.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
destruct (ln_beta beta x) as (e,He).
(* Goal: Rle (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (Build_ln_beta_prop beta x e He)) prec) emin)) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
rewrite <- bpow_plus.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (Build_ln_beta_prop beta x e He)) prec) emin)) (Fcore_Raux.bpow beta (Z.add (Z.sub e (Zpos xH)) (Z.sub (Zpos xH) prec))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
right; apply f_equal.
(* Goal: @eq Z (Z.max (Z.sub (ln_beta_val beta x (Build_ln_beta_prop beta x e He)) prec) emin) (Z.add (Z.sub e (Zpos xH)) (Z.sub (Zpos xH) prec)) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring.
(* Goal: @eq Z (Z.max (Z.sub (ln_beta_val beta x (Build_ln_beta_prop beta x e He)) prec) emin) (Z.sub e prec) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply Z.max_l.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
assert (emin+prec-1 < e)%Z; try omega.
(* Goal: Z.lt (Z.sub (Z.add emin prec) (Zpos xH)) e *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply lt_bpow with beta.
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Fcore_Raux.bpow beta e) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply Rle_lt_trans with (1:=Hx).
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
now apply He.
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec)) *)
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Rabs x) *)
apply bpow_ge_0.
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
now apply He.
Qed.

Theorem ulp_FLT_gt :
  forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
rewrite Rabs_R0; apply bpow_gt_0.
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLT_exp x) *)
rewrite ulp_neq_0; try exact Hx.
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLT_exp x)) *)
unfold canonic_exp, FLT_exp.
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R.
(* Goal: Rlt (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply bpow_gt_0.
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
now apply bpow_ln_beta_gt.
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
rewrite <- bpow_plus.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (ln_beta_val beta x (ln_beta beta x)) (Z.opp prec))) (Fcore_Raux.bpow beta (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin)) *)
apply bpow_le.
(* Goal: Z.le (Z.add (ln_beta_val beta x (ln_beta beta x)) (Z.opp prec)) (Z.max (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) emin) *)
apply Z.le_max_l.
Qed.



(** FLT is a nice format: it has a monotone exponent... *)
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
Proof.
(* Goal: Monotone_exp FLT_exp *)
intros ex ey.
(* Goal: and (forall _ : Z.lt (FLT_exp e) e, Z.lt (FLT_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLT_exp e), @eq Z (FLT_exp (Z.add (FLT_exp e) (Zpos xH))) (FLT_exp e)) *)
unfold FLT_exp.
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
zify ; omega.
Qed.

(** and it allows a rounding to nearest, ties to even. *)
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.

Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
Proof.
(* Goal: Exists_NE beta FLT_exp *)
destruct NE_prop as [H|H].
(* Goal: Exists_NE beta FLT_exp *)
(* Goal: Exists_NE beta FLT_exp *)
now left.
(* Goal: Exists_NE beta FLT_exp *)
right.
(* Goal: forall e : Z, and (forall _ : Z.lt (FLT_exp e) e, Z.lt (FLT_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLT_exp e), @eq Z (FLT_exp (Z.add (FLT_exp e) (Zpos xH))) (FLT_exp e)) *)
intros e.
(* Goal: and (forall _ : Z.lt (FLT_exp e) e, Z.lt (FLT_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLT_exp e), @eq Z (FLT_exp (Z.add (FLT_exp e) (Zpos xH))) (FLT_exp e)) *)
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
(* Goal: and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
generalize (Zmax_spec (e + 1 - prec) emin).
(* Goal: forall _ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin)), and (forall _ : Z.lt (Z.sub e prec) e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e (Z.sub e prec), @eq Z (Z.max (Z.sub (Z.add (Z.sub e prec) (Zpos xH)) prec) emin) (Z.sub e prec)) *)
(* Goal: and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
generalize (Zmax_spec (e - prec + 1 - prec) emin).
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
omega.
(* Goal: and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
generalize (Zmax_spec (e + 1 - prec) emin).
(* Goal: forall _ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin)), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
generalize (Zmax_spec (emin + 1 - prec) emin).
(* Goal: forall (_ : or (and (Z.ge (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) (Z.sub (Z.add emin (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add emin (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin))) (_ : or (and (Z.ge (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) (Z.sub (Z.add e (Zpos xH)) prec))) (and (Z.lt (Z.sub (Z.add e (Zpos xH)) prec) emin) (@eq Z (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) emin))), and (forall _ : Z.lt emin e, Z.lt (Z.max (Z.sub (Z.add e (Zpos xH)) prec) emin) e) (forall _ : Z.le e emin, @eq Z (Z.max (Z.sub (Z.add emin (Zpos xH)) prec) emin) emin) *)
omega.
Qed.

End RND_FLT.
