Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

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

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Floating-point format without underflow

Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FIX Ulp Round_NE.
Require Import Psatz.

Section RND_FLX.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable prec : Z.

Class Prec_gt_0 :=
  prec_gt_0 : (0 < prec)%Z.

Context { prec_gt_0_ : Prec_gt_0 }.

Inductive FLX_format (x : R) : Prop :=
  FLX_spec (f : float beta) :
    x = F2R f -> (Z.abs (Fnum f) < Zpower beta prec)%Z -> FLX_format x.

Definition FLX_exp (e : Z) := (e - prec)%Z.

Properties of the FLX format

Instance FLX_exp_valid : Valid_exp FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
Valid_exp FLX_exp
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
Valid_exp FLX_exp
intros k.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
k:Z
((FLX_exp k < k)%Z -> (FLX_exp (k + 1) <= k)%Z) /\
((k <= FLX_exp k)%Z ->
 (FLX_exp (FLX_exp k + 1) <= FLX_exp k)%Z /\
 (forall l : Z,
  (l <= FLX_exp k)%Z -> FLX_exp l = FLX_exp k))
unfold FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
k:Z
((k - prec < k)%Z -> (k + 1 - prec <= k)%Z) /\
((k <= k - prec)%Z ->
 (k - prec + 1 - prec <= k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z -> (l - prec)%Z = (k - prec)%Z))
generalize prec_gt_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
k:Z
(0 < prec)%Z ->
((k - prec < k)%Z -> (k + 1 - prec <= k)%Z) /\
((k <= k - prec)%Z ->
 (k - prec + 1 - prec <= k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z -> (l - prec)%Z = (k - prec)%Z))
repeat split ; intros ; omega.
Qed.

Theorem FIX_format_FLX :
  forall x e,
  (bpow (e - 1) <= Rabs x <= bpow e)%R ->
  FLX_format x ->
  FIX_format beta (e - prec) x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FLX_format x -> FIX_format beta (e - prec) x
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FLX_format x -> FIX_format beta (e - prec) x
clear prec_gt_0_.beta:radix
prec:Z
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FLX_format x -> FIX_format beta (e - prec) x
intros x e Hx [[xm xe] H1 H2].beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
FIX_format beta (e - prec) x
rewrite H1, (F2R_prec_normalize beta xm xe e prec).beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
FIX_format beta (e - prec)
  (F2R
     {|
     Fnum := xm * beta ^ (xe - e + prec);
     Fexp := e - prec |})
beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
(Z.abs xm < beta ^ prec)%Z
beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
(bpow (e - 1) <=
 Rabs (F2R {| Fnum := xm; Fexp := xe |}))%R
now eexists.beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
(Z.abs xm < beta ^ prec)%Z
beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
(bpow (e - 1) <=
 Rabs (F2R {| Fnum := xm; Fexp := xe |}))%R
exact H2.beta:radix
prec:Z
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
xm, xe:Z
H1:x = F2R {| Fnum := xm; Fexp := xe |}
H2:(Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
(bpow (e - 1) <=
 Rabs (F2R {| Fnum := xm; Fexp := xe |}))%R
now rewrite <- H1.
Qed.

Theorem FLX_format_generic :
  forall x, generic_format beta FLX_exp x -> FLX_format x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
generic_format beta FLX_exp x -> FLX_format x
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
generic_format beta FLX_exp x -> FLX_format x
intros x H.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
FLX_format x
rewrite H.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
FLX_format
  (F2R
     {|
     Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
     Fexp := cexp beta FLX_exp x |})
eexists ; repeat split.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Z.abs
   (Fnum
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
      Fexp := cexp beta FLX_exp x |}) < beta ^ prec)%Z
simpl.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
apply lt_IZR.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))) <
 IZR (beta ^ prec))%R
rewrite abs_IZR.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs (IZR (Ztrunc (scaled_mantissa beta FLX_exp x))) <
 IZR (beta ^ prec))%R
rewrite <- scaled_mantissa_generic with (1 := H).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs (scaled_mantissa beta FLX_exp x) <
 IZR (beta ^ prec))%R
rewrite <- scaled_mantissa_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(scaled_mantissa beta FLX_exp (Rabs x) <
 IZR (beta ^ prec))%R
apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp (Rabs x))).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(0 < bpow (cexp beta FLX_exp (Rabs x)))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(scaled_mantissa beta FLX_exp (Rabs x) *
 bpow (cexp beta FLX_exp (Rabs x)) <
 IZR (beta ^ prec) * bpow (cexp beta FLX_exp (Rabs x)))%R
