(**
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 abrupt 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_ulp.
Require Import Fcore_FLX.

Section RND_FTZ.

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 abrupt underflow *)
Definition FTZ_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\
  (emin <= Fexp f)%Z.

Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z.

(** Properties of the FTZ format *)
Global Instance FTZ_exp_valid : Valid_exp FTZ_exp.
Proof.
(* Goal: Valid_exp FTZ_exp *)
intros k.
(* Goal: Z.le (FTZ_exp e) (FLX_exp prec e) *)
unfold FTZ_exp.
(* Goal: and (forall _ : Z.lt (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec) (Zpos xH)) prec) (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec)) (forall (l : Z) (_ : Z.le l (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec))) *)
generalize (Zlt_cases (k - prec) emin).
(* Goal: forall _ : if Z.ltb (Z.sub k prec) emin then Z.lt (Z.sub k prec) emin else Z.ge (Z.sub k prec) emin, and (forall _ : Z.lt (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec) (Zpos xH)) prec) (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec)) (forall (l : Z) (_ : Z.le l (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (if Z.ltb (Z.sub k prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub k prec))) *)
case (Zlt_bool (k - prec) emin) ; intros H1.
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
split ; intros H2.
(* Goal: Z.le emin (Z.sub e prec) *)
omega.
(* Goal: iff (generic_format beta FTZ_exp x) (FTZ_format x) *)
split.
(* Goal: Z.le (if Z.ltb (Z.sub (Z.add (Z.sub (Z.add emin prec) (Zpos xH)) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub (Z.add emin prec) (Zpos xH)) (Zpos xH)) prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: forall (l : Z) (_ : Z.le l (Z.sub (Z.add emin prec) (Zpos xH))), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
generalize (Zlt_cases (emin + prec + 1 - prec) emin).
(* Goal: forall _ : if Z.ltb (Z.sub (Z.add (Z.add emin prec) (Zpos xH)) prec) emin then Z.lt (Z.sub (Z.add (Z.add emin prec) (Zpos xH)) prec) emin else Z.ge (Z.sub (Z.add (Z.add emin prec) (Zpos xH)) prec) emin, Z.le (if Z.ltb (Z.sub (Z.add (Z.sub (Z.add emin prec) (Zpos xH)) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub (Z.add emin prec) (Zpos xH)) (Zpos xH)) prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: forall (l : Z) (_ : Z.le l (Z.sub (Z.add emin prec) (Zpos xH))), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3.
(* Goal: Z.le emin (Z.sub e prec) *)
omega.
(* Goal: Z.le (if Z.ltb (Z.sub (Z.add (Z.sub (Z.add emin prec) (Zpos xH)) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub (Z.add emin prec) (Zpos xH)) (Zpos xH)) prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: forall (l : Z) (_ : Z.le l (Z.sub (Z.add emin prec) (Zpos xH))), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin).
(* Goal: Z.le (Z.sub ex prec) (Z.sub ex (Zpos xH)) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
generalize (prec_gt_0 prec).
(* Goal: Z.le emin (Z.sub e prec) *)
case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega.
(* Goal: forall (l : Z) (_ : Z.le l (Z.sub (Z.add emin prec) (Zpos xH))), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
intros l H3.
(* Goal: @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub (Z.add emin prec) (Zpos xH)) *)
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
generalize (Zlt_cases (l - prec) emin).
(* Goal: Z.le emin (Z.sub e prec) *)
case (Zlt_bool (l - prec) emin) ; omega.
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec))) *)
split ; intros H2.
(* Goal: Z.le (if Z.ltb (Z.sub (Z.add k (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add k (Zpos xH)) prec) k *)
(* Goal: and (Z.le (if Z.ltb (Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub (Z.add (Z.sub k prec) (Zpos xH)) prec) (Z.sub k prec)) (forall (l : Z) (_ : Z.le l (Z.sub k prec)), @eq Z (if Z.ltb (Z.sub l prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub l prec) (Z.sub k prec)) *)
generalize (Zlt_cases (k + 1 - prec) emin).
(* Goal: Z.le emin (Z.sub e prec) *)
case (Zlt_bool (k + 1 - prec) emin) ; omega.
(* Goal: Z.le (Z.sub ex prec) (Z.sub ex (Zpos xH)) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
generalize (prec_gt_0 prec).
(* Goal: Z.le emin (Z.sub e prec) *)
split ; intros ; omega.
Qed.

Theorem FLXN_format_FTZ :
  forall x, FTZ_format x -> FLXN_format beta prec x.
Proof.
intros x ((xm, xe), (Hx1, (Hx2, Hx3))).
eexists.
apply (conj Hx1 Hx2).
Qed.

Theorem generic_format_FTZ :
  forall x, FTZ_format x -> generic_format beta FTZ_exp x.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), @eq R (round beta FTZ_exp Zrnd_FTZ x) (round beta (FLX_exp prec) rnd x) *)
intros x Hx.
(* Goal: generic_format beta FTZ_exp x *)
cut (generic_format beta (FLX_exp prec) x).
(* Goal: forall _ : generic_format beta (FLX_exp prec) x, generic_format beta FTZ_exp x *)
(* Goal: generic_format beta (FLX_exp prec) x *)
apply generic_inclusion_ln_beta.
(* Goal: forall _ : not (@eq R x R0), Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
intros Zx.
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
destruct Hx as ((xm, xe), (Hx1, (Hx2, Hx3))).
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
simpl in Hx2, Hx3.
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
specialize (Hx2 Zx).
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
assert (Zxm: xm <> Z0).
(* Goal: not (@eq Z xm Z0) *)
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
contradict Zx.
(* Goal: @eq R x R0 *)
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
rewrite Hx1, Zx.
(* Goal: @eq R (@F2R beta (Float beta Z0 xe)) R0 *)
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
apply F2R_0.
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
unfold FTZ_exp, FLX_exp.
(* Goal: @eq Z (Z.sub ex prec) (if Z.ltb (Z.sub ex prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub ex prec) *)
rewrite Zlt_bool_false.
(* Goal: Z.le (Z.sub e prec) (FLX_exp prec e) *)
(* Goal: Z.le emin (Z.sub e prec) *)
apply Zle_refl.
(* Goal: Z.le emin (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
rewrite Hx1, ln_beta_F2R with (1 := Zxm).
(* Goal: Z.le emin (Z.sub (Z.add (ln_beta_val beta (Z2R xm) (ln_beta beta (Z2R xm))) xe) prec) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
cut (prec - 1 < ln_beta beta (Z2R xm))%Z.
(* Goal: Z.le emin (Z.sub e prec) *)
clear -Hx3 ; omega.
(* Goal: Z.lt (Z.sub prec (Zpos xH)) (ln_beta_val beta (Z2R xm) (ln_beta beta (Z2R xm))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
apply ln_beta_gt_Zpower with (1 := Zxm).
(* Goal: Z.le (Z.pow (radix_val beta) (Z.sub prec (Zpos xH))) (Z.abs xm) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
apply Hx2.
(* Goal: generic_format beta (FLX_exp prec) x *)
apply generic_format_FLXN.
(* Goal: FLXN_format beta prec x *)
now apply FLXN_format_FTZ.
Qed.

Theorem FTZ_format_generic :
  forall x, generic_format beta FTZ_exp x -> FTZ_format x.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), @eq R (round beta FTZ_exp Zrnd_FTZ x) (round beta (FLX_exp prec) rnd x) *)
intros x Hx.
(* Goal: FTZ_format x *)
destruct (Req_dec x 0) as [Hx3|Hx3].
(* Goal: FTZ_format x *)
(* Goal: FTZ_format x *)
exists (Float beta 0 emin).
(* Goal: iff (generic_format beta FTZ_exp x) (FTZ_format x) *)
split.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta ex)) (@F2R beta (Float beta (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH))))))) (Z.sub (Z.add emin prec) (Zpos xH)))) *)
(* Goal: FTZ_format x *)
unfold F2R. simpl.
(* Goal: @eq R x (Rmult (IZR Z0) (Fcore_Raux.bpow beta emin)) *)
(* Goal: and (forall _ : not (@eq R x R0), and (Z.le (Z.pow (radix_val beta) (Z.sub prec (Zpos xH))) (Z.abs (@Fnum beta (Float beta Z0 emin)))) (Z.lt (Z.abs (@Fnum beta (Float beta Z0 emin))) (Z.pow (radix_val beta) prec))) (Z.le emin (@Fexp beta (Float beta Z0 emin))) *)
(* Goal: FTZ_format x *)
now rewrite Rmult_0_l.
(* Goal: iff (generic_format beta FTZ_exp x) (FTZ_format x) *)
split.
(* Goal: forall _ : not (@eq R x R0), and (Z.le (Z.pow (radix_val beta) (Z.sub prec (Zpos xH))) (Z.abs (@Fnum beta (Float beta Z0 emin)))) (Z.lt (Z.abs (@Fnum beta (Float beta Z0 emin))) (Z.pow (radix_val beta) prec)) *)
(* Goal: Z.le emin (@Fexp beta (Float beta Z0 emin)) *)
(* Goal: FTZ_format x *)
intros H.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub prec (Zpos xH))) (Z.abs (@Fnum beta (Float beta Z0 emin)))) (Z.lt (Z.abs (@Fnum beta (Float beta Z0 emin))) (Z.pow (radix_val beta) prec)) *)
(* Goal: Z.le emin (@Fexp beta (Float beta Z0 emin)) *)
(* Goal: FTZ_format x *)
now elim H.
(* Goal: Z.le (Z.sub e prec) (FLX_exp prec e) *)
(* Goal: Z.le emin (Z.sub e prec) *)
apply Zle_refl.
(* Goal: FTZ_format x *)
unfold generic_format, scaled_mantissa, canonic_exp, FTZ_exp in Hx.
(* Goal: FTZ_format x *)
destruct (ln_beta beta x) as (ex, Hx4).
(* Goal: FTZ_format x *)
simpl in Hx.
(* Goal: FTZ_format x *)
specialize (Hx4 Hx3).
(* Goal: FTZ_format x *)
generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx.
(* Goal: forall (_ : if Z.ltb (Z.sub ex prec) emin then Z.lt (Z.sub ex prec) emin else Z.ge (Z.sub ex prec) emin) (_ : @eq R x (@F2R beta (Float beta (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (if Z.ltb (Z.sub ex prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub ex prec))))) (if Z.ltb (Z.sub ex prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub ex prec)))), FTZ_format x *)
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
(* Goal: FTZ_format x *)
(* Goal: FTZ_format x *)
elim Rlt_not_ge with (1 := proj2 Hx4).
(* Goal: Rge (Rabs x) (Fcore_Raux.bpow beta ex) *)
(* Goal: FTZ_format x *)
apply Rle_ge.
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Rabs x) *)
(* Goal: FTZ_format x *)
rewrite Hx2, <- F2R_Zabs.
(* Goal: Rle (Fcore_Raux.bpow beta ex) (@F2R beta (Float beta (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH))))))) (Z.sub (Z.add emin prec) (Zpos xH)))) *)
(* Goal: FTZ_format x *)
rewrite <- (Rmult_1_l (bpow ex)).
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta ex)) (@F2R beta (Float beta (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH))))))) (Z.sub (Z.add emin prec) (Zpos xH)))) *)
(* Goal: FTZ_format x *)
unfold F2R. simpl.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta ex)) (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH)))))))) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH)))) *)
(* Goal: FTZ_format x *)
apply Rmult_le_compat.
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta ex) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH)))))))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
now apply (Z2R_le 0 1).
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_ge_0.
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH)))))))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
apply (Z2R_le 1).
(* Goal: Z.le (Zpos xH) (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH))))))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
apply (Zlt_le_succ 0).
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply lt_Z2R.
(* Goal: Rlt (Z2R Z0) (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH)))))))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply bpow_gt_0.
(* Goal: Rlt (Rmult (Z2R Z0) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH)))) (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH)))))))) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH)))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
rewrite Rmult_0_l.
(* Goal: Rlt (IZR Z0) (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH)))))))) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH)))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
(* Goal: Rlt (@F2R beta (Float beta (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.sub ex prec))) (Fcore_Raux.bpow beta ex) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite F2R_Zabs, <- Hx2.
(* Goal: Rlt (IZR Z0) (Rabs x) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
now apply Rabs_pos_lt.
(* Goal: Rle (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_le.
(* Goal: Z.le emin (Z.sub e prec) *)
omega.
(* Goal: FTZ_format x *)
rewrite Hx2.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))))) (FTZ_exp (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))))) (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))) *)
eexists ; repeat split ; simpl.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.sub prec (Zpos xH))) (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) *)
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply le_Z2R.
(* Goal: Rlt (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Z2R (Z.pow (radix_val beta) prec)) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite Z2R_Zpower.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub prec (Zpos xH))) (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) *)
(* Goal: Z.le Z0 (Z.sub prec (Zpos xH)) *)
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply Rmult_le_reg_r with (bpow (ex - prec)).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply bpow_gt_0.
(* Goal: Rlt (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta (Z.sub ex prec))) (Rmult (Fcore_Raux.bpow beta prec) (Fcore_Raux.bpow beta (Z.sub ex prec))) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite <- bpow_plus.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (Z.sub prec (Zpos xH)) (Z.sub ex prec))) (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta (Z.sub ex prec))) *)
(* Goal: Z.le Z0 (Z.sub prec (Zpos xH)) *)
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta (Z.sub ex prec))) *)
(* Goal: Z.le Z0 (Z.sub prec (Zpos xH)) *)
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
(* Goal: Rlt (@F2R beta (Float beta (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.sub ex prec))) (Fcore_Raux.bpow beta ex) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite F2R_Zabs, <- Hx2.
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply Hx4.
(* Goal: Z.le Z0 (Z.sub prec (Zpos xH)) *)
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply Zle_minus_le_0.
(* Goal: Z.le (Zpos xH) (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub (Z.add emin prec) (Zpos xH))))))) *)
(* Goal: Rle (Fcore_Raux.bpow beta ex) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: FTZ_format x *)
now apply (Zlt_le_succ 0).
(* Goal: Z.lt (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.pow (radix_val beta) prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply lt_Z2R.
(* Goal: Rlt (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Z2R (Z.pow (radix_val beta) prec)) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite Z2R_Zpower.
(* Goal: Rlt (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta prec) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply Rmult_lt_reg_r with (bpow (ex - prec)).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply bpow_gt_0.
(* Goal: Rlt (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta (Z.sub ex prec))) (Rmult (Fcore_Raux.bpow beta prec) (Fcore_Raux.bpow beta (Z.sub ex prec))) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite <- bpow_plus.
(* Goal: Rlt (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta (Z.sub ex prec))) (Fcore_Raux.bpow beta (Z.add prec (Z.sub ex prec))) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
replace (prec + (ex - prec))%Z with ex by ring.
(* Goal: Rlt (Rmult (Z2R (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec))))))) (Fcore_Raux.bpow beta (Z.sub ex prec))) (Fcore_Raux.bpow beta ex) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
(* Goal: Rlt (@F2R beta (Float beta (Z.abs (Ztrunc (Rmult x (Fcore_Raux.bpow beta (Z.opp (Z.sub ex prec)))))) (Z.sub ex prec))) (Fcore_Raux.bpow beta ex) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
rewrite F2R_Zabs, <- Hx2.
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply Hx4.
(* Goal: Z.le Z0 prec *)
(* Goal: Z.le emin (Z.sub ex prec) *)
now apply Zlt_le_weak.
(* Goal: Z.le emin (Z.sub ex prec) *)
now apply Zge_le.
Qed.

Theorem FTZ_format_satisfies_any :
  satisfies_any FTZ_format.
Proof.
(* Goal: satisfies_any FTZ_format *)
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp)).
(* Goal: forall x : R, iff (generic_format beta FTZ_exp x) (FTZ_format x) *)
intros x.
(* Goal: iff (generic_format beta FTZ_exp x) (FTZ_format x) *)
split.
(* Goal: FTZ_format x *)
apply FTZ_format_generic.
(* Goal: forall _ : FTZ_format x, generic_format beta FTZ_exp x *)
apply generic_format_FTZ.
Qed.

