Library Interval.Float.Basic

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq:
Copyright (C) 2007-2016, Inria
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL:
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import Reals ZArith Psatz.
From Flocq Require Import Core.

Require Import Xreal.

Variant rounding_mode : Set :=
  rnd_UP | rnd_DN | rnd_ZR | rnd_NE.

Definition Rnearbyint mode r :=
  match mode with
  | rnd_UPIZR (Zceil r)
  | rnd_DNIZR (Zfloor r)
  | rnd_ZRIZR (Ztrunc r)
  | rnd_NEIZR (ZnearestE r)

Notation Xnearbyint := (fun modeXlift (Rnearbyint mode)).

Lemma Rnearbyint_le :
   mode x y,
  (x y)%R
  (Rnearbyint mode x Rnearbyint mode y)%R.

Lemma Rnearbyint_error_DN x :
  (-1 Rnearbyint rnd_DN x - x 0)%R.

Lemma Rnearbyint_error_UP x :
  (0 Rnearbyint rnd_UP x - x 1)%R.

Lemma Rnearbyint_error_ZR_neg x :
  (x 0
   0 Rnearbyint rnd_ZR x - x 1)%R.

Lemma Rnearbyint_error_ZR_pos x :
  (0 x
   -1 Rnearbyint rnd_ZR x - x 0)%R.

Lemma Rnearbyint_error_ZR x :
  (-1 Rnearbyint rnd_ZR x - x 1)%R.

Lemma Rnearbyint_error_NE x :
  (- (1/2) Rnearbyint rnd_NE x - x 1/2)%R.

Lemma Rnearbyint_error m x :
  (-1 Rnearbyint m x - x 1)%R.

Notation radix2 := Zaux.radix2 (only parsing).

Section Definitions.

Variable beta : radix.

Fixpoint count_digits_aux nb pow (p q : positive) { struct q } : positive :=
  if Zlt_bool (Zpos p) pow then nb
    match q with
    | xHnb
    | xI rcount_digits_aux (Pos.succ nb) (Zmult beta pow) p r
    | xO rcount_digits_aux (Pos.succ nb) (Zmult beta pow) p r

Definition count_digits n :=
  count_digits_aux 1 beta n n.

Definition FtoR (s : bool) m e :=
  let sm := if s then Zneg m else Zpos m in
  match e with
  | Zpos pIZR (sm × Zpower_pos beta p)
  | Z0IZR sm
  | Zneg p ⇒ (IZR sm / IZR (Zpower_pos beta p))%R

End Definitions.

Definition rnd_of_mode mode :=
  match mode with
  | rnd_UPrndUP
  | rnd_DNrndDN
  | rnd_ZRrndZR
  | rnd_NErndNE

Definition error_fix mode emin x :=
  (round radix2 (FIX_exp emin) (rnd_of_mode mode) x - x)%R.

Definition Xerror_fix mode emin := Xlift (error_fix mode emin).

Definition round_fix mode emin :=
  round radix2 (FIX_exp emin) (rnd_of_mode mode).

Definition Xround_fix mode emin := Xlift (round_fix mode emin).

Definition error_flt mode emin prec x :=
  (round radix2 (FLT_exp emin (Zpos prec)) (rnd_of_mode mode) x - x)%R.

Definition Xerror_flt mode emin prec := Xlift (error_flt mode emin prec).

Definition round_flt mode emin prec :=
  round radix2 (FLT_exp emin (Zpos prec)) (rnd_of_mode mode).

Definition Xround_flt mode emin prec := Xlift (round_flt mode emin prec).

Definition round beta mode prec :=
  round beta (FLX_exp (Zpos prec)) (rnd_of_mode mode).

Definition Xround beta mode prec := Xlift (round beta mode prec).

Inductive float (beta : radix) : Set :=
  | Fnan : float beta
  | Fzero : float beta
  | Float : bool positive Z float beta.

Arguments Fnan {beta}.
Arguments Fzero {beta}.
Arguments Float {beta} _ _ _.

Definition FtoX {beta} (f : float beta) :=
  match f with
  | FzeroXreal 0
  | FnanXnan
  | Float s m eXreal (FtoR beta s m e)

Lemma zpos_gt_0 : prec, Prec_gt_0 (Zpos prec).

Lemma valid_rnd_of_mode : mode, Valid_rnd (rnd_of_mode mode).

Lemma FtoR_split :
   beta s m e,
  FtoR beta s m e = F2R (Defs.Float beta (cond_Zopp s (Zpos m)) e).

Lemma is_zero_correct_float :
   beta s m e,
  is_zero (FtoR beta s m e) = false.

Definition le_upper x y :=
  match y with
  | XnanTrue
  | Xreal yr
    match x with
    | XnanFalse
    | Xreal xrRle xr yr

Definition le_lower x y :=
  le_upper (Xneg y) (Xneg x).

Lemma le_upper_refl : x, le_upper x x.

Lemma le_lower_refl : x, le_upper x x.

Lemma le_upper_trans :
   x y z,
  le_upper x y le_upper y z le_upper x z.

Lemma le_lower_trans :
   x y z,
  le_lower x y le_lower y z le_lower x z.