apply bpow_gt_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(scaled_mantissa beta FLX_exp (Rabs x) *
 bpow (cexp beta FLX_exp (Rabs x)) <
 IZR (beta ^ prec) * bpow (cexp beta FLX_exp (Rabs x)))%R
rewrite scaled_mantissa_mult_bpow.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs x <
 IZR (beta ^ prec) * bpow (cexp beta FLX_exp (Rabs x)))%R
rewrite IZR_Zpower, <- bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs x < bpow (prec + cexp beta FLX_exp (Rabs x)))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(0 <= prec)%Z
2: now apply Zlt_le_weak.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs x < bpow (prec + cexp beta FLX_exp (Rabs x)))%R
unfold cexp, FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs x < bpow (prec + (mag beta (Rabs x) - prec)))%R
ring_simplify (prec + (mag beta (Rabs x) - prec))%Z.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs x < bpow (mag beta (Rabs x)))%R
rewrite mag_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
(Rabs x < bpow (mag beta x))%R
destruct (Req_dec x 0) as [Hx|Hx].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
Hx:x = 0%R
(Rabs x < bpow (mag beta x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
Hx:x <> 0%R
(Rabs x < bpow (mag beta x))%R
rewrite Hx, Rabs_R0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
Hx:x = 0%R
(0 < bpow (mag beta 0))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
Hx:x <> 0%R
(Rabs x < bpow (mag beta x))%R
apply bpow_gt_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
Hx:x <> 0%R
(Rabs x < bpow (mag beta x))%R
destruct (mag beta x) as (ex, Ex).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
Hx:x <> 0%R
ex:Z
Ex:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x < bpow (Build_mag_prop beta x ex Ex))%R
now apply Ex.
Qed.

Theorem generic_format_FLX :
  forall x, FLX_format x -> generic_format beta FLX_exp x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
FLX_format x -> generic_format beta FLX_exp x
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
FLX_format x -> generic_format beta FLX_exp x
clear prec_gt_0_.beta:radix
prec:Z
forall x : R,
FLX_format x -> generic_format beta FLX_exp x
intros x [[mx ex] H1 H2].beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs (Fnum {| Fnum := mx; Fexp := ex |}) <
 beta ^ prec)%Z
generic_format beta FLX_exp x
simpl in H2.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
generic_format beta FLX_exp x
rewrite H1.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
generic_format beta FLX_exp
  (F2R {| Fnum := mx; Fexp := ex |})
apply generic_format_F2R.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
mx <> 0%Z ->
(cexp beta FLX_exp (F2R {| Fnum := mx; Fexp := ex |}) <=
 ex)%Z
intros Zmx.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
Zmx:mx <> 0%Z
(cexp beta FLX_exp (F2R {| Fnum := mx; Fexp := ex |}) <=
 ex)%Z
unfold cexp, FLX_exp.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
Zmx:mx <> 0%Z
(mag beta (F2R {| Fnum := mx; Fexp := ex |}) - prec <=
 ex)%Z
rewrite mag_F2R with (1 := Zmx).beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
Zmx:mx <> 0%Z
(mag beta (IZR mx) + ex - prec <= ex)%Z
apply Zplus_le_reg_r with (prec - ex)%Z.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
Zmx:mx <> 0%Z
(mag beta (IZR mx) + ex - prec + (prec - ex) <=
 ex + (prec - ex))%Z
ring_simplify.beta:radix
prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
Zmx:mx <> 0%Z
(mag beta (IZR mx) <= prec)%Z
now apply mag_le_Zpower.
Qed.

Theorem FLX_format_satisfies_any :
  satisfies_any FLX_format.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
satisfies_any FLX_format
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
satisfies_any FLX_format
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
generic_format beta FLX_exp x <-> FLX_format x
intros x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
generic_format beta FLX_exp x <-> FLX_format x
split.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
generic_format beta FLX_exp x -> FLX_format x
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
FLX_format x -> generic_format beta FLX_exp x
apply FLX_format_generic.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
FLX_format x -> generic_format beta FLX_exp x
apply generic_format_FLX.
Qed.

Theorem FLX_format_FIX :
  forall x e,
  (bpow (e - 1) <= Rabs x <= bpow e)%R ->
  FIX_format beta (e - prec) x ->
  FLX_format x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FIX_format beta (e - prec) x -> FLX_format x