Theorem FTZ_format_FLXN :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  FLXN_format beta prec x -> FTZ_format x.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)) (_ : FLXN_format beta prec x), FTZ_format x *)
intros x Hx Fx.
(* Goal: FTZ_format x *)
apply FTZ_format_generic.
(* Goal: generic_format beta FTZ_exp x *)
apply generic_format_FLXN in Fx.
(* Goal: generic_format beta FTZ_exp x *)
revert Hx Fx.
(* Goal: forall (_ : 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 FTZ_exp x *)
apply generic_inclusion_ge.
(* Goal: forall (e : Z) (_ : Z.lt (Z.sub (Z.add emin prec) (Zpos xH)) e), Z.le (FTZ_exp e) (FLX_exp prec e) *)
intros e He.
(* Goal: Z.le (FTZ_exp e) (FLX_exp prec e) *)
unfold FTZ_exp.
(* Goal: @eq Z (Z.sub ex prec) (if Z.ltb (Z.sub ex prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub ex prec) *)
rewrite Zlt_bool_false.
(* Goal: Z.le (Z.sub e prec) (FLX_exp prec e) *)
(* Goal: Z.le emin (Z.sub e prec) *)
apply Zle_refl.
(* Goal: Z.le emin (Z.sub e prec) *)
omega.
Qed.

Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1).
Proof with auto with typeclass_instances.
unfold ulp; rewrite Req_bool_true; trivial.
case (negligible_exp_spec FTZ_exp).
intros T; specialize (T (emin-1)%Z); contradict T.
apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_.
(* Goal: Z.le emin (Z.sub e prec) *)
rewrite Zlt_bool_true; omega.
assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z).
(* Goal: Z.le emin (Z.sub e prec) *)
unfold FTZ_exp; rewrite Zlt_bool_true; omega.
intros n H2; rewrite <-V.
apply f_equal, fexp_negligible_exp_eq...
(* Goal: Z.le emin (Z.sub e prec) *)
omega.
Qed.


