(**
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 without 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_FIX.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.

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 }.

(* unbounded floating-point format *)
Definition FLX_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z.

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

(** Properties of the FLX format *)

Global Instance FLX_exp_valid : Valid_exp FLX_exp.
Proof.
(* Goal: Valid_exp FLX_exp *)
intros k.
(* Goal: forall e : Z, and (forall _ : Z.lt (FLX_exp e) e, Z.lt (FLX_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLX_exp e), @eq Z (FLX_exp (Z.add (FLX_exp e) (Zpos xH))) (FLX_exp e)) *)
unfold FLX_exp.
(* Goal: and (forall _ : Z.lt (Z.sub k prec) k, Z.le (Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (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 (Z.sub l prec) (Z.sub k prec))) *)
generalize prec_gt_0.
(* Goal: forall _ : Z.lt Z0 prec, and (forall _ : Z.lt (Z.sub k prec) k, Z.le (Z.sub (Z.add k (Zpos xH)) prec) k) (forall _ : Z.le k (Z.sub k prec), and (Z.le (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 (Z.sub l prec) (Z.sub k prec))) *)
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.
Proof.
(* Goal: forall (x : R) (_ : FLX_format x), generic_format beta FLX_exp x *)
clear prec_gt_0_.
(* Goal: forall (x : R) (e : Z) (_ : and (Rle (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Rabs x)) (Rle (Rabs x) (Fcore_Raux.bpow beta e))) (_ : FLX_format x), FIX_format beta (Z.sub e prec) x *)
intros x e Hx ((xm, xe), (H1, H2)).
(* Goal: FIX_format beta (Z.sub e prec) x *)
rewrite H1, (F2R_prec_normalize beta xm xe e prec).
(* Goal: FIX_format beta (Z.sub e prec) (@F2R beta (Float beta (Z.mul xm (Z.pow (radix_val beta) (Z.add (Z.sub xe e) prec))) (Z.sub e prec))) *)
(* Goal: Z.lt (Z.abs xm) (Z.pow (radix_val beta) prec) *)
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Rabs (@F2R beta (Float beta xm xe))) *)
now eexists.
(* Goal: Z.lt (Z.abs xm) (Z.pow (radix_val beta) prec) *)
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Rabs (@F2R beta (Float beta xm xe))) *)
exact H2.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Rabs (@F2R beta (Float beta xm xe))) *)
now rewrite <- H1.
Qed.

Theorem FLX_format_generic :
  forall x, generic_format beta FLX_exp x -> FLX_format x.
Proof.
intros x H.
rewrite H.
unfold FLX_format.
(* Goal: FLX_format (@F2R beta (Float beta xm ex)) *)
eexists ; repeat split.
simpl.
apply lt_Z2R.
rewrite Z2R_abs.
rewrite <- scaled_mantissa_generic with (1 := H).
rewrite <- scaled_mantissa_abs.
apply Rmult_lt_reg_r with (bpow (canonic_exp beta FLX_exp (Rabs x))).
apply bpow_gt_0.
rewrite scaled_mantissa_mult_bpow.
rewrite Z2R_Zpower, <- bpow_plus.
2: now apply Zlt_le_weak.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLX_exp x)) *)
unfold canonic_exp, FLX_exp.
ring_simplify (prec + (ln_beta beta (Rabs x) - prec))%Z.
rewrite ln_beta_abs.
destruct (Req_dec x 0) as [Hx|Hx].
rewrite Hx, Rabs_R0.
apply bpow_gt_0.
destruct (ln_beta beta x) as (ex, Ex).
now apply Ex.
Qed.

Theorem generic_format_FLX :
  forall x, FLX_format x -> generic_format beta FLX_exp x.
Proof.
(* Goal: forall (x : R) (_ : FLX_format x), generic_format beta FLX_exp x *)
clear prec_gt_0_.
(* Goal: forall (x : R) (_ : FLX_format x), generic_format beta FLX_exp x *)
intros x ((mx,ex),(H1,H2)).
(* Goal: generic_format beta FLX_exp x *)
simpl in H2.
(* Goal: FLX_format x *)
rewrite H1.
(* Goal: generic_format beta FLX_exp (@F2R beta (Float beta mx ex)) *)
apply generic_format_F2R.
(* Goal: forall _ : not (@eq Z mx Z0), Z.le (canonic_exp beta FLX_exp (@F2R beta (Float beta mx ex))) ex *)
intros Zmx.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLX_exp x)) *)
unfold canonic_exp, FLX_exp.
(* Goal: Z.le (Z.sub (ln_beta_val beta (@F2R beta (Float beta mx ex)) (ln_beta beta (@F2R beta (Float beta mx ex)))) prec) ex *)
rewrite ln_beta_F2R with (1 := Zmx).
(* Goal: Z.le (Z.sub (Z.add (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) ex) prec) ex *)
apply Zplus_le_reg_r with (prec - ex)%Z.
(* Goal: Z.le (Z.add (Z.sub (Z.add (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) ex) prec) (Z.sub prec ex)) (Z.add ex (Z.sub prec ex)) *)
ring_simplify.
(* Goal: Z.le (ln_beta_val beta (Z2R mx) (ln_beta beta (Z2R mx))) prec *)
now apply ln_beta_le_Zpower.
Qed.