Proof with auto with typeclass_instances.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FIX_format beta (e - prec) x -> FLX_format x
intros x e Hx Fx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
Fx:FIX_format beta (e - prec) x
FLX_format x
apply FLX_format_generic.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
Fx:FIX_format beta (e - prec) x
generic_format beta FLX_exp x
apply generic_format_FIX in Fx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
Fx:generic_format beta (FIX_exp (e - prec)) x
generic_format beta FLX_exp x
revert Fx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
generic_format beta (FIX_exp (e - prec)) x ->
generic_format beta FLX_exp x
apply generic_inclusion with (e := e)...beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:(bpow (e - 1) <= Rabs x <= bpow e)%R
(FLX_exp e <= FIX_exp (e - prec) e)%Z
apply Z.le_refl.
Qed.

unbounded floating-point format with normal mantissas

Inductive FLXN_format (x : R) : Prop :=
  FLXN_spec (f : float beta) :
    x = F2R f ->
    (x <> 0%R -> Zpower beta (prec - 1) <= Z.abs (Fnum f) < Zpower beta prec)%Z ->
    FLXN_format x.

Theorem generic_format_FLXN :
  forall x, FLXN_format x -> generic_format beta FLX_exp x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
FLXN_format x -> generic_format beta FLX_exp x
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
FLXN_format x -> generic_format beta FLX_exp x
intros x [[xm ex] H1 H2].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
generic_format beta FLX_exp x
destruct (Req_dec x 0) as [Zx|Zx].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x = 0%R
generic_format beta FLX_exp x
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
generic_format beta FLX_exp x
rewrite Zx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x = 0%R
generic_format beta FLX_exp 0
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
generic_format beta FLX_exp x
apply generic_format_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
generic_format beta FLX_exp x
specialize (H2 Zx).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
generic_format beta FLX_exp x
apply generic_format_FLX.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
FLX_format x
rewrite H1.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
FLX_format (F2R {| Fnum := xm; Fexp := ex |})
eexists ; repeat split.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
xm, ex:Z
H1:x = F2R {| Fnum := xm; Fexp := ex |}
H2:(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
Zx:x <> 0%R
(Z.abs (Fnum {| Fnum := xm; Fexp := ex |}) <
 beta ^ prec)%Z
apply H2.
Qed.

Theorem FLXN_format_generic :
  forall x, generic_format beta FLX_exp x -> FLXN_format x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
generic_format beta FLX_exp x -> FLXN_format x
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
generic_format beta FLX_exp x -> FLXN_format x
intros x Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
FLXN_format x
rewrite Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
FLXN_format
  (F2R
     {|
     Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
     Fexp := cexp beta FLX_exp x |})
simpl.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
FLXN_format
  (F2R
     {|
     Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
     Fexp := cexp beta FLX_exp x |})
eexists.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
  Fexp := cexp beta FLX_exp x |} = F2R ?f
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
  Fexp := cexp beta FLX_exp x |} <> 0%R ->
(beta ^ (prec - 1) <= Z.abs (Fnum ?f) < beta ^ prec)%Z easy.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
  Fexp := cexp beta FLX_exp x |} <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs
   (Fnum
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
      Fexp := cexp beta FLX_exp x |}) < beta ^ prec)%Z
rewrite <- Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs
   (Fnum
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
      Fexp := cexp beta FLX_exp x |}) < beta ^ prec)%Z
intros Zx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(beta ^ (prec - 1) <=
 Z.abs
   (Fnum
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLX_exp x);
      Fexp := cexp beta FLX_exp x |}) < beta ^ prec)%Z
simpl.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(beta ^ (prec - 1) <=
 Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
split.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(beta ^ (prec - 1) <=
 Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)))%Z
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
(* *)
apply le_IZR.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(IZR (beta ^ (prec - 1)) <=
 IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite IZR_Zpower.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1) <=
 IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(0 <= prec - 1)%Z
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
2: now apply Zlt_0_le_0_pred.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1) <=
 IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite abs_IZR, <- scaled_mantissa_generic with (1 := Hx).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1) <=
 Rabs (scaled_mantissa beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
apply Rmult_le_reg_r with (bpow (cexp beta FLX_exp x)).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(0 < bpow (cexp beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1) * bpow (cexp beta FLX_exp x) <=
 Rabs (scaled_mantissa beta FLX_exp x) *
 bpow (cexp beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
apply bpow_gt_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1) * bpow (cexp beta FLX_exp x) <=
 Rabs (scaled_mantissa beta FLX_exp x) *
 bpow (cexp beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite <- bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1 + cexp beta FLX_exp x) <=
 Rabs (scaled_mantissa beta FLX_exp x) *
 bpow (cexp beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite <- scaled_mantissa_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1 + cexp beta FLX_exp x) <=
 scaled_mantissa beta FLX_exp (Rabs x) *
 bpow (cexp beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite <- cexp_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1 + cexp beta FLX_exp (Rabs x)) <=
 scaled_mantissa beta FLX_exp (Rabs x) *
 bpow (cexp beta FLX_exp (Rabs x)))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite scaled_mantissa_mult_bpow.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1 + cexp beta FLX_exp (Rabs x)) <=
 Rabs x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