Section FTZ_round.

(** Rounding with FTZ *)
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

Definition Zrnd_FTZ x :=
  if Rle_bool 1 (Rabs x) then rnd x else Z0.

Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
Proof with auto with typeclass_instances.
(* Goal: iff (generic_format beta FTZ_exp x) (FTZ_format x) *)
split.
(* *)
intros x y Hxy.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
unfold Zrnd_FTZ.
case Rle_bool_spec ; intros Hx ;
  case Rle_bool_spec ; intros Hy.
4: easy.
(* 1 <= |x| *)
now apply Zrnd_le.
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_le...
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
exact Hx1.
elim Rle_not_lt with (1 := Hx1).
apply Rle_lt_trans with (2 := Hy).
apply Rle_trans with (1 := Hxy).
apply RRle_abs.
(* |x| < 1 *)
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_le...
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
elim Rle_not_lt with (1 := Hy1).
apply Rlt_le_trans with (2 := Hxy).
apply (Rabs_def2 _ _ Hx).
exact Hy1.
(* *)
intros n.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R...
case Rle_bool_spec.
easy.
rewrite <- Z2R_abs.
(* Goal: forall _ : not (@eq R x R0), and (Z.le (Z.pow (radix_val beta) (Z.sub prec (Zpos xH))) (Z.abs (@Fnum beta (Float beta Z0 emin)))) (Z.lt (Z.abs (@Fnum beta (Float beta Z0 emin))) (Z.pow (radix_val beta) prec)) *)
(* Goal: Z.le emin (@Fexp beta (Float beta Z0 emin)) *)
(* Goal: FTZ_format x *)
intros H.
generalize (lt_Z2R _ 1 H).
clear.
now case n ; trivial ; simpl ; intros [p|p|].
Qed.