Theorem FLX_format_satisfies_any :
  satisfies_any FLX_format.
Proof.
(* Goal: satisfies_any FLXN_format *)
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).
(* Goal: forall x : R, iff (generic_format beta FLX_exp x) (FLX_format x) *)
intros x.
(* Goal: iff (generic_format beta FLX_exp x) (FLX_format x) *)
split.
(* Goal: forall _ : generic_format beta FLX_exp x, FLX_format x *)
(* Goal: forall _ : FLX_format x, generic_format beta FLX_exp x *)
apply FLX_format_generic.
(* Goal: 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.
Proof with auto with typeclass_instances.
intros x e Hx Fx.
(* Goal: forall _ : generic_format beta FLX_exp x, FLX_format x *)
(* Goal: forall _ : FLX_format x, generic_format beta FLX_exp x *)
apply FLX_format_generic.
apply generic_format_FIX in Fx.
revert Fx.
apply generic_inclusion with (e := e)...
apply Zle_refl.
Qed.

(** unbounded floating-point format with normal mantissas *)
Definition FLXN_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (x <> R0 ->
  Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z.

Theorem generic_format_FLXN :
  forall x, FLXN_format x -> generic_format beta FLX_exp x.
Proof.
(* Goal: forall (x : R) (_ : FLXN_format x), generic_format beta FLX_exp x *)
intros x ((xm,ex),(H1,H2)).
(* Goal: generic_format beta FLX_exp x *)
destruct (Req_dec x 0) as [Zx|Zx].
(* Goal: generic_format beta FLX_exp x *)
(* Goal: generic_format beta FLX_exp x *)
rewrite Zx.
(* Goal: generic_format beta FLX_exp (IZR Z0) *)
(* Goal: generic_format beta FLX_exp x *)
apply generic_format_0.
(* Goal: generic_format beta FLX_exp x *)
specialize (H2 Zx).
(* Goal: generic_format beta FLX_exp x *)
apply generic_format_FLX.
(* Goal: FLX_format x *)
rewrite H1.
(* Goal: FLX_format (@F2R beta (Float beta xm ex)) *)
eexists ; repeat split.
(* Goal: Z.lt (Z.abs (@Fnum beta (Float beta xm ex))) (Z.pow (radix_val beta) prec) *)
apply H2.
Qed.

Theorem FLXN_format_generic :
  forall x, generic_format beta FLX_exp x -> FLXN_format x.
Proof.
intros x Hx.
rewrite Hx.
simpl.
(* Goal: iff (generic_format beta FLX_exp x) (FLX_format x) *)
eexists ; split. split.
simpl.
rewrite <- Hx.
intros Zx.
(* Goal: iff (generic_format beta FLX_exp x) (FLX_format x) *)
split.
(* *)
apply le_Z2R.
rewrite Z2R_Zpower.
2: now apply Zlt_0_le_0_pred.
rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx).
apply Rmult_le_reg_r with (bpow (canonic_exp beta FLX_exp x)).
apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite <- scaled_mantissa_abs.
rewrite <- canonic_exp_abs.
rewrite scaled_mantissa_mult_bpow.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLX_exp x)) *)
unfold canonic_exp, FLX_exp.
rewrite ln_beta_abs.
ring_simplify (prec - 1 + (ln_beta beta x - prec))%Z.
destruct (ln_beta beta x) as (ex,Ex).
now apply Ex.
(* *)
apply lt_Z2R.
rewrite Z2R_Zpower.
2: now apply Zlt_le_weak.
rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx).
apply Rmult_lt_reg_r with (bpow (canonic_exp beta FLX_exp x)).
apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite <- scaled_mantissa_abs.
rewrite <- canonic_exp_abs.
rewrite scaled_mantissa_mult_bpow.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLX_exp x)) *)
unfold canonic_exp, FLX_exp.
rewrite ln_beta_abs.
ring_simplify (prec + (ln_beta beta x - prec))%Z.
destruct (ln_beta beta x) as (ex,Ex).
now apply Ex.
Qed.

Theorem FLXN_format_satisfies_any :
  satisfies_any FLXN_format.