unfold cexp, FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1 + (mag beta (Rabs x) - prec)) <=
 Rabs x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
rewrite mag_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (prec - 1 + (mag beta x - prec)) <= Rabs x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
ring_simplify (prec - 1 + (mag beta x - prec))%Z.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(bpow (mag beta x - 1) <= Rabs x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
destruct (mag beta x) as (ex,Ex).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
ex:Z
Ex:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(bpow (Build_mag_prop beta x ex Ex - 1) <= Rabs x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
now apply Ex.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x)) <
 beta ^ prec)%Z
(* *)
apply lt_IZR.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))) <
 IZR (beta ^ prec))%R
rewrite IZR_Zpower.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))) <
 bpow prec)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(0 <= prec)%Z
2: now apply Zlt_le_weak.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(IZR (Z.abs (Ztrunc (scaled_mantissa beta FLX_exp x))) <
 bpow prec)%R
rewrite abs_IZR, <- scaled_mantissa_generic with (1 := Hx).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs (scaled_mantissa beta FLX_exp x) < bpow prec)%R
apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp x)).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(0 < bpow (cexp beta FLX_exp x))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs (scaled_mantissa beta FLX_exp x) *
 bpow (cexp beta FLX_exp x) <
 bpow prec * bpow (cexp beta FLX_exp x))%R
apply bpow_gt_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs (scaled_mantissa beta FLX_exp x) *
 bpow (cexp beta FLX_exp x) <
 bpow prec * bpow (cexp beta FLX_exp x))%R
rewrite <- bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs (scaled_mantissa beta FLX_exp x) *
 bpow (cexp beta FLX_exp x) <
 bpow (prec + cexp beta FLX_exp x))%R
rewrite <- scaled_mantissa_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(scaled_mantissa beta FLX_exp (Rabs x) *
 bpow (cexp beta FLX_exp x) <
 bpow (prec + cexp beta FLX_exp x))%R
rewrite <- cexp_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(scaled_mantissa beta FLX_exp (Rabs x) *
 bpow (cexp beta FLX_exp (Rabs x)) <
 bpow (prec + cexp beta FLX_exp (Rabs x)))%R
rewrite scaled_mantissa_mult_bpow.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs x < bpow (prec + cexp beta FLX_exp (Rabs x)))%R
unfold cexp, FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs x < bpow (prec + (mag beta (Rabs x) - prec)))%R
rewrite mag_abs.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs x < bpow (prec + (mag beta x - prec)))%R
ring_simplify (prec + (mag beta x - prec))%Z.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
(Rabs x < bpow (mag beta x))%R
destruct (mag beta x) as (ex,Ex).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:generic_format beta FLX_exp x
Zx:x <> 0%R
ex:Z
Ex:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x < bpow (Build_mag_prop beta x ex Ex))%R
now apply Ex.
Qed.

Theorem FLXN_format_satisfies_any :
  satisfies_any FLXN_format.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
satisfies_any FLXN_format
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
satisfies_any FLXN_format
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
generic_format beta FLX_exp x <-> FLXN_format x
split ; intros H.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:generic_format beta FLX_exp x
FLXN_format x
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:FLXN_format x
generic_format beta FLX_exp x
now apply FLXN_format_generic.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
H:FLXN_format x
generic_format beta FLX_exp x
now apply generic_format_FLXN.
Qed.

Lemma negligible_exp_FLX :
   negligible_exp FLX_exp = None.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
negligible_exp FLX_exp = None
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
negligible_exp FLX_exp = None
case (negligible_exp_spec FLX_exp).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
(forall n : Z, (FLX_exp n < n)%Z) -> None = None
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall n : Z, (n <= FLX_exp n)%Z -> Some n = None
intros _; reflexivity.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall n : Z, (n <= FLX_exp n)%Z -> Some n = None
intros n H2; contradict H2.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
n:Z
~ (n <= FLX_exp n)%Z
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.