Theorem round_FTZ_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.
Proof.
(* Goal: forall (x : R) (_ : Rle (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Rabs x)), @eq R (round beta FTZ_exp Zrnd_FTZ x) (round beta (FLX_exp prec) rnd x) *)
intros x Hx.
(* Goal: @eq R (round beta FTZ_exp Zrnd_FTZ x) (round beta (FLX_exp prec) rnd x) *)
unfold round, scaled_mantissa, canonic_exp.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))))) (FTZ_exp (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))))) (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))) *)
destruct (ln_beta beta x) as (ex, He). simpl.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
assert (Hx0: x <> 0%R).
(* Goal: not (@eq R x (IZR Z0)) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
intros Hx0.
(* Goal: False *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply Rle_not_lt with (1 := Hx).
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
rewrite Hx0, Rabs_R0.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply bpow_gt_0.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
specialize (He Hx0).
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
assert (He': (emin + prec <= ex)%Z).
(* Goal: Z.le (Z.add emin prec) ex *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply (bpow_lt_bpow beta).
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) (Fcore_Raux.bpow beta ex) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply Rle_lt_trans with (1 := Hx).
(* Goal: Rlt (Rabs x) (Fcore_Raux.bpow beta ex) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply He.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
replace (FTZ_exp ex) with (FLX_exp prec ex).
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
unfold Zrnd_FTZ.
(* Goal: @eq R (@F2R beta (Float beta (if Rle_bool (IZR (Zpos xH)) (Rabs (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) then rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) else Z0) (FLX_exp prec ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite Rle_bool_true.
(* Goal: @eq Z (Z.sub ex prec) (Z.sub ex prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply refl_equal.
(* Goal: Rle (IZR (Zpos xH)) (Rabs (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite Rabs_mult.
(* Goal: Rle (IZR (Zpos xH)) (Rmult (Rabs x) (Rabs (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))).
(* Goal: Rle (IZR (Zpos xH)) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
change 1%R with (bpow 0).
(* Goal: Rle (Fcore_Raux.bpow beta Z0) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite <- (Zplus_opp_r (FLX_exp prec ex)).
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (FLX_exp prec ex) (Z.opp (FLX_exp prec ex)))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite bpow_plus.
(* Goal: Rle (Rmult (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_ge_0.
(* Goal: Rle (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Rabs x) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply Rle_trans with (2 := proj1 He).
(* Goal: Rle (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_le.
(* Goal: Z.le (FLX_exp prec ex) (Z.sub ex (Zpos xH)) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
unfold FLX_exp.
(* Goal: Z.le (Z.sub ex prec) (Z.sub ex (Zpos xH)) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
generalize (prec_gt_0 prec).
(* Goal: Z.le emin (Z.sub e prec) *)
clear -He' ; omega.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_ge_0.
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
unfold FLX_exp, FTZ_exp.
(* Goal: @eq Z (Z.sub ex prec) (if Z.ltb (Z.sub ex prec) emin then Z.sub (Z.add emin prec) (Zpos xH) else Z.sub ex prec) *)
rewrite Zlt_bool_false.
(* Goal: @eq Z (Z.sub ex prec) (Z.sub ex prec) *)
(* Goal: Z.le emin (Z.sub ex prec) *)
apply refl_equal.
(* Goal: Z.le emin (Z.sub e prec) *)
clear -He' ; omega.
Qed.

Theorem round_FTZ_small :
  forall x : R,
  (Rabs x < bpow (emin + prec - 1))%R ->
  round beta FTZ_exp Zrnd_FTZ x = R0.
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)), @eq R (round beta FTZ_exp Zrnd_FTZ x) (round beta (FLX_exp prec) rnd x) *)
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply round_0...
(* Goal: @eq R (round beta FTZ_exp Zrnd_FTZ x) (round beta (FLX_exp prec) rnd x) *)
unfold round, scaled_mantissa, canonic_exp.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))))) (FTZ_exp (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))))) (FLX_exp prec (ln_beta_val beta x (Build_ln_beta_prop beta x ex He))))) *)
destruct (ln_beta beta x) as (ex, He). simpl.
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
specialize (He Hx0).
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
unfold Zrnd_FTZ.
rewrite Rle_bool_false.
(* Goal: @eq R (@F2R beta (Float beta Z0 xe)) R0 *)
(* Goal: Z.le (FTZ_exp (ln_beta_val beta x (ln_beta beta x))) (FLX_exp prec (ln_beta_val beta x (ln_beta beta x))) *)
(* Goal: generic_format beta (FLX_exp prec) x *)
apply F2R_0.
(* Goal: Rle (IZR (Zpos xH)) (Rabs (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))).
(* Goal: Rle (IZR (Zpos xH)) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
change 1%R with (bpow 0).
rewrite <- (Zplus_opp_r (FTZ_exp ex)).
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (FLX_exp prec ex) (Z.opp (FLX_exp prec ex)))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex)))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
rewrite bpow_plus.
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.sub (Z.add emin prec) (Zpos xH))) *)
(* Goal: @eq R (@F2R beta (Float beta (Zrnd_FTZ (Rmult x (Fcore_Raux.bpow beta (Z.opp (FTZ_exp ex))))) (FTZ_exp ex))) (@F2R beta (Float beta (rnd (Rmult x (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))))) (FLX_exp prec ex))) *)
apply bpow_gt_0.
apply Rlt_le_trans with (1 := Hx).
(* Goal: Rle (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_le.
(* Goal: Z.le (FTZ_exp e) (FLX_exp prec e) *)
unfold FTZ_exp.
generalize (Zlt_cases (ex - prec) emin).
case Zlt_bool.
intros _.
(* Goal: Z.le (Z.sub e prec) (FLX_exp prec e) *)
(* Goal: Z.le emin (Z.sub e prec) *)
apply Zle_refl.
intros He'.
elim Rlt_not_le with (1 := Hx).
(* Goal: Rle (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Rabs x) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply Rle_trans with (2 := proj1 He).
(* Goal: Rle (Fcore_Raux.bpow beta (FLX_exp prec ex)) (Fcore_Raux.bpow beta (Z.sub ex (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_le.
(* Goal: Z.le emin (Z.sub e prec) *)
omega.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (FLX_exp prec ex))) *)
(* Goal: @eq Z (FLX_exp prec ex) (FTZ_exp ex) *)
apply bpow_ge_0.
Qed.

End FTZ_round.

End RND_FTZ.