Proof.
(* Goal: satisfies_any FLXN_format *)
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).
(* Goal: forall x : R, iff (generic_format beta FLX_exp x) (FLXN_format x) *)
split ; intros H.
(* Goal: FLXN_format x *)
(* Goal: generic_format beta FLX_exp x *)
now apply FLXN_format_generic.
(* Goal: generic_format beta FLX_exp x *)
now apply generic_format_FLXN.
Qed.

Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Proof.
(* Goal: @eq R (ulp beta FLX_exp (IZR Z0)) (IZR Z0) *)
unfold ulp; rewrite Req_bool_true; trivial.
(* Goal: @eq R match negligible_exp FLX_exp with | Some n => Fcore_Raux.bpow beta (FLX_exp n) | None => IZR Z0 end (IZR Z0) *)
case (negligible_exp_spec FLX_exp).
(* Goal: forall _ : forall n : Z, Z.lt (FLX_exp n) n, @eq R (IZR Z0) (IZR Z0) *)
(* Goal: forall (n : Z) (_ : Z.le n (FLX_exp n)), @eq R (Fcore_Raux.bpow beta (FLX_exp n)) (IZR Z0) *)
intros _; reflexivity.
(* Goal: forall (n : Z) (_ : Z.le n (FLX_exp n)), @eq R (Fcore_Raux.bpow beta (FLX_exp n)) (IZR Z0) *)
intros n H2; contradict H2.
(* Goal: not (Z.le n (FLX_exp n)) *)
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.

Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
(* Goal: forall x : R, Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
intros x; case (Req_dec x 0); intros Hx.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
rewrite Hx, ulp_FLX_0, Rabs_R0.
(* Goal: Rle (Rmult (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec))) (IZR Z0) *)
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
right; ring.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
rewrite ulp_neq_0; try exact Hx.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLX_exp x)) *)
unfold canonic_exp, FLX_exp.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub (ln_beta_val beta x (ln_beta beta x)) prec)) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (Z.sub (ln_beta_val beta x (ln_beta beta x)) (Zpos xH)) (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
rewrite bpow_plus.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rle (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
apply bpow_ge_0.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub (ln_beta_val beta x (ln_beta beta x)) (Zpos xH))) (Rabs x) *)
now apply bpow_ln_beta_le.
Qed.


Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R.
Proof.
(* Goal: forall x : R, Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
intros x; case (Req_dec x 0); intros Hx.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
rewrite Hx, ulp_FLX_0, Rabs_R0.
(* Goal: Rle (Rmult (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec))) (IZR Z0) *)
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
right; ring.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (ulp beta FLX_exp x) *)
rewrite ulp_neq_0; try exact Hx.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Fcore_Raux.bpow beta (canonic_exp beta FLX_exp x)) *)
unfold canonic_exp, FLX_exp.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.add (Z.sub (ln_beta_val beta x (ln_beta beta x)) (Zpos xH)) (Z.sub (Zpos xH) prec))) (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.sub (Zpos xH) prec))) *)
unfold Zminus; rewrite bpow_plus.
(* Goal: Rle (Rmult (Rabs x) (Fcore_Raux.bpow beta (Z.opp prec))) (Rmult (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) (Fcore_Raux.bpow beta (Z.opp prec))) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp prec)) *)
(* Goal: Rle (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
apply bpow_ge_0.
(* Goal: Rle (Rabs x) (Fcore_Raux.bpow beta (ln_beta_val beta x (ln_beta beta x))) *)
left; now apply bpow_ln_beta_gt.
Qed.

(** FLX is a nice format: it has a monotone exponent... *)
Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
Proof.
(* Goal: Monotone_exp FLX_exp *)
intros ex ey Hxy.
(* Goal: Z.le (FLX_exp ex) (FLX_exp ey) *)
now apply Zplus_le_compat_r.
Qed.

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

Global Instance exists_NE_FLX : Exists_NE beta FLX_exp.
Proof.
(* Goal: Exists_NE beta FLX_exp *)
destruct NE_prop as [H|H].
(* Goal: Exists_NE beta FLX_exp *)
(* Goal: Exists_NE beta FLX_exp *)
now left.
(* Goal: Exists_NE beta FLX_exp *)
right.
(* Goal: forall e : Z, and (forall _ : Z.lt (FLX_exp e) e, Z.lt (FLX_exp (Z.add e (Zpos xH))) e) (forall _ : Z.le e (FLX_exp e), @eq Z (FLX_exp (Z.add (FLX_exp e) (Zpos xH))) (FLX_exp e)) *)
unfold FLX_exp.
(* Goal: forall e : Z, and (forall _ : Z.lt (Z.sub e prec) e, Z.lt (Z.sub (Z.add e (Zpos xH)) prec) e) (forall _ : Z.le e (Z.sub e prec), @eq Z (Z.sub (Z.add (Z.sub e prec) (Zpos xH)) prec) (Z.sub e prec)) *)
split ; omega.
Qed.

End RND_FLX.