Theorem generic_format_FLX_1 :
  generic_format beta FLX_exp 1.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
generic_format beta FLX_exp 1
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
generic_format beta FLX_exp 1
unfold generic_format, scaled_mantissa, cexp, F2R; simpl.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R =
(IZR (Ztrunc (1 * bpow (- FLX_exp (mag beta 1)))) *
 bpow (FLX_exp (mag beta 1)))%R
rewrite Rmult_1_l, (mag_unique beta 1 1).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R =
(IZR (Ztrunc (bpow (- FLX_exp 1))) * bpow (FLX_exp 1))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
(bpow (1 - 1) <= Rabs 1 < bpow 1)%R
{beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R =
(IZR (Ztrunc (bpow (- FLX_exp 1))) * bpow (FLX_exp 1))%R unfold FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R =
(IZR (Ztrunc (bpow (- (1 - prec)))) * bpow (1 - prec))%R
  rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R =
(IZR (Ztrunc (IZR (beta ^ (- (1 - prec))))) *
 bpow (1 - prec))%R
  rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R = (bpow (- (1 - prec)) * bpow (1 - prec))%R
  rewrite <- bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
1%R = bpow (- (1 - prec) + (1 - prec))
  now replace (_ + _)%Z with Z0 by ring. }beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
(bpow (1 - 1) <= Rabs 1 < bpow 1)%R
rewrite Rabs_R1; simpl; split; [now right|].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
(1 < IZR (Z.pow_pos beta 1))%R
unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
(1 < beta)%Z
assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega.
Qed.

Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
ulp beta FLX_exp 0 = 0%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
ulp beta FLX_exp 0 = 0%R
unfold ulp; rewrite Req_bool_true; trivial.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
match negligible_exp FLX_exp with
| Some n => bpow (FLX_exp n)
| None => 0%R
end = 0%R
rewrite negligible_exp_FLX; easy.
Qed.

Lemma ulp_FLX_1 : ulp beta FLX_exp 1 = bpow (-prec + 1).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
ulp beta FLX_exp 1 = bpow (- prec + 1)
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
ulp beta FLX_exp 1 = bpow (- prec + 1)
unfold ulp, FLX_exp, cexp; rewrite Req_bool_false; [|apply R1_neq_R0].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
bpow (mag beta 1 - prec) = bpow (- prec + 1)
rewrite mag_1; f_equal; ring.
Qed.

Lemma succ_FLX_1 : (succ beta FLX_exp 1 = 1 + bpow (-prec + 1))%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
succ beta FLX_exp 1 = (1 + bpow (- prec + 1))%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
succ beta FLX_exp 1 = (1 + bpow (- prec + 1))%R
now unfold succ; rewrite Rle_bool_true; [|apply Rle_0_1]; rewrite ulp_FLX_1.
Qed.

Theorem eq_0_round_0_FLX :
   forall rnd {Vr: Valid_rnd rnd} x,
     round beta FLX_exp rnd x = 0%R -> x = 0%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall rnd : R -> Z,
Valid_rnd rnd ->
forall x : R,
round beta FLX_exp rnd x = 0%R -> x = 0%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall rnd : R -> Z,
Valid_rnd rnd ->
forall x : R,
round beta FLX_exp rnd x = 0%R -> x = 0%R
intros rnd Hr x.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
round beta FLX_exp rnd x = 0%R -> x = 0%R
apply eq_0_round_0_negligible_exp; try assumption.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Valid_exp FLX_exp
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
negligible_exp FLX_exp = None
apply FLX_exp_valid.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
negligible_exp FLX_exp = None
apply negligible_exp_FLX.
Qed.

Theorem gt_0_round_gt_0_FLX :
   forall rnd {Vr: Valid_rnd rnd} x,
     (0 < x)%R -> (0 < round beta FLX_exp rnd x)%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall rnd : R -> Z,
Valid_rnd rnd ->
forall x : R,
(0 < x)%R -> (0 < round beta FLX_exp rnd x)%R
Proof with auto with typeclass_instances.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall rnd : R -> Z,
Valid_rnd rnd ->
forall x : R,
(0 < x)%R -> (0 < round beta FLX_exp rnd x)%R
intros rnd Hr x Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
(0 < round beta FLX_exp rnd x)%R
assert (K: (0 <= round beta FLX_exp rnd x)%R).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
(0 <= round beta FLX_exp rnd x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
K:(0 <= round beta FLX_exp rnd x)%R
(0 < round beta FLX_exp rnd x)%R
rewrite <- (round_0 beta FLX_exp rnd).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
(round beta FLX_exp rnd 0 <= round beta FLX_exp rnd x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
K:(0 <= round beta FLX_exp rnd x)%R
(0 < round beta FLX_exp rnd x)%R
apply round_le...beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
(0 <= x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
K:(0 <= round beta FLX_exp rnd x)%R
(0 < round beta FLX_exp rnd x)%R now apply Rlt_le.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
K:(0 <= round beta FLX_exp rnd x)%R
(0 < round beta FLX_exp rnd x)%R
destruct K; try easy.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
H:0%R = round beta FLX_exp rnd x
(0 < round beta FLX_exp rnd x)%R
absurd (x = 0)%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
H:0%R = round beta FLX_exp rnd x
x <> 0%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
H:0%R = round beta FLX_exp rnd x
x = 0%R
now apply Rgt_not_eq.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
rnd:R -> Z
Hr:Valid_rnd rnd
x:R
Hx:(0 < x)%R
H:0%R = round beta FLX_exp rnd x
x = 0%R
apply eq_0_round_0_FLX with rnd...
Qed.


Theorem ulp_FLX_le :
  forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
(ulp beta FLX_exp x <= Rabs x * bpow (1 - prec))%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
(ulp beta FLX_exp x <= Rabs x * bpow (1 - prec))%R
intros x; case (Req_dec x 0); intros Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x = 0%R
(ulp beta FLX_exp x <= Rabs x * bpow (1 - prec))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(ulp beta FLX_exp x <= Rabs x * bpow (1 - prec))%R
rewrite Hx, ulp_FLX_0, Rabs_R0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x = 0%R
(0 <= 0 * bpow (1 - prec))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(ulp beta FLX_exp x <= Rabs x * bpow (1 - prec))%R
right; ring.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(ulp beta FLX_exp x <= Rabs x * bpow (1 - prec))%R
rewrite ulp_neq_0; try exact Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(bpow (cexp beta FLX_exp x) <=
 Rabs x * bpow (1 - prec))%R
unfold cexp, FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(bpow (mag beta x - prec) <= Rabs x * bpow (1 - prec))%R
replace (mag beta x - prec)%Z with ((mag beta x - 1) + (1-prec))%Z by ring.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(bpow (mag beta x - 1 + (1 - prec)) <=
 Rabs x * bpow (1 - prec))%R
rewrite bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(bpow (mag beta x - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
apply Rmult_le_compat_r.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(0 <= bpow (1 - prec))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(bpow (mag beta x - 1) <= Rabs x)%R
apply bpow_ge_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(bpow (mag beta x - 1) <= Rabs x)%R
now apply bpow_mag_le.
Qed.

Theorem ulp_FLX_ge :
  forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
(Rabs x * bpow (- prec) <= ulp beta FLX_exp x)%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall x : R,
(Rabs x * bpow (- prec) <= ulp beta FLX_exp x)%R
intros x; case (Req_dec x 0); intros Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x = 0%R
(Rabs x * bpow (- prec) <= ulp beta FLX_exp x)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <= ulp beta FLX_exp x)%R
rewrite Hx, ulp_FLX_0, Rabs_R0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x = 0%R
(0 * bpow (- prec) <= 0)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <= ulp beta FLX_exp x)%R
right; ring.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <= ulp beta FLX_exp x)%R
rewrite ulp_neq_0; try exact Hx.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <= bpow (cexp beta FLX_exp x))%R
unfold cexp, FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <= bpow (mag beta x - prec))%R
unfold Zminus; rewrite bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <=
 bpow (mag beta x) * bpow (- prec))%R
apply Rmult_le_compat_r.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(0 <= bpow (- prec))%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x <= bpow (mag beta x))%R
apply bpow_ge_0.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
Hx:x <> 0%R
(Rabs x <= bpow (mag beta x))%R
left; now apply bpow_mag_gt.
Qed.

Lemma ulp_FLX_exact_shift :
  forall x e,
  (ulp beta FLX_exp (x * bpow e) = ulp beta FLX_exp x * bpow e)%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R
intros x e.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R
destruct (Req_dec x 0) as [Hx|Hx].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x = 0%R
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x <> 0%R
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R
{beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x = 0%R
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R unfold ulp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x = 0%R
(if Req_bool (x * bpow e) 0
 then
  match negligible_exp FLX_exp with
  | Some n => bpow (FLX_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLX_exp (x * bpow e))) =
((if Req_bool x 0
  then
   match negligible_exp FLX_exp with
   | Some n => bpow (FLX_exp n)
   | None => 0
   end
  else bpow (cexp beta FLX_exp x)) * bpow e)%R
  now rewrite !Req_bool_true, negligible_exp_FLX; rewrite ?Hx, ?Rmult_0_l. }beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x <> 0%R
ulp beta FLX_exp (x * bpow e) =
(ulp beta FLX_exp x * bpow e)%R
unfold ulp; rewrite Req_bool_false;
  [|now intro H; apply Hx, (Rmult_eq_reg_r (bpow e));
    [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x <> 0%R
bpow (cexp beta FLX_exp (x * bpow e)) =
((if Req_bool x 0
  then
   match negligible_exp FLX_exp with
   | Some n => bpow (FLX_exp n)
   | None => 0
   end
  else bpow (cexp beta FLX_exp x)) * bpow e)%R
rewrite (Req_bool_false _ _ Hx), <- bpow_plus; f_equal; unfold cexp, FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Hx:x <> 0%R
(mag beta (x * bpow e) - prec)%Z =
(mag beta x - prec + e)%Z
now rewrite mag_mult_bpow; [ring|].
Qed.

Lemma succ_FLX_exact_shift :
  forall x e,
  (succ beta FLX_exp (x * bpow e) = succ beta FLX_exp x * bpow e)%R.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
forall (x : R) (e : Z),
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R
intros x e.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R
destruct (Rle_or_lt 0 x) as [Px|Nx].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Px:(0 <= x)%R
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R
{beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Px:(0 <= x)%R
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R rewrite succ_eq_pos; [|now apply Rmult_le_pos, bpow_ge_0].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Px:(0 <= x)%R
(x * bpow e + ulp beta FLX_exp (x * bpow e))%R =
(succ beta FLX_exp x * bpow e)%R
  rewrite (succ_eq_pos _ _ _ Px).beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Px:(0 <= x)%R
(x * bpow e + ulp beta FLX_exp (x * bpow e))%R =
((x + ulp beta FLX_exp x) * bpow e)%R
  now rewrite Rmult_plus_distr_r; f_equal; apply ulp_FLX_exact_shift. }beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
succ beta FLX_exp (x * bpow e) =
(succ beta FLX_exp x * bpow e)%R
unfold succ.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(if Rle_bool 0 (x * bpow e)
 then (x * bpow e + ulp beta FLX_exp (x * bpow e))%R
 else (- pred_pos beta FLX_exp (- (x * bpow e)))%R) =
((if Rle_bool 0 x
  then x + ulp beta FLX_exp x
  else - pred_pos beta FLX_exp (- x)) * bpow e)%R
rewrite Rle_bool_false; [|assert (H := bpow_gt_0 beta e); nra].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- pred_pos beta FLX_exp (- (x * bpow e)))%R =
((if Rle_bool 0 x
  then x + ulp beta FLX_exp x
  else - pred_pos beta FLX_exp (- x)) * bpow e)%R
rewrite Rle_bool_false; [|now simpl].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- pred_pos beta FLX_exp (- (x * bpow e)))%R =
(- pred_pos beta FLX_exp (- x) * bpow e)%R
rewrite Ropp_mult_distr_l_reverse, <-Ropp_mult_distr_l_reverse; f_equal.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
pred_pos beta FLX_exp (- x * bpow e) =
(pred_pos beta FLX_exp (- x) * bpow e)%R
unfold pred_pos.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(if
  Req_bool (- x * bpow e)
    (bpow (mag beta (- x * bpow e) - 1))
 then
  (- x * bpow e -
   bpow (FLX_exp (mag beta (- x * bpow e) - 1)))%R
 else
  (- x * bpow e - ulp beta FLX_exp (- x * bpow e))%R) =
((if Req_bool (- x) (bpow (mag beta (- x) - 1))
  then - x - bpow (FLX_exp (mag beta (- x) - 1))
  else - x - ulp beta FLX_exp (- x)) * bpow e)%R
rewrite mag_mult_bpow; [|lra].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(if
  Req_bool (- x * bpow e)
    (bpow (mag beta (- x) + e - 1))
 then
  (- x * bpow e -
   bpow (FLX_exp (mag beta (- x) + e - 1)))%R
 else
  (- x * bpow e - ulp beta FLX_exp (- x * bpow e))%R) =
((if Req_bool (- x) (bpow (mag beta (- x) - 1))
  then - x - bpow (FLX_exp (mag beta (- x) - 1))
  else - x - ulp beta FLX_exp (- x)) * bpow e)%R
replace (_ - 1)%Z with (mag beta (- x) - 1 + e)%Z; [|ring]; rewrite bpow_plus.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(if
  Req_bool (- x * bpow e)
    (bpow (mag beta (- x) - 1) * bpow e)
 then
  (- x * bpow e -
   bpow (FLX_exp (mag beta (- x) - 1 + e)))%R
 else
  (- x * bpow e - ulp beta FLX_exp (- x * bpow e))%R) =
((if Req_bool (- x) (bpow (mag beta (- x) - 1))
  then - x - bpow (FLX_exp (mag beta (- x) - 1))
  else - x - ulp beta FLX_exp (- x)) * bpow e)%R
unfold Req_bool; rewrite Rcompare_mult_r; [|now apply bpow_gt_0].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(if
  match
    Rcompare (- x) (bpow (mag beta (- x) - 1))
  with
  | Eq => true
  | _ => false
  end
 then
  (- x * bpow e -
   bpow (FLX_exp (mag beta (- x) - 1 + e)))%R
 else
  (- x * bpow e - ulp beta FLX_exp (- x * bpow e))%R) =
((if
   match
     Rcompare (- x) (bpow (mag beta (- x) - 1))
   with
   | Eq => true
   | _ => false
   end
  then - x - bpow (FLX_exp (mag beta (- x) - 1))
  else - x - ulp beta FLX_exp (- x)) * bpow e)%R
fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- x * bpow e -
 bpow (FLX_exp (mag beta (- x) - 1 + e)))%R =
((- x - bpow (FLX_exp (mag beta (- x) - 1))) * bpow e)%R
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- x * bpow e - ulp beta FLX_exp (- x * bpow e))%R =
((- x - ulp beta FLX_exp (- x)) * bpow e)%R
{beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- x * bpow e -
 bpow (FLX_exp (mag beta (- x) - 1 + e)))%R =
((- x - bpow (FLX_exp (mag beta (- x) - 1))) * bpow e)%R unfold FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- x * bpow e - bpow (mag beta (- x) - 1 + e - prec))%R =
((- x - bpow (mag beta (- x) - 1 - prec)) * bpow e)%R
  replace (_ - _)%Z with (mag beta (- x) - 1 - prec + e)%Z; [|ring].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- x * bpow e - bpow (mag beta (- x) - 1 - prec + e))%R =
((- x - bpow (mag beta (- x) - 1 - prec)) * bpow e)%R
  rewrite bpow_plus; ring. }beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
x:R
e:Z
Nx:(x < 0)%R
(- x * bpow e - ulp beta FLX_exp (- x * bpow e))%R =
((- x - ulp beta FLX_exp (- x)) * bpow e)%R
rewrite ulp_FLX_exact_shift; ring.
Qed.

FLX is a nice format: it has a monotone exponent...

Instance FLX_exp_monotone : Monotone_exp FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
Monotone_exp FLX_exp
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
Monotone_exp FLX_exp
intros ex ey Hxy.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
ex, ey:Z
Hxy:(ex <= ey)%Z
(FLX_exp ex <= FLX_exp ey)%Z
now apply Zplus_le_compat_r.
Qed.

and it allows a rounding to nearest, ties to even.

Hypothesis NE_prop : Z.even beta = false \/ (1 < prec)%Z.

Instance exists_NE_FLX : Exists_NE beta FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
Exists_NE beta FLX_exp
Proof.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
Exists_NE beta FLX_exp
destruct NE_prop as [H|H].beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
H:Z.even beta = false
Exists_NE beta FLX_exp
beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
H:(1 < prec)%Z
Exists_NE beta FLX_exp
now left.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
H:(1 < prec)%Z
Exists_NE beta FLX_exp
right.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
H:(1 < prec)%Z
forall e : Z,
((FLX_exp e < e)%Z -> (FLX_exp (e + 1) < e)%Z) /\
((e <= FLX_exp e)%Z ->
 FLX_exp (FLX_exp e + 1) = FLX_exp e)
unfold FLX_exp.beta:radix
prec:Z
prec_gt_0_:Prec_gt_0
NE_prop:Z.even beta = false \/ (1 < prec)%Z
H:(1 < prec)%Z
forall e : Z,
((e - prec < e)%Z -> (e + 1 - prec < e)%Z) /\
((e <= e - prec)%Z ->
 (e - prec + 1 - prec)%Z = (e - prec)%Z)
split ; omega.
Qed.

End RND_FLX.